こんにちは。コロンビア大学の博士課程でセキュリティ・AIを研究している Koukyosyumei です。
Claude Code や Codex などのAIエージェントによって、かなり大きなWebアプリでも短時間で実装できるようになってきました。一方で、コードを書く速度が上がるほど難しくなるのが、「このコード、本当に意図した通りに動くの？」 という問題です。
もちろん、通常はテストを書きます。しかしテストで確認できるのは、基本的には「試した入力について正しく動いた」ということだけです。たとえば、
- 他のユーザーのデータを書き換えられない
- 残高が負にならない
- 権限のないユーザーは管理操作を実行できない
- ある操作のあともデータベースの不変条件が保たれる
といった性質を、すべての入力について保証したいことがあります。そこで使えるのが、今とても注目を集めている formal verification（形式検証）です。
Lean 4とは？
この記事で使う Lean 4 は、プログラミング言語であると同時に、数学的な定理とその証明を書くためのproof assistant（定理証明支援系)です。
たとえば普通のテストでは、
1を足したら2になった
100を足したら101になった
といった具体的な例を確認します。
一方、Leanでは、
任意の自然数 n について、
n + 1 は n より大きい
というように、すべての値について成り立つ性質を命題として書き、その証明が本当に正しいかをLean自身に厳密に検査させることができます。
Webアプリに当てはめると、
どのユーザーA、ユーザーBについても、
Aが操作したことでBのデータが書き換わることはない
といった性質を定理として表現できます。
そしてLeanのkernelが証明を受理すれば、その定理が、置いた前提のもとで論理的に成り立つことを機械的に確認できます。
ただし、ここで一つ問題があります。Webアプリ本体はRustで書きたいのに、証明のためだけに同じロジックをLeanでもう一度書くと、
Rustの実装
≠
Leanで書いたモデル
というズレが起きる可能性があります。
そこで今回紹介するh5i-appでは、Rustで書いたアプリケーションロジックをAeneasを使ってLean 4へ変換し、その変換後のコードに対して証明を書くという方法を取ります。
つまり、
Rustで実装
↓
Lean 4へ自動変換
↓
性質を定理として記述
↓
Leanで証明
という流れです。
h5i-appとは？
この記事では、この仕組みをWebアプリ開発に組み込むための h5i-app を紹介します。h5i-appは、Webセキュリティ向けツール h5i の一部として開発されており、AxumをベースにしたRust Webアプリの重要なロジックをLean 4で証明できるようにする仕組みです。
ポイントは、Webアプリ全体をLeanで書き直すのではなく、普段どおりRustでアプリを書き、その重要なロジックだけをLean 4で証明するというところです。
また、h5i-appを使ったからといって、「Webアプリ全体が数学的に完全に正しい」と自動的に証明されるわけではありません。代わりに、開発者が「このアプリでは何が必ず成り立つべきか」をLeanの定理として記述し、その定理を証明します。
h5i-appの概要
h5i-appは、AxumというRustで最も人気のあるWebフレームワークに、証明可能なロジックを追加するための仕組みです。大まかな構造は次のようになります。
HTTP request
│
▼
┌──────────────┐
│ Axum / HTTP │
│ transport │
└──────┬───────┘
│
▼
┌──────────────────────┐
│ Rust kernel │
│ │
│ 認証後の判断 │
│ ビジネスロジック │
│ 状態遷移 │
└──────┬───────────────┘
│
│ Aeneas
▼
┌──────────────────────┐
│ Lean 4 │
│ │
│ theorem / proof │
└──────────────────────┘
│
▼
┌──────────────────────┐
│ storage / PostgreSQL │
└──────────────────────┘
h5i-appの中心にあるのが kernel であり、
現在の状態
+
操作を行ったユーザー
+
ユーザーが要求した操作
↓
許可 / 拒否
+
新しい状態
+
返信
という、アプリケーションの本質的な判断ロジックを書きます。このkernelはSQLやHTTPから切り離した純粋なRustとして実装され、Aeneasを用いて、RustからLean 4に変換することができます。
証明対象になるのは主に、
- アプリケーションの状態遷移
- 認可ロジック
- ビジネスロジック
- DBへ発行する書き込みの組み立て
- SnapshotとDB表現の対応
実際にプロジェクトを作ってみる
それでは簡単なアプリを作ってみましょう。ここでは、ユーザーごとに数値を1つ保存できる簡単な「電卓のメモリ」のようなアプリを考えます。
まずプロジェクトを作成します。
$ h5i app new calculator-01
$ cd calculator-01
生成されたプロジェクトは、おおよそ次のような構成になります。
calculator-01/
├── h5i-app.toml
├── kernel/
│ └── src/
│ └── lib.rs
└── proofs/
├── Theorems.lean
└── generated/
-
kernel/src/lib.rs: Rustで書くアプリケーションロジック -
proofs/Theorems.lean: 成り立ってほしい性質とその証明 -
proofs/generated/: Rustから自動生成されたLeanコード -
h5i-app.toml: 抽出・証明・mutation testingの設定
Step 1: 誰が操作しているかを定義する
まず、ユーザーを表すPrincipalを定義します。
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Principal {
pub org: u64,
pub user: u64,
}
ここでは、orgが所属するorganization、userはorganization内のユーザーIDと解釈できます。
Step 2: アプリの状態を定義する
次に、アプリケーションが保持するデータを定義します。h5i-appにはschema!という、データベースの仕様をRustやLean 4・PostgreSQLに共通して定義するためのマクロがあります。
h5i_app_schema::schema! {
mapping calc_tables for calculator_kernel,
lean "../proofs/generated/Schema.lean";
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct Snapshot {
memories: Vec<Memory>,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Memory in "memories" {
key { user: u64 }
value: u64
}
}
ここで、Snapshotは現在のデータベース状態、Memoryはユーザー一人分のデータでありテーブルの列情報を示していると考えれば十分です。
schema!からは概念的に、
pub struct Memory {
pub user: u64,
pub value: u64,
}
だけでなく、
Rust上の行操作
DBとの変換
SQL書き込み表現
Lean側のschema定義
などが生成されます。これによって、RustとLean 4におけるデータベースのモデル化を自動で行うことができます。
Step 3: kernelにアプリの判断を書く
次に、Webアプリの中心となるkernelを書きます。h5i-appにおいて、Webアプリの中心となるののがkernelであり、この部分がLean4で検証されます。
記補填的には、以下のような型を持ち、
fn transition(
actor: &Principal,
snap: &Snapshot,
cmd: &Command,
) -> Result<(WriteSet, Reply), Error>
誰が (`actor`)
+
現在どんな状態で (`snapshot`)
+
何をしようとしているか (`command`)
を受け取って、
許可するなら:
DBへの変更 (`WriteSet`)
+
ユーザーへの返信 (`Reply`)
拒否するなら:
Error
を返します。
このCalculatorの例だと、以下のように実装されます。
/// The app logic: the write (at most one memory) and the reply, or a refusal
/// that commits nothing.
pub fn transition(actor: &Principal, snap: &Snapshot, cmd: &Command) -> Result<(Option<Memory>, Reply), Error> {
match cmd {
Command::Set { value } => Ok((Some(Memory { user: actor.user, value: *value }), Reply::Value(*value))),
Command::Apply { op, arg } => {
let m = memory_of(&snap.memories, actor.user);
match compute(*op, m, *arg) {
Ok(v) => Ok((Some(Memory { user: actor.user, value: v }), Reply::Value(v))),
Err(e) => Err(e),
}
}
Command::Get => Ok((None, Reply::Value(memory_of(&snap.memories, actor.user)))),
}
}
ここで、実際の電卓の計算はcompute関数で行われています。
/// `a op b` on natural numbers below 2^64, or why it has no such result.
pub fn compute(op: Op, a: u64, b: u64) -> Result<u64, Error> {
match op {
Op::Add => {
if a > u64::MAX - b {
Err(Error::Overflow)
} else {
Ok(a + b)
}
}
Op::Sub => {
if a < b {
Err(Error::Underflow)
} else {
Ok(a - b)
}
}
Op::Mul => {
if b != 0 && a > u64::MAX / b {
Err(Error::Overflow)
} else {
Ok(a * b)
}
}
Op::Div => {
if b == 0 {
Err(Error::DivByZero)
} else {
Ok(a / b)
}
}
}
}
Step 4: kernelを実際のWebサーバーにつなぐ
kernel単体ではHTTPリクエストを受け取れません。そこでサーバー側では、kernelをKernel traitに接続します。
pub struct Calc;
impl Kernel for Calc {
type Principal = k::Principal;
type Snapshot = k::Snapshot;
type Command = k::Command;
type WriteSet = Option<k::Memory>;
type Reply = k::Reply;
type Error = k::Error;
fn tenant(actor: &k::Principal) -> TenantId {
TenantId(actor.org)
}
fn transition(
actor: &k::Principal,
snap: &k::Snapshot,
cmd: &k::Command,
) -> Result<(Option<k::Memory>, k::Reply), k::Error> {
k::transition(actor, snap, cmd)
}
fn apply(
snap: &k::Snapshot,
w: &Option<k::Memory>,
) -> k::Snapshot {
k::apply(snap, w)
}
}
一見複雑ですが、ここでやっていることはほぼ配線で、
Axum
↓
h5i-app Engine
↓
Calc::transition
↓
calculator_kernel::transition
という流れになります。
リクエストを受け取り、アプリを実行する時には、おおまかに次の処理が行われます。
HTTP request
│
▼
ユーザーを認証
│
▼
PostgreSQL transaction開始
│
▼
そのtenantの状態をSnapshotとして読み込む
│
▼
kernel::transition(actor, snapshot, command)
│
├── Err
│ └─ rollback
│
└── Ok
│
▼
writeをDBへ反映
│
▼
commit
Step 5: RustコードをLeanへ変換する
次に、実際にCalculatorで使われているkernel::transitionをそのままLean4に変換して、その性質を証明します。
まず、
h5i app extract
を実行します。このコマンドがAeneasによってRustコードをLean 4へ変換され、
proofs/generated/
以下に生成されます。
Step 6: 「正しい」とは何かを書く
ここからがformal verificationの本体です。例えば、「どんなデータベースの状態・どんなコマンドについても、transition関数がパ日記を起こさず、何らかの出力を返す」という性質を記述してみましょう。
/-- The kernel never fails: no panic, overflow or bad index, for any input. -/
theorem transition_total (a : Principal) (s : Snapshot) (c : Command) :
∃ r, transition a s c = ok r := by
have h : transition a s c ⦃ _ => True ⦄ := by
Step 7: 証明する
仕様を書いたら、次にその証明を書きます。
/-- The kernel never fails: no panic, overflow or bad index, for any input. -/
theorem transition_total (a : Principal) (s : Snapshot) (c : Command) :
∃ r, transition a s c = ok r := by
have h : transition a s c ⦃ _ => True ⦄ := by
unfold transition; cases c <;> step*
obtain ⟨r, hr, -⟩ := (WP.spec_equiv_exists _ _).1 h
exact ⟨r, hr⟩
最後に、
h5i app check
を実行します。
あるいは、Rustからの再抽出も含めて、
h5i app prove
を実行します。
証明が通れば、
Rust kernel
↓
AeneasによるLeanへの抽出
↓
指定したtheorem
↓
Lean kernelによるproof checking
まで成功したことになります。
どんな性質を証明できる？
h5i-appで特に相性が良いのは、状態遷移として表現できる性質です。
たとえば認可なら、
別organizationのユーザーは
このresourceを書き換えられない
データの整合性なら、
操作前に残高が0以上なら
操作後も0以上
ワークフローなら、
approvedになっていないrequestを
paidへ遷移させることはできない
所有権なら、
resource.ownerが変化するのは
transfer操作が成功した場合だけ
といった性質です。
まとめ
h5i-appは、「Rustで書いたWebアプリの重要なロジックをLeanで証明する」ことを可能にする、新しいフレームワークです。AIエージェントが大量のコードを書く時代には、人間がコードを一行ずつ確認するだけでは追いつかなくなるかもしれません。そのとき、「このコードを読んで、たぶん正しそう」や「単体テストに通っているので、たぶん大丈夫だろう」だけではなく、「この性質については、すべての入力に対して成立することをLeanが確認した」 と言える仕組みは、これまで以上に重要になると考えています。
証明を書く部分などは難しく感じるかもしれませんが、現在のAIの力を借りると、驚くほど簡単に様々な性質を証明することができるので、ぜひ試してみてください！