NyxのAI監査システム「SPECA」、イーサリアム財団の研究助成金に採択

仕様書から「守るべき条件」を抽出するSPECA

イーサリアム(Ethereum)に特化した国内研究機関「ニックス・ファウンデーション(Nyx Foundation:以下、Nyx)」独自開発の監査システムが、イーサリアム財団(Ethereum Foundation)の研究助成金に採択されたことが5月7日に発表された。

同システムは「SPECA(Specification-to-Checklist Agentic Auditing)」と呼ばれるAIエージェント型の監査システムだ。

今回の採択は、イーサリアム財団のプロトコルセキュリティ研究チームが公募した「大規模言語モデル(LLMs)をイーサリアムのプロトコルセキュリティ研究へ統合する取り組み(Integrating Large Language Models (LLMs) into Ethereum Protocol Security Research)」に対応するものだ。同公募では、イーサリアムの仕様変更をAIで解析し、仕様書と各クライアント実装の不整合を検出する仕組みの研究開発が求められていた。

Nyxによると、こうした研究が重視される背景には、イーサリアム特有の開発構造があるという。イーサリアムでは、単一の公式ソフトウェアがネットワークを運営しているわけではなく、複数の開発チームがそれぞれ独立してクライアントソフトウェアを実装している。そのため、各チームは共通の仕様書をもとに互換性のあるソフトウェアを開発する必要があるとのことだ。

一方で、仕様は厳密な数式や機械可読形式だけで定義されているわけではなく、人間による解釈を前提とした記述も多い。Nyxは、同じ仕様書を参照していても、細かな実装方法や例外処理の解釈が各チームで異なった場合、ネットワーク障害や脆弱性につながる可能性があると説明している。

例えば、あるクライアントでは有効と判断された取引が、別のクライアントでは無効と判断された場合、ブロック生成や検証結果に不一致が発生し、チェーン分岐などの問題につながる可能性があるとのこと。

Nyxは、こうした問題に対応するためにSPECAを開発したという。発表によると、SPECAは実装コードと仕様書を照合する「仕様駆動(Specification-driven)」型の監査システムだ。コード内の既知パターンを検出する従来型ツールとは異なり、自然言語で書かれた仕様書から「守るべき条件」を抽出したうえで、AIが実装コード側でその条件が満たされているかを段階的に検証する仕組みを採用している。

Nyxは、SPECAについて、イーサリアムの大型アップグレード「フサカ(Fusaka)」に向けて2025年9〜10月に実施された監査コンテストを用いた検証で、既知脆弱性15件すべてを検出し、さらに追加バグ4件を独自発見したとしている。なおフサカ自体は、その後2025年12月にメインネットへ実装された。また同団体は、C/C++プロジェクト向けベンチマーク「レポオウディット(RepoAudit)」でも、他のAI監査システムと比較して高水準の精度を達成し、新たな脆弱性候補12件を報告したと説明している。

今回のイーサリアム財団からの助成金採択を受け、Nyxは今後4ヶ月間にわたり、イーサリアム仕様書を自動解析し、クライアント実装との不整合を検出するCLI/APIツールの開発を進める計画だ。

同ツールは、ギットハブ(GitHub)上の開発フローへの統合も想定されており、開発初期段階で仕様違反を検出する仕組みを目指すという。

さらにNyxは、形式検証向け言語「リーン4(Lean 4)」を活用した自動検証技術との統合も進める方針を示している。

なお、近年では、AIを活用したセキュリティ監査の取り組みが拡大している。今年2月にはアンソロピック(Anthropic)が、AIがコードベースを解析し脆弱性を検出・修正提案する「クロードコードセキュリティ(Claude Code Security)」を発表している。

Nyxは今回の研究について、AIエージェントと形式検証を組み合わせることで、イーサリアムを含むソフトウェア監査の自動化を進める取り組みだと説明している。

参考:プレスリリース論文
画像:PIXTA

関連ニュース

関連するキーワード

この記事の著者・インタビューイ

渡邉洋輔

「あたらしい経済」編集部 記者 ブロックチェーンおよびデジタル資産分野を専門とし情報発信を行っている。オンチェーンデータや流動性構造など、市場設計の観点からのリサーチにも取り組んでいる。