なぜ仕様駆動にしたのか

コードだけ見るツールが見落とすもの

SPECA を作る前、最初に書いたプロトタイプは普通の「コードを見てバグを探す」スタイルでした。LLM にリポジトリを渡して「バグを見つけて」と頼む方式です。結果は誤検出率 88% でした。

このとき気づいたのは、LLM が「なんとなくあやしい」と思った箇所を列挙していたということです。コードが正しい・正しくないを判断する根拠がないため、形式だけ見て推測するしかない。根拠がないから、誤検出が増えても止められない。

一方で見逃したのは何か。Ethereum Fusaka コンテストで後から確認すると、見落とした欠陥のひとつは KZG バッチ検証の数学的不変条件の違反でした。コードの書き方だけ見ても何も怪しくない。違反しているのは「仕様書に書いてある数式が要求すること」であって、コードのパターンではありません。366 件の監査提出もこれを見逃しました。

もうひとつ事例を挙げます。あるアクセス制御の実装で、コード上はすべての関数に onlyOwner 修飾子が付いているように見えました。しかし仕様書には「初期化フェーズ中のみ、一部の操作は誰でも呼べる」という例外条件が書いてありました。コードはこの例外を実装していたのですが、その例外条件がいつ終了するかの定義が仕様と実装でズレていました。コードだけ見ていたら「修飾子が付いている = OK」で終わっていました。

仕様書を読む発想に至る流れ

コードに根拠がないなら、根拠を別の場所から持ってくればいい、というのが出発点です。

仕様書には「こういう条件のとき、こういう処理をしなければならない」という記述があります。これを形式化すれば、「証明しなければならないこと」のリストが作れます。コードが正しいかどうかを問うのではなく、「この条件が成立することを証明せよ」という問いに変える。証明できない部分 (proof gap) が出てきたとき、そこが候補検出になります。

この方向転換で何が変わったか。誤検出が出たとき、「なぜ誤検出と言えるのか」を根拠付きで説明できるようになりました。どのプロパティの、どのフェーズの判断が間違っていたか、追跡できます。

仕様駆動が効く 3 つの場面

1. 複数の実装を同じ基準で比較したい
Ethereum では同じ仕様 (EIP) に対して複数のクライアント実装が存在します。コードベースが違うと、通常のスキャンツールでは横断的な比較ができません。SPECA は仕様から作ったプロパティを共通の基準として使うため、10 種類の実装に同じ条件を当てて比較できます。Fusaka では 10 実装に対してこれを実施しました。

2. 仕様が要求する不変条件を確認したい
「この関数は常にこの事前条件が成立していなければならない」という類の要件は、コード上にコメントとして書かれていないことがほとんどです。仕様書を読めばそこに書いてある。SPECA はそれをプロパティとして取り出して検証します。

3. 誤検出の原因を分析したい
SPECA の誤検出は「信頼境界の誤解」「コード読み間違い」「仕様の誤解釈」の 3 種類に分類できました。どの種類かが分かれば、プロンプトやフィルタのどこを直せばいいかも分かります。根拠なく出てくる誤検出は、どこを直せばいいかが分からないため、改善が難しい。

仕様駆動の限界

正直に書いておきます。

仕様書が存在しないプロジェクトには使えません。コードだけがあって、ドキュメントも Issues も何もない状態では、SPECA は手がかりを見つけられません。

仕様書自体にバグがある場合も難しいです。仕様が間違っていれば、そこから作ったプロパティも間違います。「仕様どおりに実装されているか」の検証は、仕様が正しいことを前提にしています。

また、仕様の記述が曖昧すぎる場合、Phase 01e が生成するプロパティの質が下がります。「適切に処理する」「安全に実装する」のような記述からは、検証可能な条件を作りにくい。

それでも、仕様が存在して、それなりに具体的に書かれているシステムを対象にする場合、この方向は有効だと考えています。