SPECA：仕様書からバグを見つけるAIセキュリティ監査フレームワークOSS公開

概要¶

Nyx Foundation が SPECA（Specification-to-Checklist Agentic Auditing Framework） をOSS公開した。コードではなく「仕様書」からバグを見つけるAIエージェント型セキュリティ監査フレームワーク。MITライセンス。

GitHub: https://github.com/NyxFoundation/speca

詳細¶

従来のコード駆動型ツールとの違い¶

従来のセキュリティ監査ツールはコードを直接解析するが、SPECAは仕様書（EIP、コンセンサス仕様書など）を起点にする。

処理フロー：

仕様書（自然言語）
  → 型付きセキュリティプロパティを抽出
     （Invariant / Precondition / Postcondition / Assumption）
  → STRIDE + CWE Top 25 で脅威モデル整理
  → proof-attempt reasoning で実装に問いかける
     「このプロパティが成立することを証明してみろ」
  → 仕様と実装のギャップを検出

3つの価値¶

仕様レベルでしか表現できない脆弱性の検出: コードパターンだけでは拾えない仕様由来のバグを発見
複数実装間の横断比較: 同じプロパティ辞書で複数実装を一律評価
偽陽性の原因分析: 根拠を完全トレースし、偽陽性を根本原因ごとに分解

技術スタック¶

Claude Code CLI + MCPサーバーで動作
対応言語: Go / Rust / Nim / TypeScript / C（マルチ言語）
GitHub Actions で全フェーズ自動実行可能
並列化・リジューム・予算制御・circuit breaker 完備の Python オーケストレータ
全ステップの出力を JSON で構造化（監査可能・解釈可能）

使い方¶

# repo をクローンしてコマンド1つで実行
uv run python3 scripts/run_phase.py --target 04 --workers 4 --max-concurrent 64

設定ファイル： - BUG_BOUNTY_SCOPE.json : バグバウンティのスコープ・ルールを記載 - TARGET_INFO.json : 監査対象の情報を記載

実績¶

対象	結果
Intmax ZK実装	脆弱性発見
SP1 zkVM実装	脆弱性発見
Ethereumクライアント実装 20件以上	脆弱性発見
Sherlock Ethereum Fusaka 監査コンテスト	既知15件すべて検出 + 新規4件独立発見
RepoAudit C/C++ ベンチマーク	最高水準精度 + 新規候補12件報告

なぜ重要か / いつ使うか¶

ブロックチェーン・DeFi のセキュリティ監査: EIPや仕様書ベースのプロジェクトで威力を発揮
バグバウンティ: BUG_BOUNTY_SCOPE.json に対象を設定するだけで実践的な脆弱性探索が可能
複数実装の一括評価: 同一仕様から派生した複数実装を横断比較できる

公開の背景として、企業のセキュリティ部門でもClaudeやOpenAIを活用したツールが現実的な選択肢になってきたタイミングで、「防御側・ホワイトハッカー側が先に活用できる環境を作る」という判断でOSS化された。ライセンスはMITなので自由に改造・拡張・フォーク可能。