PARITY: Signed Proof for COBOL-to-Java Migrations

The problem AI has made COBOL-to-Java translation fast. It has not made it safe. Banks must prove the new Java behaves exactly like the old COBOL before cutover, and that proof is where migrations stall and fail. Equivalence testing is commonly estimated at 25-40% of a migration's cost, and failed cutovers carry real penalties: TSB's 2018 migration ended in £48.65M of regulatory fines. The hardest defects hide from ordinary tests: a rounding mode, a packed-decimal sign, a silently truncated field. Generated code can pass its own tests and still be wrong, and an LLM cannot judge its own work. Our solution PARITY is a deterministic verification gate that sits after any migrator (IBM Bob, another tool, or a human). It: 1. Parses the COBOL copybooks and record layouts and admits a behavioural contract (Bob proposes it; PARITY checks it against the parsed source). 2. Generates adversarial inputs aimed at risky constructs (COMP-3, ROUNDED, SIZE ERROR, REDEFINES, edit masks), plus human and Bob-proposed vectors, each admitted individually, with a secret holdout set drawn fresh on every run. 3. Runs the original COBOL (GnuCOBOL, guarded by a known-answer check) and the migrated Java on identical inputs. 4. Classifies every field difference with an ordered, versioned rule table: regression vs. representational. The default is regression, so it fails closed. 5. Passes six gates and issues SAFE, FLAGGED, REFUSED or INCOMPLETE, HMAC-signed, hash-chained in a tamper-evident run log, and replayable by an auditor with one command. 6. Traces each defect to the exact COBOL line and writes a defect brief (never containing holdout inputs) that Bob uses to fix the Java. No LLM is on the verdict path. This is enforced by the architecture: the pure core has no port through which a model could be called, and a test fails the build if one is imported. Users Migration engineers run `parity verify` in their loop or CI; the exit code is the verdict. Risk, audit and compliance teams run `parity replay` to prove a signed report re-derives from the exact sources and inputs. Results Bob's first migration passed its own 29/29 tests, yet on both of our sample batch programs (interest accrual and loan instalments, written to exercise the constructs where migrations fail) PARITY found real defects (35 functional regressions each), traced to exact COBOL lines. In the second program the Java printed interest that should have silently truncated, and after Bob's first fix a third, previously masked defect appeared. Bob fixed everything through PARITY's briefs; PARITY certified SAFE on fresh secret holdouts, and replay matched. It even caught a GnuCOBOL dialect bug in its own oracle. What makes it unique It is an independent verifier that grades any migrator and trusts none. It explains why a difference matters. Every verdict is signed and replayable, and it refuses rather than guesses on constructs it cannot model. Today it covers single-file batch programs; multi-file VSAM/Db2 batch and interactive CICS are the next runtime adapters on the same core.