\section{Versions}
\label{app:pins}

Lean is v4.35.0 throughout. The versions listed are those of our frozen copies, on which our own checks ran; the technical report~\cite{fvtechreport} lists the versions behind most other results.

\begin{itemize}
\item Migration theorems: equiv-lean \code{751764f}, whose migration modules are byte-identical to those we checked at
\code{a572cf6}, with the COBOL semantics of the coblean snapshot \code{20261024T2306Z}, JimpleLean
\code{20261025T0149Z}, Charon \code{de8736f} and Aeneas \code{fdebf20}. AWS CardDemo at \code{59cc6c2f}. GnuCOBOL
3.2.0, JDK 17, Soot 4.7.1.
\item Termination of the Java translations: equiv-lean \code{9f0e5fb} with JimpleLean \code{20261025T2312Z}, the
termination version. The composite theorems: equiv-lean \code{ba05f6e}, on the same versions. The refutations of three
mutants' statements: equiv-lean \code{47d9ce3}, with JimpleLean \code{20261025T2312Z}.
\item CBSTM03B: coblean snapshot \code{pin2306Z-cbstm03b-20261027T0112Z}; its translations: equiv-lean \code{cc9e349}
(partial correctness for Java) and \code{0fd209e} (total correctness), with JimpleLean \code{20261025T2312Z} and Aeneas
\code{fdebf20}. CBSTM03A with CBSTM03B: snapshot \code{pin2306Z-cbstm03ab-20261027T1251Z}; its translations: equiv-lean
\code{a50f10e} (Rust) and \code{8ed869e} (Java), on the versions of the joint build. CSUTLDTC: snapshot
\code{pinM3-csutldtc-20261027T2010Z}, on the semantics of snapshot \code{20261027T2008Z}. COBSWAIT: snapshot
\code{pinM7-cobswait-20261028T0554Z}, on the semantics of snapshot \code{20261028T0551Z}.
\item The joint build, which builds the migration theorems together with later results: equiv-lean \code{04d2599}, with cirlean \code{e6ac99a}, JimpleLean \code{20261026T2035Z}, StrictTS
\code{a15926a}, coblean \code{20261024T2306Z} and Aeneas \code{fdebf20}; the composite theorems and the refutations are
added in \code{89806a8} and \code{b46c478}, which change no file of \code{04d2599}.
\item C semantics: the three later versions of Sections~\ref{sec:validation} and~\ref{sec:limits} are cirlean
\code{e6ac99a}, \code{424e821} and \code{7c73739}; the last is the one frozen after the runs behind our theorems.
\item C to Rust: equiv-lean \code{751764f}, cirlean \code{28e2380}, ClangIR from llvm-project \code{4955d32b}, Charon
\code{de8736f} and Aeneas \code{fdebf20}, tiny-regex-c \code{f2632c6}. jsmn: equiv-lean \code{373874f} with the same
tools, jsmn \code{25647e6}. Adler-32: equiv-lean \code{ff07aac} with the same tools, zlib 1.3.1 (\code{51b7f2ab}).
\end{itemize}

\section{Pre-registrations}
\label{app:prereg}

The migration study and its measurement of translation errors followed a fixed protocol (Section~\ref{sec:protocol})
but had no pre-registration. The studies in the table below are pre-registered: a file with the procedure, the outcomes
and the analysis was frozen before the runs it governs, together with a SHA-256 manifest of its input files (samples,
commit lists, selection tools), and addenda fixed the samples and inputs left open by a file, each frozen before the
runs it governs. Later decisions went into an append-only deviation log, and each is reported where it affects a
number. For a run with \emph{inputs recorded}, the inputs and the tool commit were fixed and hashed before it started,
but no analysis was frozen. A result is \emph{exploratory} if it lies outside the migration study and every pre-registration and we logged it as such, with its date, in the deviation log, where such results are tagged ``labelled''. The files, the log and their SHA-256 hashes are in the artifact. Because
no hash was deposited with a third party, this record is self-attested.

\begin{center}
\small
\begin{tabular}{lll}
\toprule
File & Study & Frozen (UTC) \\
\midrule
\code{PREREG\_C\_v2.md} & security fixes, proof reuse & 2026-10-24 \\
\code{PREREG\_D\_v2.md} & random samples, first run & 2026-10-24 \\
\code{PREREG\_C1b\_v1.md} & security fixes, second pass & 2026-10-25 \\
\code{PREREG\_D2\_v1.md} & random samples, second run & 2026-10-25 \\
\code{PREREG\_T\_v1.md} & Thrift & 2026-10-25 \\
\code{PREREG\_M\_v1.md} & mutants of the semantics & 2026-10-25 \\
\code{PREREG\_N\_v1.md} & NIST COBOL85 & 2026-10-25 \\
\code{PREREG\_H\_v1.md} & fuzz harnesses & 2026-10-25 \\
\code{PREREG\_V\_v1.md} & LLVM test programs & 2026-10-25 \\
\bottomrule
\end{tabular}
\end{center}

\section{Model settings}
\label{app:llm}


All model calls go to one commercial LLM through its API, in October 2026, with a fixed reasoning-effort setting and at
most 64,000 output tokens per call. Translation runs allow at most 10 attempts and \$15 each, with 60 fresh generated
cases per round and 300 for the final check, and seeds 1 to 3 for the input generator. The root-cause labels were produced by further calls with a fixed prompt, one per run in 30 of the 32 runs with behaviour
repairs; repairs that only fixed build failures were labelled from the build error, without a model call. In the security-fix and sample studies, the orchestrator uses the
same model for contracts, invariants and proof scripts, with three proposals per proof. The proofs of the migration
theorems were written by LLM agents and checked by Lean (Section~\ref{sec:effort}).