IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking

Dominik Blain

Translating COBOL to a modern language can change what a program computes, and LLM translations carry no guarantee of equivalence. We present IRONPROOF, which parses COBOL into an…