So funktioniert es · für Entwickler & Architekten

Quellcode rein.
Sicheres Rust raus.

Constat überführt IBM i Programme (ILE COBOL, RPG IV in fester und freier Form, eingebettetes SQL, DDS und CL) in einen Rust-Workspace, der sich baut und läuft. Ein echter Compiler, kein Skript und kein LLM. Eine Pipeline, kein manuelles Neuschreiben, keine verlorene Logik.

Die Pipeline

Fünf Stufen, durchgängig

01

Parsen

Ihr RPG, COBOL, DDS und CL werden von einem echten Parser in ein präzises internes Modell eingelesen. Nichts abgeleitet, nichts geraten.

02

Auf IR absenken

Das Modell wird über typisierte Zwischenrepräsentationen in SSA-Form abgesenkt, sodass jede Operation explizit und erfasst ist.

03

Optimieren

Compiler-Durchläufe räumen den Code auf, wie es jeder echte Compiler tut, ohne zu ändern, was er berechnet.

04

Rust generieren

Idiomatisches Rust kommt aus einem beweisgestützten Codegenerator, dazu ein PostgreSQL-Schema, wo DB2 im Umfang liegt.

05

Verifizieren

Die Ausgabe wird mit maschinengeprüften Beweisen (Lean 4) und SMT-Solvern (Z3, CVC5) auf Äquivalenz geprüft und mit prüfbaren Nachweisen verpackt.

Exaktes Verhalten

Was erhalten bleibt

Geschäftslogik wird nicht angenähert. Die Ausgabe reproduziert genau die Teile der IBM i Semantik, die ein naiver Konverter falsch macht:

  1. 01

    Gepackte und gezonte Dezimalarithmetik, bis zur letzten Stelle

  2. 02

    EBCDIC-Sortierung und Zeichensemantik

  3. 03

    REDEFINES / OCCURS Satz- und Speicherstruktur

  4. 04

    PERFORM / GO TO Kontrollfluss

  5. 05

    Plattformdienste: Data Queues, Nachrichtenwarteschlangen, Data Areas, Spool, Journaling

So beweisen wir es

Ein verifizierter Compiler, und eine klare Vertrauensgrenze

Die meisten Werkzeuge prüfen die Ausgabe im Nachhinein. Constat verifiziert den Generator selbst und benennt dann genau, was vertraut statt bewiesen bleibt.

  1. 01

    Der Generator ist der Beweis

    Der Codegenerator ist selbst ein Programm, geschrieben und maschinengeprüft in einem Theorembeweiser. Was Ihr Rust schreibt, ist genau das, worüber die Beweise sind, keine separate Spezifikation.

  2. 02

    Am Generator bewiesen, pro Programm nachgeprüft

    Die Korrektheit des Generators wird einmal im Beweiser maschinell geprüft, sodass das, was Ihr Rust schreibt, genau das ist, worum es in den Beweisen geht. Jedes Programm wird zusätzlich mit Ihren Eingaben durchgängig geprüft. Wo eine Operation noch nicht modelliert ist oder das erzeugte Rust einen auditierten Nachbearbeitungsschritt braucht, zählen wir das zur Vertrauensgrenze, statt es als bewiesen auszugeben.

  3. 03

    Zwei Solver, unabhängig gegengeprüft

    Darüber hinaus werden migrierte Programme von den Solvern Z3 und CVC5 geprüft, die ihre Arithmetik und Datenverarbeitung über die von uns modellierten Operationen als äquivalent beweisen, mit einem zweiten Solver als unabhängiger Gegenprobe. Jede Beweispflicht nennt ihren Umfang; es ist keine pauschale Aussage über jedes Programm.

  4. 04

    Die Vertrauensgrenze, benannt

    Wir benennen genau, was vertraut statt bewiesen bleibt: den Beweiser-Kernel, den Rust-Compiler über eine eingeschränkte Ausgabe-Teilmenge, die Laufzeitbibliothek, einen kurzen auditierten Nachbearbeitungsschritt am erzeugten Rust und eine benannte Liste von Annahmen über die Legacy-Plattform, jede durch einen reproduzierbaren Test abgesichert.

Auf Eisen ausführen

Ein öffentliches Programm, auf echtem IBM i, Byte für Byte identisch

NC116A ist ein Dezimalpräzisions-Test aus der öffentlichen NIST-COBOL-85-Konformitätssuite, geschrieben von NIST, nicht von uns. Wir haben es transpiliert und dann auf einem laufenden IBM i V7R5 und auf dem erzeugten Rust ausgeführt. Die Ausgabe ist dieselbe, bis aufs Byte.

NC116A NIST COBOL-85 conformance suite Rundung, Abschneiden, Skala, 18-stellige Multiplikation. Ein Programm, das jeder nachschlagen kann.
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;

Beide ausführen. Die Ausgabe vergleichen.

IBM i V7R5 · IBM Power (live) echte 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
Dieselbe Ausgabe, bis aufs Byte, von echtem IBM i und vom erzeugten Rust. 10 bestanden · 0 fehlgeschlagen

44 öffentliche NIST-Programme laufen Byte-genau auf echtem IBM i. NC116A ist eines davon.

Ein zweiter, unabhängiger Beleg: der formale Beweis

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]

Der Dezimalkern ist für jeden Operanden im von NC116A genutzten Bereich maschinengeprüft: das erzeugte ROUNDED ist die nächste skalierte Ganzzahl, und Gleichstände brechen half-away-from-zero, nicht das round-half-to-even, das eine naive Portierung von Rust erben würde. 9 Theoreme, 0 sorry, 0 Annahmen von uns, dieselben Standard-Axiome wie der Bankbeweis unten.

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

