HEXAGONbeta

Proof-Carrying Modernization: LLM Translations of COBOL Batch Programs, Each Proved Against the Original in Lean

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Science

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

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.

References

  1. Leonardo de Moura; Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021
  2. The LLVM Project. ClangIR: a high-level MLIR dialect for C and C++. 2026. https://llvm.github.io/clangir/; upstream llvm-project commit 4955d32b used herelink
  3. Raja Vallée-Rai; Phong Co; Etienne Gagnon; Laurie Hendren; Patrick Lam; Vijay Sundaresan. Soot – a Java Bytecode Optimization Framework. Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research (CASCON). 1999
  4. son-risa. CBACT04C (INTCALC): the last account's interest is written as a transaction but never added to the account. 2026. Opened 2026-10-03. CardDemo issue #64, https://github.com/aws-samples/aws-mainframe-modernization-carddemo/issues/64link
  5. Michael Tautschnig. Bound externally-controlled reference-modification lengths and subscripts. 2026. Opened 2026-06-17. CardDemo pull request #54, https://github.com/aws-samples/aws-mainframe-modernization-carddemo/pull/54link
  6. Son Ho; Jonathan Protzenko. Aeneas: Rust Verification by Functional Translation. Proceedings of the ACM on Programming Languages, vol. 6, no. ICFP, pp. 711–741. 2022
  7. Son Ho; Guillaume Boisseau; Lucas Franceschino; Yoann Prak; Aymeric Fromherz; Jonathan Protzenko. Charon: An Analysis Framework for Rust. Computer Aided Verification (CAV), pp. 377–391. 2025DOI
  8. Petr Bauch. circe: Lean-based verification tool for C++. 2026. https://github.com/petr-bauch/circe, public since 2026-09-21link
  9. opencompl. VeIR pull request #1346: cir: add the CIR integer and core dialect. 2026. https://github.com/opencompl/veir/pull/1346, merged 2026-09-02link
  10. Marco Paganoni; Carlo A. Furia. Verifying Functional Correctness Properties at the Level of Java Bytecode. Formal Methods (FM). 2023
