仕様は人間が読み、コードは機械が読む

GitHub Next と Microsoft Research は 10 月 21 日、Proof-Driven Development Kit を発表した。研究プレビューで、動くのは Rust だけ。そして、コーディングエージェントを回している多くのチームが避けてきた主張をしている。もう diff を一行ずつ読めないなら、読めるふりをやめて、別のものをレビューしよう、と。

その「別のもの」が仕様だ。PDD Kit のワークフローでは、人間が仕様を承認し、マシンがあらゆる入力に対して実装がそれを満たしているかを検証する。

5 つのステップと、人間が座る場所

ループはこう回る。チームはまず Chopin で機能を計画する。Chopin は GitHub Next のマルチプレイヤーなエージェント計画ツールだ。次に PDD Kit がコードについて議論し、意図を推論し、Verus で書かれた形式仕様を提案する。Verus は Rust 向けの既存のオープンソース証明言語だ。人間が承認するのは仕様であって、コードではない。そして Verus が、エージェントの生成したコードがあらゆる入力でその仕様を満たすことを証明する。完全な証明が無理な箇所では、PDD Kit はテストと computer-use エージェントによる経験的な確認にフォールバックし、出力は検証済みの pull request になる。

この反転がアイデアの全部だ。人間は要件をレビューする。検証器が実装をレビューする。Verus では、仕様は関数に事前条件と事後条件を付けて、検証器がそれを discharge しなければならない。保証は、ある具体的な意味でグリーンなテストスイートより強い。テストは入力をサンプリングするが、証明はすべての入力について量化する。

GitHub 自身の説明はこうだ。Chopin と PDD Kit を組み合わせれば、AI 生成コードを一行ずつレビューせずに本番へ出せ、コードレビューとテストだけより強い保証が得られる。ただしこれはベンダーが自社の研究プレビューを説明しているだけで、監査された結果ではない。あまり固く受け取らないほうがいい。

{{INLINE1}}

コストは消えたのではなく、場所が変わった

これを「レビュー負担は解決した」と読みたくなる。そうではない。負担はパイプラインの前段に移り、しかも過小評価しがちな形で難しくなった。

証明できるほど正確な仕様を書くのは、diff をレビューするのとは別の技能だ。曖昧な要件は証明できない仕様を生み、検証器は失敗という形でそれを教えてくれる。だから導入から数週間は「動かないツール」に見える。実際に起きているのは、要件の曖昧さがいつもより早く、もっともらしい関数で覆い隠したりしないものによって表面化している、ということだ。

誰も読まない設計ドキュメントを書き続けてきたチームにとって、これは実質的な変化だ。設計ドキュメントが構造材になる。検査される成果物がそれになるからだ。

証明が止まる場所

機能リストより重要な制約が 3 つある。

Rust だけ。Verus が検証するのは Rust で、GitHub Next によれば PDD Kit が今日動くのは Rust のみ。新しい言語を持ち込まず、コードの作り方も変えない。エージェントが TypeScript や Python を書いているなら、まだ入れられるものはない。本番コードのどれだけが Rust でないかを考えれば、これは小さな一文をまとった大きな制約だ。

仕様が表現できるものだけ。形式証明が扱えるのは、正確に述べられる性質だ。入出力の契約、不変条件、状態機械の遷移。UI の挙動、I/O の多いロジックの大半、「正しさ」が性質ではなく判断であるものは扱えない。それらは全部テストと人間のレビューというフォールバック経路に流れ、そこはまさに今日の負担がすでに置かれている場所だ。

研究プレビューで、しかも具体的な来歴がある。Chopin は GitHub Next のプロジェクトページに 2026 年 9 月付の研究プロトタイプとして載っている。GitHub Next はこれまでにもプロトタイプを出してきた。Repo Mind、Project Copernicus、SpecLang などで、いずれも一般提供には至っていない。実コードに対する最初の公開デモは GitHub Universe、10 月 28〜29 日を予定している。

正直さが宿るのはフォールバックのほう

最も多くを語る設計判断は、証明器そのものではない。証明できないコードのために明示的に第二の経路を用意したことだ。テストと computer-use エージェントによる経験的な確認に流す。

これは、ほとんどの検証ツールが認めようとしない告白だ。証明できるコードとできないコードがあり、そうでないふりをするのは二本のパイプラインを出すより悪い、とアーキテクチャの中で言っている。これを使うチームは最終的に、モジュールごとにラベルを持つことになる。証明済み、テスト済み、レビュー済み。カバレッジレポートが生み出すどの数字より、正直な信頼度の棚卸しだ。

引っかかるのは、フォールバック経路がエージェントの自己採点の場でもあることだ。UI をクリックして変更が効いたか確かめる computer-use エージェントも、やはりエージェントで、やはりサンプリングしていて、壊れたフローを「問題なし」と結論しうる。証明経路が与えるのは証明。フォールバックが与えるのは、通ってしまったデモだ。

下にある研究こそ、安心できる部分

PDD Kit はゼロから作られた検証器ではない。Verus は独立していて、すでに定着している。Microsoft Research の verus-proof-synthesis リポジトリに土台がある。LLM 駆動の 2 つのシステム、AutoVerus と VeruSAGE が Verus の証明を生成・修復し、それぞれ 150 件と 849 件の検証タスクでベンチマークされている。

PDD Kit が足しているように見えるのはパッケージングだ。この証明合成の研究ラインが、ベンチマークの演習ではなく、計画から PR までの製品ワークフローに組み込まれたのは初めてだ。「AI が自分のコードを証明できる」より小さな主張で、より信用できる。

名前が情報源によって揃っていない点にも注意したい。同じ週の報道に Proof-Driven Development Kit と Property-Driven Development Kit が両方登場し、どちらも同じ発表に紐づけられている。どちらかを選んで先に進めばいい。ブランディングを担っているのはどちらにせよ略語のほうだ。

今日できること

残る結論は「GA を待て」ではない。エージェント主体のコードベースは、証明できる領域とできない領域に分かれる、ということだ。そして設定はもうどちらがどちらかを知っているべきだ。

パーサ、状態機械、データ構造の不変条件、境界付きの算術、並行プリミティブ。ここは証明できる領域で、Verus はオープンソースで今すぐ使える。PDD Kit があってもなくても。フロントエンドの作業の大半、グルーコードの大半、そして正しさが「ユーザーが何をしたかったか」に依存するものは、そうではない。

実務的な動きは 2 つ。第一に、リポジトリ内の証明可能なモジュールにタグを付け、エージェントをそこに限って Verus に向ける。ベンダーがワークフローを出すより先に。第二に、エージェントに自分の仕事を検証するテストまで書かせるのをやめる。その配置は昔から利益相反で、グリーンのスイートの意味が薄くなった理由でもある。

居心地の悪い問い

仕様を人間が承認でき、証明をマシンが discharge できるなら、レビュアーは何のためにいるのか。コードを読むためではないし、おそらくエージェントが 412 行目に入れたバグを捕まえるためでもない。

レビュアーの仕事は、本来そうであるべきものになる。システムが何をすべきかを決め、それを言っていない仕様を突き返すこと。diff の承認ボタンを押すより難しい。そして、検証器が代わりにできない唯一の部分でもある。