\section{Introduction}
\label{sec:intro}

Large organisations still run batch jobs written in COBOL, and many of them plan to move this code to Java or to
memory-safe languages such as Rust. Large language models now write such translations quickly. The translations, however,
can be wrong in ways that are easy to miss: a sort order that follows Unicode instead of EBCDIC, a field read before it
is set, or a total that the original program carries from one record to the next. Testing finds many of these
defects, but a test suite exercises only the inputs that someone thought to write down. When a translation replaces the
original, the question is whether the two programs behave the same on every input.

A proof answers that question only if its statement, the meaning of both programs and the proof itself can be
trusted. For a whole program, a statement written by hand can be as wrong as the translation it is meant to check.
The meaning matters above all for the COBOL program, in which record layouts, decimal arithmetic, the EBCDIC
collating order and file handling all decide the outcome. And the proof of a whole program is long. We address
each in turn. For the \aTheorems{} migration theorems, a generator writes each statement from the COBOL program and the translation's
interface; only three
small input domains and the model of one assembler routine are written directly, by LLM agents, and the generator itself belongs to the trusted base. The COBOL side is an executable Lean semantics of our front end's
output for the unmodified source, which we check by differential testing and on the NIST COBOL85 suite in GnuCOBOL's conventions for characters and signs. The IBM conventions used in the theorems are tested only in an
exploratory run, with gaps listed in Section~\ref{sec:limits}. LLM agents write the proofs, but Lean's kernel checks
every one of them, so no proof step has to be trusted.

We apply this to AWS CardDemo, a public mainframe application, and take the eight batch programs of CardDemo that run
on their own and are covered by our COBOL front end. A language model translates each program to Rust and to Java in a
repair loop, and nobody edits its output (Section~\ref{sec:migration}). For each of the \aTheorems{} translations we
prove in Lean~4~\cite{lean4} that it behaves like our semantics of the original COBOL program on every \emph{admissible}
input: records whose fields fit their declared formats, bounded in number, together with the further premises listed in Section~\ref{sec:example}. For Rust
the theorem is an equivalence of the two programs' outcomes: the lines they display, the records they write and rewrite
(compared as field values decoded by the COBOL program's layouts), whether they end abnormally, that is, abend, and the
return code where the program sets one. For
Java it is a refinement with partial correctness: whenever the COBOL run is safe, no Java run goes wrong, and every
Java run that terminates matches the COBOL outcome.

All \aTheorems{} translations are proved. For three Java programs, the proved translations come from a second style
guide, which we introduced after the proofs of those programs' first-guide translations had stalled. In the agents' checks, the unchanged proof of a theorem fails to check or times out when any of the \aMutants{} seeded
mutants replaces its translation (Section~\ref{sec:trust}). The translation runs also show how the model
goes wrong. In \aaFirstDiff{} of the \aaRuns{} runs (\aaFirstDiffPct\%), the first version that ran disagreed with our
semantics of the COBOL program on some generated input. Testing on the semantics found every behavioural error we know
of, and none of the 16 proofs exposed a further difference. Instead, the proofs required bounds on the number of records and
corrections to some of the statements.

Our verification stack (Section~\ref{sec:stack}) also has semantics for C and C++, through ClangIR, and for a subset of
TypeScript. Section~\ref{sec:further} summarises its uses on code that was not translated from COBOL: Rust ports of C
code, fuzzing harnesses, library commits, random samples and Apache Thrift. There the results are more limited, and
the technical report~\cite{fvtechreport} gives them in full.

Our contributions are:
\begin{itemize}
\item Proved migration: \aTheorems{} kernel-checked theorems that relate LLM translations of the eight standalone
CardDemo batch programs covered by our front end to our semantics of the unmodified COBOL programs on every admissible
input, with mostly generated statements and a mutation test of the theorems (Sections~\ref{sec:example}
to~\ref{sec:trust}).
\item A measurement of LLM translation errors in this batch layer, by prompt and language, in which each behavioural
error is witnessed by an input on which the translation and the original disagree (Section~\ref{sec:migration}).
\item Lean semantics for COBOL, C and C++, Java and a TypeScript subset, joined by one notion of simulation and each tested against a reference implementation (Sections~\ref{sec:stack} and~\ref{sec:trust}); Section~\ref{sec:limits} summarizes their known defects.
\end{itemize}
Section~\ref{sec:example} works through one program, Section~\ref{sec:stack} describes the stack, and
Section~\ref{sec:migration} reports the migration study. Section~\ref{sec:trust} states what the theorems rely on and
how we tested the semantics, and Section~\ref{sec:further} summarises the further uses. Sections~\ref{sec:related}
and~\ref{sec:limits} discuss related work and the limitations.