形式検証を中核に据え、最もセキュアなクライアントの実現を目指す。
一般社団法人Nyx Foundation（東京都文京区、以下「Nyx」）は、Ethereumの次世代コンセンサス層「Lean Consensus」に対応する新規クライアント「Verity」の開発を開始したことをお知らせいたします。 
 
量子コンピュータの進歩により暗号技術の世代交代（PQC移行）が世界的に進む中、Ethereumはその最前線に位置しています。 
 
その中でNyxはこれまで、Ethereumエコシステムの中で実績を積み重ねてきました。
•
XMSSの一部命題をLean4言語で形式証明
•
Fusakaアップグレード監査コンテストで脆弱性報告件数 世界1位（17件）
•
Ethereum Foundation主導のzkVM「Lean Multisig」開発に参画
この経験から、私たちは自分たちの手で最もセキュアなクライアントをつくることにしました。それがVerityです。
 
Verityは形式検証（ソフトウェアの正しさを数学的に証明する手法）を中核に据え、「最もセキュアなクライアント」の実現を目指します。
 
我々のアプローチは既にEFのPQC移行チームから評価を得ており、パリで開催されたETH CCのサイドイベントにて、中心的な研究者であるJustin Drake氏の基調講演にて紹介されました。
 
暗号の転換期が、すべてのソフトウェアに到来する
量子コンピュータの進歩により、TLSやデジタル署名など現在広く使われている暗号技術が将来的に破られるリスクが現実味を帯びつつあります。これはブロックチェーンに限った話ではなく、オンラインバンキング、電子政府など、あらゆるデジタルシステムに共通する課題です。
 
日本国内でも、金融庁が2026年3月に「金融機関にかかる耐量子計算機暗号（PQC）移行実証実験」の企画競争を開始するなど、金融インフラにおけるPQC移行が動き始めています。
 
こうした暗号技術の世代交代が最も進んでいるのがEthereumです。
 
世界中で数十万のノードが稼働する大規模分散金融システムとして、耐量子暗号への移行にいち早く着手しています。オープンソースかつパブリックな環境で、高いセキュリティ要件を満たしながら暗号基盤を刷新するこの取り組みは、ブロックチェーンを超え、広くソフトウェアインフラのセキュリティを考える上で重要な先行事例となっています。
 
Nyxは、このEthereumの最前線で得られる知見を、日本の金融機関や社会インフラのセキュリティ強化に還元することを見据えています。
 
Lean Consensusが重要な理由
Ethereumが進める次世代プロトコル「Lean Consensus」は、このような脅威に正面から対処するだけでなく、これまでの技術負債を返済する壮大なプロジェクトです。 
 
Ethereum Foundationの研究者Justin Drakeが提唱する「Lean Ethereum」ビジョンの中核プロジェクトとして位置づけられ、コンセンサスクライアント（ブロックチェーンネットワークの合意形成を担うソフトウェア）の大規模な刷新を通じて、以下の技術的目標の実現を目指しています。
•
耐量子暗号への移行: 現行のBLS署名からハッシュベースの耐量子署名スキーム（XMSS）への移行を目指す
•
zkVMによる署名集約: 耐量子署名をzkVM（汎用的な計算の正しさを検証可能にする仮想マシン）上で効率的に集約する仕組み（Lean Multisig）の導入
•
高速ファイナリティ: トランザクションが確定するまでの時間を、現行の約15分から数秒へ短縮することを目標として議論中
2026年は実装フェーズとして位置づけられており、複数チームがクライアント実装に参画しています。
 
ここで重要になるのがクライアント多様性という考え方です。これはソフトウェアエンジニアリングにおける冗長性設計の原則そのものです。
 
Ethereumも異なる言語・設計思想による複数のクライアント実装を維持することで、特定の実装に依存するリスクを分散し、ネットワーク全体の耐障害性を高めています。Nyxは、この多様性に形式検証という新たな軸で貢献します。
 
Verityの設計思想
Verityは、Lean Consensusの新規独立実装として、「最もセキュアなクライアント」をコンセプトに掲げた新しいクライアント実装です。
 
他のクライアント実装との最大の違いは、形式検証を開発プロセスの中核に据えている点にあります。形式検証とは、ソフトウェアが仕様通りに動作することを数学的に証明する手法です。航空宇宙分野では飛行制御ソフトウェアの安全性保証にすでに活用されています。
 
さらに近年、AIによるコード生成が急速に普及したことで、「コードを書くこと」は容易になった一方、「そのコードが正しく動作するか」を保証する課題が浮き彫りになっています。形式検証は、この課題に対する根本的な解として、世界的に関心が高まっています。
 
Verityでは、プロトコル仕様全体をLean4言語で形式化し、仕様そのものに矛盾や欠陥がないことを数学的に証明します。この形式化された仕様を基盤とすることで、仕様と実装の乖離を防ぎます。
 
従来のソフトウェアテストが「特定の条件下でバグがないこと」を示すのに対し、形式検証は「仕様の範囲内においてバグがありえないこと」を数学的に証明する点で、セキュリティ保証のレベルが根本的に異なります。
 
Verityのロードマップ
Verityの開発は、Ethereum財団のLean Consensus Roadmapに沿って進めていきます。
 
2026年10月には第二回ケンブリッジPQ Workshopへの招待を受けており、耐量子暗号やクライアント実装に関する最新の議論に引き続き参画します。
 
Verity開発者の想い
開発責任者 津田 匠貴
Ethereumはこれまで、スケーラビリティの限界やPoSへの移行など、幾度となく大きな技術的課題に向き合ってきました。それらのソリューションは単なる延命策にとどまらず、ブロックチェーン業界全体の進化を押し進めてきました。
次の大きな課題として立ち上がっているのが量子コンピュータの脅威です。ここでも、Ethereumは他のブロックチェーンに先駆けて移行を進めています。
2025年にケンブリッジで開催されたPQ Workshopに参加した私は、この困難な課題もまた、Ethereumに集う優秀な技術者たちとともに乗り越えられると確信しました。
Verityは既にEFのPQC移行チームから高い評価を得ており、先日パリで開催されたカンファレンスにて、中心的な研究者であるJustin Drake氏に紹介されました。我々はEthereumが100年先でも安全に使えるように、その未来にコミットします。
 
Nyx Foundationについて
https://nyx.foundation
一般社団法人Nyx Foundation（所在地：東京都文京区）は、Ethereum・ブロックチェーンに特化した私設の研究機関です。形式検証とセキュリティを専門領域とし、次世代プロトコルの安全性向上に取り組んでいます。
 
すべての活動資金は寄付・研究助成金・スポンサーシップによって支えられています。Ethereum Foundationやブロックチェーン企業・大学との連携を進め、Financial Cryptography 2026 DeFi Workshopでの論文採択など、国際的な学術成果も上げています。