Show all 53 referencesShow fewer references
  1. Denis Bogdănaş; Grigore Roşu. K-Java: A Complete Semantics of Java. Principles of Programming Languages (POPL). 2015
  2. Dominik Blain. IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking. 2026. arXiv:2610.11073
  3. Abdulaziz Abdujalilov. cobol-equiv: differential testing harness and a Python runtime for COBOL numeric semantics. 2026. https://github.com/abdulazizbalu/cobol-equiv, created 2026-10-13link
  4. Jesse Alama. Thales and Tarski: a proof tool for TypeScript and a JavaScript semantics in Lean 4. 2026. https://github.com/lakatos-ts/thaleslink
  5. Midspiral. LemmaScript: a verification toolchain for TypeScript. 2026. https://github.com/midspiral/LemmaScriptlink
  6. Robert Dockins; Adam Foltzer; Joe Hendrix; Brian Huffman; Dylan McNamee; Aaron Tomb. Constructing Semantic Models of Programs with the Software Analysis Workbench. Verified Software: Theories, Tools, and Experiments (VSTTE). 2016
  7. Theodoros Kasampalis; Daejun Park; Zhengyao Lin; Vikram S. Adve; Grigore Roşu. Language-Parametric Compiler Validation with Application to LLVM. Architectural Support for Programming Languages and Operating Systems (ASPLOS). 2021
  8. Ştefan Ciobâcă; Dorel Lucanu; Vlad Rusu; Grigore Roşu. A Language-Independent Proof System for Full Program Equivalence. Formal Aspects of Computing, vol. 28, no. 3, pp. 469–497. 2016
  9. Thomas Sewell; Magnus O. Myreen; Gerwin Klein. Translation Validation for a Verified OS Kernel. Programming Language Design and Implementation (PLDI). 2013
  10. Peter Lammich. Refinement for Monadic Programs. 2012. Archive of Formal Proofs, https://www.isa-afp.org/entries/Refine_Monadic.htmllink
  11. seL4 project. l4v: seL4 proofs, \textttlib/CorresWhile.thy. 2026. https://github.com/seL4/l4vlink
  12. Xavier Leroy. A Formally Verified Compiler Back-end. Journal of Automated Reasoning, vol. 43, no. 4, pp. 363–446. 2009
  13. Yiannis Charalambous; Rafael Menezes; Youcheng Sun; Lucas C. Cordeiro. Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification. 2026. arXiv:2607.10291
  14. K. Rustan M. Leino; Valentin Wüstholz. Fine-Grained Caching of Verification Results. Computer Aided Verification (CAV). 2015
  15. Cristiano Calcagno; Dino Distefano; Jérémy Dubreil; Dominik Gabi; Pieter Hooimeijer; Martino Luca; Peter O'Hearn; Irene Papakonstantinou; Jim Purbrick; Dulma Rodriguez. Moving Fast with Software Verification. NASA Formal Methods (NFM). 2015
  16. Nuno P. Lopes; Juneyoung Lee; Chung-Kil Hur; Zhengyang Liu; John Regehr. Alive2: Bounded Translation Validation for LLVM. Programming Language Design and Implementation (PLDI). 2021
  17. Benny Godlin; Ofer Strichman. Regression Verification. Design Automation Conference (DAC). 2009
  18. Dennis Felsing; Sarah Grebing; Vladimir Klebanov; Philipp Rümmer; Mattias Ulbrich. Automating Regression Verification. Automated Software Engineering (ASE). 2014
  19. Shuvendu K. Lahiri; Chris Hawblitzel; Ming Kawaguchi; Henrique Rebêlo. SymDiff: A Language-Agnostic Semantic Diff Tool for Imperative Programs. Computer Aided Verification (CAV). 2012
  20. Peter Baumann; Jürg Fässler; Markus Kiser; Zafer Öztürk. Beauty and the Beast or A Formal Semantic Description of the Control Constructs of Cobol and its Implementation. no. IFI-93.39. 1993
  21. V. A. Dasu; M. Santra; M. R. U. Rashid; A. Kumar; S. Tizpaz-Niari; G. Tan. Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust. 2026. arXiv:2605.25411v2
  22. A. Browne; E. Lee; C. Salvi. Proving LLM-Generated GPU Kernels Correct and Safe: Floating-Point Verification in Lean and VerCors. 2026. arXiv:2610.24548
  23. E. Lazaropoulos; Z. Paraskevopoulou. Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens. 2026. arXiv:2607.26306v2
  24. A. Z. H. Yang; Y. Takashima; B. Paulsen; J. Dodds; D. Kroening. VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners. 2024. arXiv:2404.18852v2
  25. S. Bhatia; J. Qiu; N. Hasabnis; S. A. Seshia; A. Cheung. Verified Code Transpilation with LLMs. Advances in Neural Information Processing Systems 37 (NeurIPS 2024). 2024
  26. A. L. Ferenczi; M. Bessonov; A. Ponnudurai; C. R. Mamillapalli; K. K. Maddula; K. K. Lingamneni. Certifying Repeatable Entry-Replay Witnesses for COBOL-to-Java Migration. 2026. arXiv:2610.27272
  27. DukeDeSouth. Fix arithmetic and control flow bugs in batch programs. 2026. Opened 2026-02-24. CardDemo pull request #32, https://github.com/aws-samples/aws-mainframe-modernization-carddemo/pull/32link
  28. R. Pan; A. R. Ibrahimzada; R. Krishna; D. Sankar; L. P. Wassi; M. Merler; B. Sobolev; R. Pavuluri; S. Sinha; R. Jabbarvand. Lost in Translation: A Study of Bugs Introduced by Large Language Models while Translating Code. Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (ICSE). 2024DOI
  29. H. F. Eniser; H. Zhang; C. David; M. Wang; M. Christakis; B. Paulsen; J. Dodds; D. Kroening. Towards Translating Real-World Code with LLMs: A Study of Translating to Rust. 2024. arXiv:2405.11514
  30. H. Chang; G. Meng; S. Xiao; K. Chen; Y. Li; K. Sun. When Code Crosses Borders: A Security-Centric Study of LLM-based Code Translation. 2025. arXiv:2509.06504v2
  31. Y. Du; Y. Zhang; M. Li. Hallucinations of Large Language Models in Cross-Language Code Translation: Phenomena and Mitigation. 2026. arXiv:2610.27868
  32. X. Wang; H. Chen; A. Cheung; Z. Jia; N. Zeldovich; M. F. Kaashoek. Undefined Behavior: What Happened to My Code?. Proceedings of the Asia-Pacific Workshop on Systems (APSys). 2012DOI
  33. X. Wang; N. Zeldovich; M. F. Kaashoek; A. Solar-Lezama. Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior. Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP). 2013DOI
  34. C. Hathhorn; C. Ellison; G. Roşu. Defining the Undefinedness of C. Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2015DOI
  35. Theorem Labs, PBC. OSS Verify: proofs and theorem statements about OSS-Fuzz fuzz targets, release 2026.10.0. 2026. Tag v2026.10.0 (commit 8f5f467); read at commit 98e995d, 2026-10-23. https://github.com/theorem-labs/oss-verify-proofslink
  36. imaami. v1.7.19 added Undefined Behavior to \textttcJSON_SetValuestring(). 2024. Opened 2024-12-25; see also pull request #924 and issue #1106. cJSON issue #919, https://github.com/DaveGamble/cJSON/issues/919link
  37. CERT Polska; Michal Majchrowicz; Marcin Wyczechowski. CVE-2026-16554: cJSON \textttprint_string_ptr() 32-bit \textttsize_t wraparound. 2026. Published 2026-07-27. https://cert.pl/en/posts/2026/07/CVE-2026-16554/link
  38. A. Chudnov; N. Collins; B. Cook; J. Dodds; B. Huffman; C. MacCárthaigh; S. Magill; E. Mertens; E. Mullen; S. Tasiran; A. Tomb; E. Westbrook. Continuous Formal Verification of Amazon s2n. Computer Aided Verification (CAV). 2018DOI
  39. N. Chong; B. Cook; K. Kallas; K. Khazem; F. R. Monteiro; D. Schwartz-Narbonne; S. Tasiran; M. Tautschnig; M. R. Tuttle. Code-Level Model Checking in the Software Development Workflow. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP). 2020DOI
  40. V. Malík; T. Vojnar. Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects. IEEE Conference on Software Testing, Verification and Validation (ICST). 2021DOI
  41. L. Sarker; A. Satter; T. Bultan. Quantitative Symbolic Patch Impact Analysis. NASA Formal Methods (NFM 2026), pp. 367–390. 2026DOI
  42. H. Tu; H. Zhao; Y. Song; M. Zafar; R. Meng; A. Roychoudhury. Agentic Verification of Software Systems. Proceedings of the ACM on Software Engineering, vol. 3, no. FSE. 2026DOI
  43. Tejasvi Singh Tomar. Proof-Carrying Modernization: Artifact and Technical Report. 2026. ZenodoDOI

Version history

  1. v1 · 23 pagesSubmitted by Tejasvi Singh TomarInitial depositCurrentNov 06, 2026