AI Migrates COBOL to Java Fast — Proving It's Correct Is Hard

AI tools can now translate COBOL into compiling Java quickly, but translation accuracy is not the same as migration completeness — the survival of decades of undocumented business rules and edge-case behavior. Spot-testing the legacy and migrated systems side by side only proves the paths engineers thought to check, missing exactly the failure modes that matter: COBOL's fixed-point arithmetic silently becoming floating-point in a fresh Java implementation, then compounding across millions of accounts into an audit-level discrepancy months later.

To close that gap, a differential equivalence verifier was built around an SMT solver that formally proves whether legacy and migrated code produce identical outputs and data writes for identical inputs. When it can't prove equivalence, it returns a real, replayable counterexample instead of a confidence score. V1 deliberately covers only arithmetic and branching logic, explicitly flagging loops, file I/O, REDEFINES, and string handling as out of scope rather than silently passing them.

During development, the team caught its own bug: naive handling of sequential variable reuse could produce false equivalence verdicts, fixed through explicit per-step state tracking and witness refinement to guarantee every counterexample is genuine. Run against 14 real customer COBOL systems (~200,000 lines, 300 modules, 8,700 generated regression tests), the verifier flagged 412 semantic mismatches — discrepancies that spot-testing alone would have let ship undetected.