仕組み・開発者とアーキテクト向け

ソースを入力。
安全な Rust を出力。

Constat は IBM i プログラム（ILE COBOL、固定形式とフリー形式の RPG IV、埋め込み SQL、DDS、CL）を、ビルドして動作する Rust ワークスペースへ変換します。スクリプトでも LLM でもない、本物のコンパイラーです。1つのパイプラインで、手作業の書き換えなし、ロジックの喪失なし。

パイプライン

端から端まで、5つのステージ

01

解析

あなたの RPG、COBOL、DDS、CL を、本物のパーサーで正確な内部モデルへ読み込みます。推測も、憶測もありません。

02

IR へ変換

モデルを、SSA 形式の型付き中間表現へ落とし込み、すべての演算を明示的に扱います。

03

最適化

コンパイラーのパスが、計算内容を変えずに、本物のコンパイラーと同じようにコードを整えます。

04

Rust 生成

証明に裏打ちされたコードジェネレーターから、慣用的な Rust が出力されます。DB2 が対象範囲にあれば、PostgreSQL スキーマも生成されます。

05

検証

出力は、機械検証された証明（Lean 4）と SMT ソルバー（Z3、CVC5）で同等性を確認され、監査できる証拠とともにパッケージ化されます。

正確な動作

何を保持するか

ビジネスロジックは近似されません。出力は、素朴な変換ツールが誤る IBM i のセマンティクスの部分を、正確に再現します。

  1. 01

    パック10進数とゾーン10進数の演算を、最後の桁まで

  2. 02

    EBCDIC の照合順序と文字セマンティクス

  3. 03

    REDEFINES / OCCURS のレコードとメモリーレイアウト

  4. 04

    PERFORM / GO TO の制御フロー

  5. 05

    プラットフォーム機能：データキュー、メッセージキュー、データエリア、スプール、ジャーナリング

証明の方法

検証されたコンパイラーと、明確な信頼境界

多くのツールは出力を事後にチェックします。Constat はジェネレーター自体を検証し、そのうえで、何が証明ではなく信頼にとどまるかを正確に示します。

  1. 01

    ジェネレーターそのものが証明

    コードジェネレーター自体が、定理証明器の中で書かれ機械検証されたプログラムです。あなたの Rust を書くもの自体が証明の対象であり、別個の仕様ではありません。

  2. 02

    ジェネレーターで証明し、プログラムごとに再検査

    ジェネレーターの正しさは証明器の中で一度だけ機械検証されます。つまり、あなたの Rust を書くもの自体が証明の対象です。各プログラムはさらに、あなたの入力で端から端まで検査されます。ある演算がまだモデル化されていない場合や、生成された Rust に監査済みの後処理が必要な場合は、証明済みと呼ばずに信頼境界に数えます。

  3. 03

    2つのソルバー、独立した相互チェック

    さらに、移行したプログラムは Z3 と CVC5 のソルバーで検査され、私たちがモデル化した演算の範囲で、その演算とデータ処理が同等であることを証明します。2つ目のソルバーが独立した相互チェックになります。各証明義務はその範囲を明示し、すべてのプログラムに対する一括の保証ではありません。

  4. 04

    信頼境界を、名指しで

    何が証明ではなく信頼にとどまるかを正確に示します。証明器のカーネル、限定された出力サブセットに対する Rust コンパイラー、ランタイムライブラリ、生成された Rust に適用される短い監査済みの後処理、そしてレガシープラットフォームの挙動に関する名前付きの前提（それぞれ再現可能なテストで裏づけ）です。

実機で走らせる

公開プログラムを 実機の IBM i で、バイト単位で一致

NC116A は、公開されている NIST COBOL-85 適合性スイートの 10 進精度テストで、私たちではなく NIST が書いたものです。これをトランスパイルし、稼働中の IBM i V7R5 と生成された Rust の両方で実行しました。出力はバイト単位まで同一です。

NC116A NIST COBOL-85 conformance suite 丸め、切り捨て、スケール、18 桁の乗算。誰でも調べられるプログラムです。
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;

両方を実行し、出力を比較。

IBM i V7R5 · IBM Power (live) 実機 
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
実機の IBM i と生成された Rust から、バイト単位まで同じ出力。 10 PASS · 0 FAIL

44個の公開 NIST プログラムが実機の IBM i でバイト単位一致で実行されます。NC116A はその一つです。

二つ目の独立した封印：形式的証明

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]

10 進の中核は、NC116A が用いる範囲のすべての被演算子について機械検証されています。生成された ROUNDED は最も近いスケール整数であり、同点は round-half-to-even（素朴な移植が Rust から受け継ぐもの）ではなく half-away-from-zero で決まります。9 つの定理、sorry 0、私たちの仮定 0、下の銀行証明と同じ標準公理です。

