Large language models translate legacy code quickly, but a translation can differ from the original on inputs that no test exercises. We show that LLM translations of whole, unmodified COBOL programs into Rust and Java can be proved in Lean 4 to behave like our semantics of the originals on every admissible input: a bounded number of well-formed records, among other premises. The COBOL semantics is executable; it computes record layouts, decimal arithmetic and file handling from our front end's output for the unmodified source. For the eight standalone batch programs of AWS CardDemo covered by that front end, all 16 translations are proved, as equivalences for Rust and as refinements with partial correctness for Java. The statements are generated from the programs except for a few small parts, LLM agents write the proofs, and Lean's kernel checks them. Before any proof, 35% of the first running translations differed from our semantics of the original on a generated input, and no proof found a difference that this testing had missed.
In plain words
Large organisations still run batch programs written in COBOL, and many plan to move them to Java or Rust. AI language models translate such programs quickly, but a translation can behave differently from the original on inputs that no test tried; in this study, about a third of the first translations that ran gave different results from the paper’s model of the original on generated test inputs. From CardDemo, a public mainframe application, the paper takes the eight batch programs that run on their own and that the paper’s tools can read. For each, it proves in the Lean proof assistant that a Rust translation and a Java translation behave like the original on every allowed input, with the original’s meaning as the paper defines it. For Java, the proof covers only the runs that finish.
Illustration of the paper’s main result. Each row is one of the eight standalone batch programs of AWS CardDemo that the paper’s COBOL front end covers, with a description of the program and its length in non-comment lines of COBOL, not counting copybooks. A teal cell marks a translation into Rust or Java that is proved in Lean to behave like the paper’s semantics of the COBOL program on every admissible input: an equivalence for Rust, a refinement with partial correctness for Java. For CBACT01C, CBTRN02C and CBTRN03C, the proved Java translation is the one written under a second style guide, introduced after the proofs of the first-guide translations had stalled. An orange dot marks a program whose Lean statement includes a part written directly by LLM agents rather than generated: a model of the assembler routine COBDATFT for CBACT01C, and an input domain for each of CBACT04C, CBTRN02C and CBTRN03C.
