How it works · for developers & architects

Source in.
Safe Rust out.

Constat converts IBM i programs (ILE COBOL, RPG IV in both fixed and free format, embedded SQL, DDS and CL) into a Rust workspace that builds and runs. A real compiler, not a script and not an LLM. One pipeline, no manual rewrite, no lost logic.

The pipeline

Five stages, end to end

01

Parse

Your RPG, COBOL, DDS and CL are read by a real parser into a precise internal model. Nothing inferred, nothing guessed.

02

Lower to IR

The model is lowered through typed intermediate representations in SSA form, so every operation is explicit and accounted for.

03

Optimize

Compiler passes tidy the code the way any real compiler does, without changing what it computes.

04

Generate Rust

Idiomatic Rust comes out of a proof-backed code generator, plus a PostgreSQL schema where DB2 is in scope.

05

Verify

The output is checked for equivalence with machine-checked proofs (Lean 4) and SMT solvers (Z3, CVC5), then packaged with evidence you can audit.

Exact behavior

What it preserves

Business logic isn't approximated. The output reproduces the parts of IBM i semantics that a naive converter gets wrong:

  1. 01

    Packed and zoned decimal arithmetic, down to the last digit

  2. 02

    EBCDIC collation and character semantics

  3. 03

    REDEFINES / OCCURS record and memory layout

  4. 04

    PERFORM / GO TO control flow

  5. 05

    Platform facilities: data queues, message queues, data areas, spool, journaling

How we prove it

A verified compiler, and a clear trust boundary

Most tools check the output after the fact. Constat verifies the generator itself, then states exactly what stays trusted rather than proven.

  1. 01

    The generator is the proof

    The code generator is itself a program, written and machine-checked inside a theorem prover. The thing that emits your Rust is the very thing the proofs are about, not a separate spec.

  2. 02

    Proven at the generator, re-checked per program

    The generator's correctness is machine-checked once in the theorem prover, so the thing that writes your Rust is the thing the proofs are about. Each program is then checked end to end on your inputs. Where an operation is not yet modeled, or the emitted Rust needs an audited post-processing step, we account for it in the trust boundary rather than call it proven.

  3. 03

    Two solvers, cross-checked

    On top of that, migrated programs are checked by the Z3 and CVC5 solvers, which prove their arithmetic and data handling equivalent over the operations we model, with a second solver as an independent cross-check. Each obligation states its scope; it is not a blanket claim over every program.

  4. 04

    The trust boundary, named

    We state exactly what stays trusted rather than proven: the prover kernel, the Rust compiler over a restricted output subset, the runtime library, a short audited post-processing step applied to the emitted Rust, and a named list of assumptions about the legacy platform, each backed by a reproducible test.

Run it on iron

A public program, run on real IBM i, byte-identical

NC116A is a decimal-precision test from the public NIST COBOL-85 conformance suite, written by NIST, not by us. We transpiled it, then ran it on a live IBM i V7R5 and on the generated Rust. The output is the same, down to the byte.

NC116A NIST COBOL-85 conformance suite Rounding, truncation, scale, 18-digit multiplication. A program anyone can look up.
NC116A.cbl cobol 
*> Test 3: ROUNDED (3 dec to 2 dec)    MOVE 123.456 TO WS-DEC3    COMPUTE WS-DEC2 ROUNDED = WS-DEC3    IF WS-DEC2 = 123.46        PERFORM PASS    ELSE        PERFORM FAIL    END-IF*> Test 7: Division with decimal result    MOVE 10 TO WS-INT5    COMPUTE WS-DEC2 = WS-INT5 / 3    IF WS-DEC2 = 3.33        PERFORM PASS    ELSE        PERFORM FAIL    END-IF
NC116A.rs rust 
let ws_dec2_v40 = scaled_divide(ws_int5_v39, 0u8, v38, 0u8, 2u8);let ws_large_c_v32 = axiom_arith_mul_overflow_pic(ws_large_a_v30, ws_large_b_v31, 18u8).0;

Run both. Compare the output.

IBM i V7R5 · IBM Power (live) real hardware 
PASS NC116A-01PASS NC116A-02PASS NC116A-03PASS NC116A-04PASS NC116A-05PASS NC116A-06PASS NC116A-07PASS NC116A-08PASS NC116A-09PASS NC116A-10NC116A PRECISION TESTSPASS: 10FAIL: 00
axiom-rt · generated Rust rust 
PASS NC116A-01PASS NC116A-02PASS NC116A-03PASS NC116A-04PASS NC116A-05PASS NC116A-06PASS NC116A-07PASS NC116A-08PASS NC116A-09PASS NC116A-10NC116A PRECISION TESTSPASS: 10FAIL: 00
Same output, to the byte, from real IBM i and the generated Rust. 10 pass · 0 fail

