19
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@ryo33(平山 遼)

AIに証明を書かせてセキュアに開発する言語 Tauto をリリースしました！

19
Last updated at Posted at 2026-11-01

はじめに

AIにコードを書いてもらうのが当たり前になってきました。
でも、こんなモヤモヤはありませんか？

  • AIが書いたコード、差分を全部読むのはもう限界
  • テストは通っている。でも テストを書いていないケースは大丈夫？
  • AIに「なぜ正しいの？」と聞いても、その説明が正しいかは分からない

コードの生成が速くなるほど、確認する側の負担は増えていきます。

そこで私は、AIがコードと一緒に「このコードは必ずこの性質を満たす」という証明も書き、人間はその性質（命題）をレビューする ための言語、Tauto を作っています。

インストール方法と動かし方は、リポジトリの README の Quickstart にあります（この記事のサンプルは、記事と同時に公開した版で動作を確認しています）。

この記事では、

  1. 証明があると 何がうれしいのか
  2. テストと証明をどう使い分ける のか
  3. AI時代のエンジニアは 何を確認すべき なのか

を、具体例を交えて紹介します。

対象者

  • AIコーディング（バイブコーディング）をしていて、品質の確かめ方に悩んでいる人
  • 権限・お金・状態管理など、バグると困るコードを書いている人
  • 「証明」や「型」に興味はあるけど、難しそうで手を出していない人

たとえば、こんなバグ

ブログサービスで「投稿を削除できるのは、その投稿の作者だけ」というルールがあるとします。

ところがコードが大きくなると、

  • 画面からの削除では作者チェックをしている
  • でも APIからの削除ではチェックが抜けている

という 辻褄の合わない状態 が生まれます。
その結果、他人の投稿を勝手に消せてしまう。

これは「アクセス制御の不備」と呼ばれ、OWASP Top 10 でも筆頭に挙がる、Webアプリでよくある脆弱性です。

Tauto では、このルールを 命題 として書き、どんな入力でも成り立つことを証明 します。

// 操作する人と、投稿の関係
pub(open) inductive enum Relation {
  Author
  Stranger
}

// 投稿を削除できるかどうか
pub fn can_delete(r: Relation): Bool {
  match r {
    Author => true
    Stranger => false
  }
}

// 命題：「削除できたなら、その人は投稿の作者だった」
pub theorem delete_only_author(r: Relation, h: can_delete(r) = true): r = Author {
  match r: r = Author {
    Author => Refl
    Stranger => False::elim(false_ne_true(h))
  }
}

もし誰か（あるいはAI）が Stranger => true と書き換えたら、この証明は通らず、コンパイルエラー になります。

$ tauto check --lang ja post.taut
FAILED  delete_only_author: post.taut:19:17: 型が一致しない: `false = true` が期待されたが `can_delete(Stranger) = true` だった
  異なる部分: `false` が期待されたが `true` だった
2 ok, 1 failed, 0 incomplete; 0 skipped, 0 from imports; axioms: none

人間は証明の細部をすべて追う代わりに、delete_only_author の 結論と前提が仕様どおりか を重点的にレビューできます。

これは入門用の小さな例です（ケースが2つだけなら、テストでも網羅できます）。証明が効いてくるのは、入力や状態の組み合わせが増えて、網羅的なテストが難しくなったときです。

また、ここで証明しているのは Relation に対する判定の規則です。実際のアプリケーションでは、認証済みのユーザーと投稿の作者をサーバー側で照合して Relation を求めます。そのうえで、削除の処理を can_delete(r) = true の証明を引数に要求する関数に集約すれば、その関数を証明なしで呼ぶことを型検査で防げます。外部のコードから直接データベースを操作するような経路は、この証明の対象外です。

Tauto の特徴

  • セキュア：命題に書いた「やってはいけないこと」が起きないことを、すべての入力について証明できる
  • AIに書かせることを前提にした設計：AIにどんどん書かせても、証明の中身は機械が検査するので、人間は命題の確認に集中できる
  • 読みやすい証明：書き換えなどのステップでは、そのとき何を示しているか（ゴール）を書くので、人間にもAIにも読める
  • 実際に動く：Rust と JavaScript にコンパイルでき、Rust 経由で WebAssembly にもなる

テストと証明の使い分け

証明はテストの代わりではありません。 得意なことが違います。

テスト 証明
確かめられる範囲 書いた入力 について すべての入力 について
得意なこと 実際に動かして確かめる 「絶対に起きない」を保証する
向いている対象 外部APIとの連携、性能、UI、実行環境での動作 権限、状態遷移、計算のルール

たとえば、次のようなことは、証明だけでは確かめきれず、実際の環境でのテストや計測 が重要になります。

  • 外部のAPIやライブラリが、期待どおりに応答するか
  • 実際のブラウザやサーバーで 速度やメモリが十分か
  • そもそも 命題が仕様を正しく表しているか（具体的な入力で動かしてみると、命題のずれに気づけます）

反対に、「他人の投稿は 絶対に 消せない」のようなルールは、入力や状態の組み合わせが膨大になると、テストだけで網羅するのが難しくなります。ここが証明の出番です。

テストで「期待どおりに動くこと」を確かめ、証明で「指定した性質が必ず成り立つこと」を確かめる。

