仕様駆動のセキュリティが重要視される背景
現代のブロックチェーンや複雑なITシステムにおいて、セキュリティの最大の脅威の一つは「仕様と実装のズレ」です。イーサリアムのような世界規模の分散型ネットワークでは、単一のソフトウェアではなく、複数の異なるクライアント（ノードソフトウェア）が稼働することでネットワークの堅牢性を保っています。
しかし、自然言語で書かれた複雑な仕様書を、各開発チームが正確に解釈し、バグなく実装することは極めて困難です。近年、Anthropic社が発表した「Claude Code Security」など、仕様に準拠しているかをAIが検証するアプローチが注目を集めています。
SPECAの機能と実績
Nyx Foundationが開発した「SPECA」は、自然言語の仕様書から自動的に検証用チェックリストを生成し、複数の実装コードと照らし合わせて脆弱性を特定するAIエージェントです。同システムは世界トップクラスの性能を誇るとされています。
SPECAはすでに、イーサリアムのセキュリティ向上において具体的な成果を上げています。2025年秋に開催されたイーサリアムの次期大型アップグレード「Fusaka」に関する公開監査コンテストでは、11種類の異なるクライアント実装から約17件の脆弱性を発見し、報告件数で世界第1位を獲得しました。さらに、バグバウンティプログラムを通じた約2件の脆弱性報告の受理や、クライアント実装への直接的な修正提案など、プロトコルセキュリティに深く貢献しています。
また、SPECAの技術的成果をまとめた論文は、AI分野のトップカンファレンスであるICLR 2026の「Agents in the wild workshop」にも採択されています（arXiv:2602.07513）。先日にはSPECAのオープンソース化が発表され、SNS上で大きな反響を呼びました。
助成金プロジェクトの概要と今後の展開
今回のイーサリアム財団からの助成金を受け、Nyx Foundationは5月から4ヶ月間にわたり、以下のマイルストーンに取り組むとしています。
-
SPECAのワークフロー統合とツール公開: イーサリアムの仕様書（Execution/Consensus specs）を自動で読み込み、クライアント実装との不整合を検出するプロトタイプ（CLI/API）を開発します。これにより、GitHubのCI/CDパイプラインなどにSPECAを組み込み、開発の初期段階で仕様違反を検知できる体制を構築する計画です。
-
Lean形式検証との融合による高度な安全性担保: Nyx Foundationが先行して取り組む「Lean言語を用いた形式検証の自動化」技術とSPECAを統合します。SPECAが生成したセキュリティ要件を、数学的な証明に基づくLean 4の形式仕様へと自動変換するパイプラインを構築し、進化し続けるイーサリアムの仕様に対しても、より厳密でスケーラブルな安全性検証を実現することを目指します。
-
継続的な脆弱性発見と学術的貢献: 助成金期間中も継続してクライアントの監査を行い、発見された脆弱性の報告と修正パッチの提供を行うとしています。また、これらの成果をまとめたフルペーパーを、セキュリティ分野のトップカンファレンスへ投稿する予定です。
Nyx Foundationは、AIエージェントと形式検証の技術を組み合わせることで、イーサリアムをはじめとするあらゆるITシステムの脆弱性発見を自動化し、誰もが安心して利用できるデジタル社会の基盤構築に貢献していくとしています。このツールはオープンソースで公開され、一般利用を目指す方針です。
Nyx Foundationについて
一般社団法人Nyx Foundation（所在地：東京都文京区）は、Ethereum・ブロックチェーンに特化した研究機関です。形式検証とセキュリティを専門領域とし、次世代プロトコルの安全性向上に取り組んでいます。すべての活動資金は寄付、研究助成金、スポンサーシップによって支えられており、Ethereum Foundationやブロックチェーン企業・大学との連携も進め、国際的な学術成果も上げています。
ソース: 一般社団法人Nyx Foundationからの情報
URL: https://nyx.foundation/