セキュリティ監査というと、多くの人は「コードを読んでバグを探す」イメージを持つと思います。
たしかにそれは王道です。ただ、SPECA が面白いのはそこから一歩ずれていて、**“このソフトは本来どうあるべきか” を書いた仕様書を起点にする**ところです。
たとえば仕様書には、
といったルールが書かれます。SPECA はそうした文章をもとに、監査用のチェックリストを組み立てるイメージです。
個人的には、これはかなり筋がいい発想だと思います。
なぜなら、実際のバグって「コードのどこかが変」というより、仕様と実装のズレとして現れることが多いからです。コードだけ見ても気づきにくいズレを、仕様から逆算してあぶり出そうとする。ここがSPECAの肝でしょう。
リポジトリの説明では、SPECA は Specification-to-Checklist Agentic Auditing Framework とされています。
ざっくり訳すと、
つまり、仕様書 → チェック項目 → 監査 という流れを、AIエージェントのように段階分割して実行する仕組みです。
README では、SPECA は自然言語の仕様から明示的で型付きの security propertiesを導き、それをもとに実装を監査すると説明されています。
ここでいう property は「満たすべき性質」のことです。たとえば「送金額は残高を超えてはいけない」みたいなルールですね。
typed というのは、性質の種類を整理して扱うという意味合いが強いと読めます。雑に「なんか怪しい」ではなく、きちんと分類して扱うわけです。
SPECA の主張は、単に「AIで脆弱性を探します」ではありません。そこが重要です。
README によると、従来の code-driven auditor は「知られているバグパターン」を探しがちなのに対し、SPECA は仕様から property を作るので、
仕様レベルの違反を見つけやすい、という立て付けになっています。
これはかなり本質的だと思います。
よくある脆弱性検出は、過去の事例を学習して「似た形」を見つけるのが得意です。でも、現実の事故は必ずしも「よくある形」では起きません。
仕様があるなら、むしろ仕様に照らして正しいかを見たほうが、未知のバグにも近づけるはずです。
もちろん、これは理想論だけではなく、実装が難しい話でもあります。
自然言語の仕様は曖昧なので、そこから監査可能な property に落とし込むには解釈が必要です。SPECA はその解釈を、段階的なパイプラインと proof-attempt reasoning で支える設計のようです。
README では、SPECA は structured proof-attempt reasoning を使うと説明されています。
要するに、実装が仕様を満たしているかを、いきなり「怪しい／怪しくない」で判定するのではなく、**“満たしていることを証明しようとする試み”**として扱うわけです。
この考え方はかなり賢いです。
セキュリティ監査では、「なぜ問題なのか」を説明できることが重要です。単にアラートを大量に出されても、現場では困ります。
SPECA は、どの仕様に対して、どの証明の試みが失敗したのかを追えるようにして、結果をトレース可能にしようとしているようです。
README には、深い分析で出た false positives（誤検知）は 3つの解釈可能な root cause に追跡できた、とあります。
ここも面白いところで、誤検知が「モデルがバグだと思ったから」で終わらず、どのパイプライン段階でズレたかまで見えるのは、研究ツールとしてかなり価値があります。
README に載っている headline results はかなり強気です。
ただし、これはリポジトリ側の主張であって、読む側はその前提で受け取るのが大事です。
これはもし事実なら、かなりインパクトがあります。
特に「cryptographic invariant violation」というのは、暗号まわりの不変条件が壊れている状態で、地味だけど危険度が高いタイプの問題です。
暗号のバグは、表面的には普通に動いて見えるのに、条件を1つ外すだけで致命傷になることがあるので、こういう発見はかなり価値があります。
precision は「出したもののうち、どれだけ当たっていたか」という指標です。
ざっくり言うと、空振りが少ないかを表します。監査ツールではかなり重要です。
見つける数だけ多くても、誤検知だらけでは現場で嫌われますからね。
README を見ると、SPECA は研究用の概念実証というだけでなく、わりとちゃんと運用できる形を目指している印象です。
おすすめの起動方法としては、TUI（テキストUI）を使う流れが案内されています。
npx speca-cli@latest doctor
npx speca-cli@latest init
npx speca-cli@latest run --target 04
そのほか、オーケストレータを直接回す方法も載っています。
中身としては、claude-code や uv、MCP setup など、AIエージェント系の開発環境を組み合わせる構成です。
ここで注目したいのは、SPECAがワンショットの診断ツールではなく、パイプライン型だという点です。
README には 01a Spec discovery、01b Subgraph、01e Property、02c Code resolution、Audit map、Review といったフェーズが並んでいます。
つまり、
という、かなり丁寧な流れです。
この「段階を刻む」設計は地味ですが、実はすごく大事です。いきなり全部をAIにやらせるより、途中結果を確認しながら進めたほうが、監査の説明責任が取りやすいからです。
README によると、詳細なドキュメントは speca.pages.dev にまとまっていて、しかも日本語がデフォルトだそうです。
これは日本語圏の読者には嬉しいポイントです。研究プロジェクトって英語だけで終わりがちですが、こういう配慮はありがたいです。
ドキュメントには、たとえば次のような項目があります。
README だけでもかなり情報量がありますが、実際に触るならドキュメントサイトが本体、という感じでしょう。
ファイル構成を見ると、かなり本格的です。
scripts/ : orchestration と各 phase の実行prompts/ : フェーズごとの worker promptbenchmarks/ : 評価用ハーネスcli/ : speca-cliwebsite/ : Docusaurus のドキュメントtests/ : pytestoutputs/ : パイプライン出力この構成からわかるのは、SPECA が単なる論文のデモではなく、ツールチェーンとして設計されていることです。
個人的には、こういう「研究っぽいけど、ちゃんと道具になっている」プロジェクトはかなり好感が持てます。アイデアだけのPoCより、ずっと実用に近いからです。
README にも明記されていますが、SPECA はresearch artifact です。
つまり、研究成果物であり、出てきた findings は candidate vulnerabilities にすぎません。
人間の監査者が確認し、必要ならベンダーや bug bounty program に報告する前に検証する必要があります。
ここはすごく大事です。
AIベースの監査は便利そうに見えますが、最終責任をAIに渡すことはできません。
むしろ、SPECA のような仕組みは「人間が監査するための下地を作る」ものと考えるのが健全だと思います。
SPECA の面白さは、単にAIでコードを読むのではなく、仕様を軸に監査の筋道を作るところにあります。
これは、セキュリティ監査の世界でかなり重要な発想です。バグはコードの外側、つまり「本来こうあるべきだった」という仕様の世界に潜んでいることが多いからです。
また、README にある実績が本当に再現可能なら、SPECA はかなり強力な研究基盤になりそうです。
特に、未知バグの発見や、誤検知の原因を説明できる設計は、実務に近い価値があります。
個人的には、SPECA は「AIで何でもやる」タイプではなく、人間の監査を強くするためにAIを使う方向に見えるのが好印象です。
こういう設計のほうが、結局は長生きするのではないかと思います。
参考: GitHub - NyxFoundation/speca: SPECA: Specification-to-Checklist Agentic Auditing Framework