Tauto 自身も、言語の実装を数千のテストケースで確かめ、型検査の核の性質の一部は Lean で証明しています。

AIが書いたコードをどう確かめるか

Tauto では、

  1. 性質を 命題 として書く
  2. それに対応する 証明 をコードで書く

という形で正しさを表します。さらに 依存型 という仕組みで、一般的な静的型付けよりも多くのことを型で制約できます。

コンパイルが通れば、その命題が成り立つことを機械が確認したことになります。

なので、人間は証明の本文を一行一行読まなくても、「命題の立て方が正しいか」の確認に集中できます。

ただし注意点もあります。

  • 保証されるのは 命題に書いた性質だけ です。命題が仕様からずれていれば、「ずれたもの」が正しく証明されるだけです。
  • 外部ライブラリやコンパイル過程など、証明の外にある部分 は、テストなど別の方法で確かめる必要があります。
  • この保証は、証明を検査するコンパイラ自身（型検査の核）が正しく動くことと、証明で使う公理や外部コードの前提が正しいことに依存します。そのため、核はできるだけ小さく保ち、tauto check は使った公理を表示します（上の例では axioms: none）。

人間とAIに読みやすい証明

機械が検査できるからといって、証明は読まなくていい・読めなくていい、わけではありません。
証明を読んで、命題や仕様そのものの問題に気づく こともあります。

そこで Tauto では、書き換えなどのステップを使うとき、そのステップの前後のゴールを明示的に書く ことを求めます。たとえば「掛け算の交換法則」の証明の一部はこうなります。

Succ(k) => by rewrite!(mul_succ_l(k, n)): nat!(`$n * $k + $n = ${Succ(k)} * $n`) {
  ⊢ nat!(`$n * $k + $n = $n + $k * $n`) from by rewrite!(mul_comm(n, k)) {
    ⊢ nat!(`$k * $n + $n = $n + $k * $n`) from add_comm(k * n, n)
  }
}

⊢ の後ろが「今この時点で何を示そうとしているか」です。
書き換えるたびにゴールが書いてあるので、証明を上から順に追えます。

どこでも動く・速く動く

証明つきのコードも、プロダクションで動かなければ意味がありません。

動かしたい場所 コンパイル先
ブラウザ・Node.js JavaScript
サーバー・ネイティブアプリ Rust
WebAssembly Rust 経由で wasm32

既存の JavaScript や Rust のライブラリも呼び出せます（対応している型の範囲には制限があります）。

実行速度も重要です。Rust に出力する場合は、所有権と参照カウントによって GC なしでメモリを管理 します。
ただし、生成コードの性能は処理内容や実行時のオーバーヘッドに左右されるため、性能が重要な部分ではベンチマークで確認する必要があります。

どんなときに Tauto を使うといいか

全部のコードを Tauto で書く必要はありません。おすすめは 「ここが壊れたらまずい」部分 です。

  • 権限・アクセス制御：「作者以外は削除できない」「ログインしていなければ閲覧できない」
  • お金・数量の計算：「残高を超えて引き出せない」「合計が一致する」
  • 状態遷移：「支払い前には発送されない」「キャンセル済みの注文は復活しない」

AIに頼むときは、こう指示するのがコツです。

「can_delete を実装して。あわせて『削除できたなら作者だった』という定理を証明して」

そしてレビューでは、

  • 命題 が、自分の欲しい仕様を表しているか
  • 前提（h: …） が強すぎて、何も言っていない命題になっていないか
  • 命題で表しきれない部分に、テスト があるか

を見ます。証明の本文はコンパイラが検査してくれます。

これからの時代にエンジニアとしてどう成長していくか

これからはAIがコードを書く時代です。人間のエンジニアは不要になるのでしょうか？

私はそう思いません。

AIがいくら上手くコードを書けるようになっても、間違いはゼロになりません。
人間が求めた通りのものができているかを確かめる必要があります。

これから人間のエンジニアとして重要になるのは、

  • 命題をAIと一緒に立てる能力（AIへの指示）
  • 命題と証明を理解する能力（AIのアウトプットの確認）

ではないでしょうか？

もちろん全ての仕事がこの2つに集約されるわけではありません。何を作るべきかを考えること、使いやすさ、保守性、テストなど、証明だけでは解決できない課題はたくさんあります。

それでも、仕様を命題として正確に伝える能力 と AIが立てた命題を理解して確かめる能力 は、ますます重要になると考えています。

おわりに

  • 証明した部分については、AIが書いたコードの確認の中心を、差分を全部読むことから、命題をレビューすることへ移せる（証明の対象外のコードは、引き続きレビューやテストで確かめる）
  • テストと証明は役割が違い、両方を使う
  • 証明はゴールを明示して、人間にもAIにも読める形で書く

まずは、手元のコードの 「絶対にこうなってはいけない」 を一つ、命題として書いてみてください。

Tauto言語の勉強会のお知らせ

命題の立て方や証明の読み方を、実際に手を動かして学べる 勉強会を開きます！

  • 日時：11/14（土）19:00〜
  • 場所：オンライン（Discord）

参加登録は connpass からお願いします。

リポジトリはこちらです。

19
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
19
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?