自分で再現する 
axiom transpile NC116A.cbl --platform ibm-icargo run --release        # -> 10 PASS / 0 FAIL, byte-identical to IBM i

つまり NC116A は、独立に二重で封印されています。実機の IBM i でのバイト単位で同一の実行と、その 10 進中核の全被演算子に対するこの証明です。データベースの状態を持たないため、ここにデータベース双模倣はなく、符号付きの一般ケースはテストが行使しないため対象外です。全入力に対する双模倣を伴う完全な DB2 移行については、下の銀行プログラムをご覧ください。

書類ではなく、忠実さ

参照が間違っていたとき、私たちは 実機 と一致した

NC142A も公開されている NIST テストです。コミットされた「期待出力」は 8 つの検査すべてが合格すると述べています。しかし実機の IBM i V7R5 で実行すると合格しません。数値項目への "54321" の MOVE で、マシンは 10 進データエラーを発生させ、最初のテストの後にジョブがアベンドします。生成された Rust も、同じ場所で、同じようにアベンドします。

コミットされた NIST の模範解答 PASS ×8 合格と主張
実機の IBM i V7R5 MCH1202 abend 実際の挙動
axiom-rt、生成された Rust MCH1202 abend 実機と一致
NC142A · 両方、同一 
PASS NC142A-01MCH1202  Escape  sev-40  NC142A  *STMT  →  CEE9901, job abends

これが移行ツールの誠実な試金石です。寛容な参照ではなく、実際のプラットフォームを、その厳格さと失敗も含めて再現すること。公開された模範解答が間違っていた場所でさえ、私たちはマシンとバイト単位で一致します。NC142A は、私たちの出力の変更ではなく、公開コーパスにおけるオラクル忠実性の修正として扱いました。

証拠を見る

1つのプログラム、すべての成果物

図ではありません。実際に封印された1つのプログラムをパイプライン全体に通し、各段階はその成果物からの逐語的な抜粋です。ソース、生成された Rust、定理、そして run-on-both の結果を、ご自身で読めます。

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
完全な成果物チェーンを見る 7 段階、ソースから再検証できるドシエまで
  1. 01

    プログラム

    input

    本物の COBOL。発生計算の核心は、日次レート、そして元本 × レート × 日数です。

    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

    すべての行に出所がある

    generated

    ソースマップは、生成された各 Rust 関数を、その元となった正確な COBOL 行に結び付けます。新しいコードを古いコードと照らし合わせて読めます。

    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

    生成された Rust

    generated

    同じ演算を、メモリ安全な Rust で。パックされた 10 進数のスケールは正確に保たれ、浮動小数点ではなく 128 ビット整数で計算されます。名前はコンパイラの SSA 形式で、上のマップが各名前を 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 から PostgreSQL へ、ルールごとに

    generated

    DB2 固有の表現はすべて PostgreSQL に書き換えられ、その経路が文ごとに記録されます。

    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

    定理と、その受領書

    proof-artifact + receipt

    機械検証された双模倣定理です。あらゆる入力に対して、DB2 と PostgreSQL の実行が同じ状態を生みます。受領書はカーネルの公理リストそのものです。標準的な Lean の公理ひとつだけに依拠し、私たち独自の仮定はありません。

    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

    両方で実行し、バイト単位で比較

    verification

    オリジナルは実機の IBM i V7R5 で実行され、Rust は同じ入力で実行されました。結果として得られた業務状態は、行ごとに一致しました。

    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

    再検証できるドシエ

    receipt

    ひとつのコマンドで記録全体を端から端まで再検証します。後から何かを差し替えたり編集したりはできません。

    artifacts_checked
    21
    proof_artifacts_proven
    2
    dossier_digest
    61f950ee0cb024cd51d72ae391e268ed…
    codegen_sha256
    7ed16a32379e18ef…
    verdict
    COHERENT
    from axiom audit --json (fresh run, 2026-07-18)
これがカバーする範囲と、しない範囲
  • 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.

AI エージェントはどう監査するか

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.

得られるもの

自社が所有するワークスペース

読みやすい Rust と、オープンな PostgreSQL スキーマを自社のインフラ上で。さらに、プログラムごとに完全な記録が付きます。構文木、中間表現、形式的証明、自分の Z3 や CVC5 で再チェックできる SMT 式、そして行単位のソースから Rust への対応マップです。あなたの COBOL と Rust の間に、隠れているものはありません。あなたのチームは、出力だけでなく移行の数学を読めます。ランタイムのロックインも、ブラックボックスもありません。

同等性の証明方法を見る