44 public NIST programs run byte-exact on real IBM i. NC116A is one of them.

A second, independent seal: the formal proof

NC116ADecimal.lean lean 
theorem qRound_within_half (N D : ℤ)    (hN : 0 < N) (hD : 0 < D) :    2 * |qRound N D * D - N| ≤ D := by …theorem qRound_ties_away (N D : ℤ)    (hN : 0 < N) (hD : 0 < D) (htie : 2 * qRem N D = D) :    qRound N D = qTrunc N D + 1 := by …-- #print axioms qRound_within_half'…qRound_within_half' depends on axioms: [propext, Quot.sound]

The decimal core is machine-checked for every operand in the regime NC116A uses: the generated ROUNDED is the nearest scaled integer, and ties break half-away-from-zero, not the round-half-to-even a naive port would inherit from Rust. 9 theorems, 0 sorry, 0 assumptions of ours, the same standard axioms as the banking proof below.

reproduce it yourself 
axiom transpile NC116A.cbl --platform ibm-icargo run --release        # -> 10 PASS / 0 FAIL, byte-identical to IBM i

So NC116A is sealed twice, independently: the byte-identical run on real IBM i, and this all-operand proof of its decimal core. It has no database state, so there is no database bisimulation here, and the signed general case is out of scope because its tests do not exercise it. For the full DB2 migration with an all-inputs bisimulation, see the banking program below.

Fidelity, not paperwork

When the reference was wrong, we matched the real machine

NC142A is another public NIST test. Its committed "expected output" says all eight checks pass. Run it on a real IBM i V7R5 and they do not: on a MOVE of "54321" into a numeric field, the machine raises a decimal-data error and the job abends after the first test. The generated Rust abends at the same point, the same way.

The committed NIST answer key PASS ×8 says it passes
Real IBM i V7R5, live MCH1202 abend the real behavior
axiom-rt, the generated Rust MCH1202 abend matches real iron
NC142A · both, identical 
PASS NC142A-01MCH1202  Escape  sev-40  NC142A  *STMT  →  CEE9901, job abends

This is the honest test of a migration tool: reproduce the real platform, including its strictness and its failures, not a lenient reference. We match the machine byte for byte, even where the published answer key was wrong. We routed NC142A as an oracle-fidelity fix in the public corpus, not as a change to our output.

See the evidence

One program, every artifact

Not a diagram. A real sealed program walked through the whole pipeline, each stage a verbatim excerpt from the artifact it came from. Read the source, the generated Rust, the theorem, and the run-on-both result yourself.

