保証・監査担当者とリスク責任者向け
確かめられる
確信。
モダナイゼーションは、新しいシステムが従来と静かに異なる動作をしたときに失敗します。気づくのは本番で、監査で、あるいは法廷です。Constat は、「同じように動作する」ことを、信じるしかないものではなく、確かめられるものにするために作られています。
公開 NIST COBOL-85 プログラムが実機の IBM i V7R5 でバイト単位一致で実行されます。私たちのコーパスではなく、誰でも調べて自分で実行できるプログラムです。
両方で実行した例を見る保証の組み立て方
1つの約束ではなく、3つの仕組み
両方を実行し、比較する
元のシステムは IBM i 上で、モダナイズしたシステムは Rust で動きます。両方が同じ実際の入力を処理し、その結果のビジネス状態を直接比較します。同等性は、たまたま通ったテストから推測するのではなく、測定します。
検証済みエンジン
Rust を生成するエンジンは、機械検証された数学的証明に裏打ちされており、私たちが明示する小さな信頼境界を伴います。出力が一致することを期待するベストエフォートのツールではなく、検証済みのトランスパイラーです。
監査できる証拠
モダナイズしたすべてのプログラムには、証拠パッケージが付属します。何が、どのように生成されたか、そして元の動作と同じであることの証明です。あなたのチームと監査担当者が、自分たちの条件で検査できます。
証拠を、3つの層で
各主張が実際にどこまで証明されているか
私たちは保証を、広い順に3つの独立した層で示します。多くのツールはこれらを混ぜてしまいます。私たちは分けて示し、保証がどこで終わり、ロードマップがどこから始まるかを正確に見えるようにします。
パイプラインは IBM i 資産が書かれている言語を解析し、慣用的な Rust を生成します。これは最も広い層であり、最も弱い保証です。コードをトランスパイルすること自体は、挙動が保たれる証明ではありません。
Rust を書くエンジンは Lean 4 のカーネル内で検証され、明示的に名前を付けた小さな公理フットプリントを持ちます。結果を支えるものは、記録なしには何も仮定しません。
最も狭く最も強い層です。各プログラムを実際の IBM i ハードウェアで実行し、同じ入力でモダンな双子を走らせ、バイト単位で比較し、誰でも再検証できる資料を残します。私たちが「証明済み」と呼ぶのはこれです。
ここにある数値はすべて、記録の成果物から生成されます。出典のない数字は公開しません。
監査証跡
すべてのステップを保持するから、すべてのステップを確かめられる
モダナイゼーションは、たどり直せてはじめて信頼できます。Constat は、ソースから動作する Rust までの完全なトレイルを保持し、あなたにお渡しします。トランスパイルに関して、ブラックボックスは1つもありません。
形式的証明（Lean 4）
エンジンの正しさは、Lean 4 定理証明器で証明されています。証明は機械検証されており、結果とともに移動します。
2 つのソルバーで相互検証
モデル化した演算は SMT ソルバー Z3 が判定し、CVC5 が独立に再検査します。片方のソルバーの誤りがすり抜けません。SMT-LIB2 の式は出力でき、第三者が再検査できます。
トランスパイルトレイル
抽象構文木と、各ステージのすべての中間表現を保持します。あなたのコードがどのように Rust になったかは、隠されておらず、公開されています。
ソースと Rust の対応マップ
生成された Rust の各行は、元となった COBOL または RPG へさかのぼってリンクします。新しいコードを古いコードと突き合わせて、行単位で読めます。
各成果物に来歴を記録
すべての成果物は来歴とともに記録されます。そのため、後から何も差し替えられたり編集されたりしていないことを、第三者が確認できます。
自分で再監査する
1つのコマンドが、記録全体を端から端まで再チェックします。成果物、証明、そしてどのジェネレーターが生成したかの正確な記録です。プロセスは決定的なので、2回の実行はバイト単位で同一であり、そのまま比較できます。ここでは何も信頼を必要とせず、あなたの確認だけを必要とします。
$ axiom audit --json{ "verdict": "COHERENT" }既定で正直に
主張しないこと
同等性は、あなたの入力を使ってプログラムごとに確立します。一括の製品保証ではありません。私たちがモダナイズして検証していないプログラムは対象外であり、そのことを明言します。証明済みのレーンではなくモダナイゼーションのターゲットである場合は、そのようにラベル付けします。スコープは常に明示的です。証明そのものについても一言。コードジェネレーターは Lean カーネルで機械検証されますが、最終的な Rust は監査済みの後処理を通ります。その後処理が検証済みジェネレーターに取り込まれるまでは、それは信頼計算基盤（TCB）の一部であり、私たちは証明済みと呼ばずにそこに数えます。
私たちは IBM i（IBM Power 上で動作します）を、メインフレーム（IBM Z）と区別しています。私たちの動作検証は実際の IBM i ハードウェアに対して実行します。その他のターゲットは、各案件の中で検証します。
デューデリジェンス
必要なだけ深く
技術評価では、NDA のもとで、実際のプログラムの証明と証拠を、あなたのエンジニアと監査担当者に一つずつご説明します。最も難しい質問をお持ちください。