NC116A ist also zweifach und unabhängig versiegelt: der Byte-identische Lauf auf echtem IBM i und dieser Beweis über alle Operanden seines Dezimalkerns. Es hat keinen Datenbankzustand, daher gibt es hier keine Datenbank-Bisimulation, und der allgemeine vorzeichenbehaftete Fall ist außerhalb des Rahmens, weil seine Tests ihn nicht ausüben. Für die vollständige DB2-Migration mit einer Bisimulation über alle Eingaben siehe das Bankprogramm unten.

Treue, kein Papierkram

Als die Referenz falsch lag, stimmten wir mit der echten Maschine überein

NC142A ist ein weiterer öffentlicher NIST-Test. Seine committete "erwartete Ausgabe" sagt, dass alle acht Prüfungen bestehen. Führt man ihn auf einem echten IBM i V7R5 aus, tun sie das nicht: bei einem MOVE von "54321" in ein numerisches Feld löst die Maschine einen Dezimaldatenfehler aus und der Job bricht nach dem ersten Test ab. Das erzeugte Rust bricht an derselben Stelle auf dieselbe Weise ab.

Der committete NIST-Lösungsschlüssel PASS ×8 sagt, es besteht
Echtes IBM i V7R5, live MCH1202 abend das echte Verhalten
axiom-rt, das erzeugte Rust MCH1202 abend stimmt mit echtem Eisen überein
NC142A · beide, identisch 
PASS NC142A-01MCH1202  Escape  sev-40  NC142A  *STMT  →  CEE9901, job abends

Das ist der ehrliche Test eines Migrationswerkzeugs: die echte Plattform reproduzieren, samt ihrer Strenge und ihrer Fehler, nicht eine nachsichtige Referenz. Wir stimmen mit der Maschine Byte für Byte überein, sogar dort, wo der veröffentlichte Lösungsschlüssel falsch war. Wir haben NC142A als Oracle-Treue-Korrektur im öffentlichen Korpus eingeordnet, nicht als Änderung unserer Ausgabe.

Sehen Sie die Evidenz

Ein Programm, jedes Artefakt

Kein Diagramm. Ein echtes versiegeltes Programm durch die gesamte Pipeline, jede Stufe ein wörtlicher Auszug aus dem Artefakt, aus dem sie stammt. Lesen Sie den Quellcode, das erzeugte Rust, das Theorem und das Run-on-both-Ergebnis selbst.

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
Die vollständige Artefaktkette ansehen 7 Stufen, von der Quelle bis zu einem nachprüfbaren Dossier
  1. 01

    Das Programm

    input

    Echtes COBOL. Der Kern der Abgrenzung: der Tagessatz, dann Kapital mal Satz mal Tage.

    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

    Jede Zeile ist rückführbar

    generated

    Die Source-Map verknüpft jede erzeugte Rust-Funktion mit der genauen COBOL-Zeile, aus der sie stammt. Lies den neuen Code gegen den alten.

    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

    Das erzeugte Rust

    generated

    Dieselbe Arithmetik in speichersicherem Rust. Die Skala der gepackten Dezimalzahl bleibt exakt erhalten, gerechnet auf 128-Bit-Ganzzahlen, nie mit Gleitkomma. Die Namen sind die SSA-Form des Compilers; die Map oben bindet jeden an das 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 zu PostgreSQL, Regel für Regel

    generated

    Jede DB2-Eigenheit wird nach PostgreSQL umgeschrieben, und die Spur wird Anweisung für Anweisung festgehalten.

    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

    Das Theorem und sein Beleg

    proof-artifact + receipt

    Ein maschinengeprüftes Bisimulations-Theorem: für jede Eingabe erzeugen der DB2- und der PostgreSQL-Lauf denselben Zustand. Der Beleg ist die wörtliche Kernel-Axiomliste. Er ruht auf einem einzigen Standard-Lean-Axiom und auf keiner Annahme von uns.

    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

    Auf beiden ausgeführt, Byte für Byte verglichen

    verification

    Das Original lief auf echter IBM i V7R5-Hardware; das Rust lief mit denselben Eingaben. Der resultierende Geschäftszustand stimmte überein, Zeile für Zeile.

    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

    Ein Dossier, das du erneut prüfen kannst

    receipt

    Ein einziger Befehl prüft den gesamten Datensatz von Anfang bis Ende erneut, sodass nachträglich nichts vertauscht oder verändert werden kann.

    artifacts_checked
    21
    proof_artifacts_proven
    2
    dossier_digest
    61f950ee0cb024cd51d72ae391e268ed…
    codegen_sha256
    7ed16a32379e18ef…
    verdict
    COHERENT
    from axiom audit --json (fresh run, 2026-07-18)
Was das abdeckt und was nicht
  • 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.

Wie ein KI-Agent es prüft

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.

Was Sie erhalten

Ein Workspace, der Ihnen gehört

Lesbares Rust und ein offenes PostgreSQL-Schema auf Ihrer Infrastruktur. Dazu der vollständige Datensatz pro Programm: der Syntaxbaum, die Zwischenrepräsentationen, die formalen Beweise, die SMT-Formeln zum Nachprüfen mit Ihrem eigenen Z3 oder CVC5 und eine zeilengenaue Quelle→Rust-Zuordnung. Nichts bleibt zwischen Ihrem COBOL und dem Rust verborgen; Ihr Team liest die Mathematik der Migration, nicht nur die Ausgabe. Kein Laufzeit-Lock-in, keine Blackbox.

So beweisen wir Äquivalenz