BORROW_INT Drains open borrowings, accrues interest (principal × rate/daycount × days), and CALLs GL_POST to book a balanced double-entry journal. L2 BISIMILAR vs live IBM i V7R5
See the full artifact chain 7 stages, from source to a re-checkable dossier
  1. 01

    The program

    input

    Real COBOL. The core accrual: the daily rate, then principal times rate times days.

    borrow_int.sqlcblle cobol 
    COMPUTE-ACCR-AMOUNT.    IF DC-365       COMPUTE WS-RATE-DAILY = HV-BW-RATE / K-DAYCOUNT-365          ON SIZE ERROR SET STEP-FAIL TO TRUE EXIT PARAGRAPH    END-IF    COMPUTE WS-ACCR-RAW =            HV-BW-PRINCIPAL * WS-RATE-DAILY * WS-DAYS-TO-ACCRUE       ON SIZE ERROR          SET STEP-FAIL TO TRUE          MOVE RC-AMOUNT-OVERFLOW TO WS-OUT-RC    END-COMPUTE
    from projects-xl/bankdemo/src/borrow_int.sqlcblle:559
  2. 02

    Every line traces back

    generated

    The source map links every generated Rust function to the exact COBOL line it came from. Read the new code against the old.

    borrow_int.map.json json
    COBOLparagraphRust
    :559COMPUTE-ACCR-AMOUNT:5542 · compute_accr_amount
    :535COMPUTE-DAYS-TO-ACCRUE:5460 · compute_days_to_accrue
    :454ACCR-SINGLE-BORROW:5204 · accr_single_borrow
    from .axiom/compiler/borrow_int.map.json
  3. 03

    The generated Rust

    generated

    The same arithmetic in memory-safe Rust. Packed-decimal scale is preserved exactly, computed on 128-bit integers, never floats. The names are the compiler's SSA form; the map above ties each one back to the COMPUTE.

    borrow_int.rs rust 
    pub fn compute_accr_amount(data: &mut ProgramData) {  let v298 = scaled_divide_i128_keep(v297, 6u8, v296 as i128, 0u8, 6u8);  let v330 = axiom_arith_mul_overflow_pic_i128(v328, v329, 38u8).0;  let v332 = axiom_arith_mul_overflow_pic_i128(v330, v331 as i128, 38u8).0;  store_packed_trunc(|b| data.set_field_107(b), v332.wrapping_div(100i128), 11usize, true, 21u32, false);}
    from .axiom/…/borrow_int.rs (regenerated at build)
  4. 04

    DB2 to PostgreSQL, rule by rule

    generated

    Every DB2-ism is rewritten to PostgreSQL, and the trail is recorded statement by statement.

    borrow_int.sql-rewrites.jsonl diff
    CHAR(CURRENT DATE, ISO) TO_CHAR(CURRENT_DATE, 'YYYY-MM-DD') CHAR(x,ISO)→TO_CHAR, CURRENT-register
    DAYS(DATE(?)) - DAYS(DATE(?)) ((DATE(?) - DATE '0001-01-01')::int + 1) - … DAYS→date-arith
    from verify/dossier/sql-rewrites/borrow_int.sql-rewrites.jsonl
  5. 05

    The theorem, and its receipt

    proof-artifact + receipt

    A machine-checked bisimulation theorem: for every input, the DB2 and PostgreSQL runs produce the same state. The receipt is the verbatim kernel axiom list. It rests on one standard Lean axiom and no assumptions of ours.

    BorrowIntMasterInstance.lean lean 
    theorem borrowInt_master :    ∀ (inputs …), db2Run inputs = pgRun inputs := by …-- #print axioms borrowInt_master'…borrowInt_master' depends on axioms: [propext]
    from lean4/Axiom/Bisim/BorrowIntMasterInstance.lean:185 + …MasterInstance.axioms.txt
  6. 06

    Run on both, compared byte for byte

    verification

    The original ran on real IBM i V7R5 hardware; the Rust ran on the same inputs. The resulting business state matched, row for row.

    BORROWPF
    3/3 rows · ACCRINT 4980 / 5985 / 7500 (packed decimal, 6dp, truncated identically)
    GLJRN
    6/6 rows · double-entry balanced, sum DR = CR = 18465.00
    captured
    iron BANKDEMOXL via IBM i MCP, 2026-06-23
    from verify/bisim/oracles/borrow_int/{BORROWPF,GLJRN}.S1.json
  7. 07

    A dossier you can re-check

    receipt

    One command re-checks the whole record, end to end, so nothing can be swapped or edited after the fact.

    artifacts_checked
    21
    proof_artifacts_proven
    2
    dossier_digest
    61f950ee0cb024cd51d72ae391e268ed…
    codegen_sha256
    7ed16a32379e18ef…
    verdict
    COHERENT
    from axiom audit --json (fresh run, 2026-07-18)
What this covers, and what it does not
  • The dossier manifest seals the .axiom/* artifacts; the emitted .rs is tracked with its own hash, not yet inside the manifest.
  • The run-on-both observational equivalence lives in the bisimulation registry, not inside the per-program dossier.
  • Here the equivalence proof is the Lean bisimulation theorem; the standalone Z3/CVC5 pass is a separate, more conservative overflow analysis.

How an AI agent audits it

An AI agent drives the whole thing through the MCP server and re-checks the result itself.

agent · axiom MCP 
mcp__axiom__transpile(source, decouple=["DB2=postgresql"], audit=true)→ { rc: 0, result: { verify }, audit: { verdict: "COHERENT", artifacts_checked: 21, dossier_digest } }the agent re-verifies every SHA-256 in the manifest itself. trust nothing, check everything
transpileauditanalyzeplancodegen_provenanceverb_statusdoctor

--agent emits one JSON line; --fail-on gates the exit code (rc 3 = verification gate tripped); --progress ndjson streams phase events. A green exit cannot contradict the certificate.

What you get

A workspace you own

Readable Rust and an open PostgreSQL schema, on your infrastructure. Then the full record per program: the syntax tree, the intermediate representations, the formal proofs, the SMT formulas to re-check with your own Z3 or CVC5, and a line-by-line source-to-Rust map. Nothing is hidden between your COBOL and the Rust; your team reads the math of the migration, not just the output. No runtime lock-in, no black box.

See how we prove equivalence