
PROBLEM Banks, insurance companies, governments and payroll processing services still rely on COBOL for crucial systems. Migration from COBOL is essential, but difficult and risky: it comes with a specific failure mode, namely translations that compile successfully, parse correctly, pass code review, but modify behavior silently. COBOL has semantics that modern programming languages do not have: truncation except for ROUNDED, round half-up instead of bankers, silent high-order overflow to fixed-size fields, and platform-specific byte encodings for signs and packed decimals. Such issues are undetectable in code and reveal themselves through incorrect calculations of salaries and bank statements. AI translates faster, but trustworthiness becomes the key issue: the output looks convincing and is not formally verified. SOLUTION This project replaces faith with proofs. Output of the original COBOL compiled with GnuCOBOL becomes the oracle: its output serves as a specification. - Two blind translators: two IBM Bob sessions translate the same COBOL program using different policies, idiomatic and structural, with restricted permissions to keep translators blind to each other's output. - A prosecutor: Hypothesis-driven testing generates boundary and random inputs, compares outputs of the original binary, two translations and detects any discrepancy between them, reducing disagreement to the minimal input. - A resolution loop: a scheduler sends a list of dependent programs in waves, transforms each finding into evidence-based request for fixing (the minimal input and hexdiff), sends parallel subtasks to fix each translator and verifies programs again to detect regressions. RESULTS Translation of five payroll programs revealed four silent bugs in two carefully designed and reviewed single-pass AI translations. They both incorrectly assumed IBM mainframe encodings of signs and packed decimals, which are not correct in GnuCOBOL. In one case, the bug affected only negative numbers; the prosecutor reduced the input to a single -0.01. One overflow bug had been masked by another one and emerged only after the first bug was fixed: it changed overtime payment by 400,100.00. None of them were evident from code review. After two fix rounds, five payroll programs passed on 5,044 adversarial inputs against the original COBOL and spent under 1.3 Bobcoins on total. TARGET USERS Teams responsible for modernizing COBOL applications. Users point the system at their COBOL programs and get verified translations, the per-program benchmarking, the log of runs and evidence-based fix requests for any failures. Human involvement is needed to verify the oracle, not to verify translations manually. WHAT MAKES IT UNIQUE Many AI-assisted coding projects generate code and hope. This system assumes that AI output is flawed and uses the original program as the oracle. Different translators have low chances of making the same mistake; byte-by-byte comparison detects bugs that have the same output when decoded to human-readable format. I have also verified the verification process: the oracle was hand-checked against the binary and early false positives were investigated and corrected in the harness, not in the translators.
27 Sep 2026