ヴィタリック、「形式検証」活用を解説。AI時代のEthereum安全性向上で

AI時代の防御技術として「形式検証」に注目

イーサリアム（Ethereum）共同創設者ヴィタリック・ブテリン（Vitalik Buterin）氏が、ソフトウェアの正しさを数学的に証明する「形式検証（Formal Verification）」について解説するブログ記事を5月18日に公開した。 　

同記事のタイトルは「A shallow dive into formal verification（形式検証の基礎を理解する）」だ。ブテリン氏は、AIによるコード生成や脆弱性発見能力が急速に向上する中、暗号資産（仮想通貨）や暗号技術基盤の安全性をどのように担保するかが重要な課題になっているとの認識を示している。

ブテリン氏は記事冒頭で、イーサリアム研究開発コミュニティなどでの、「リーン（Lean）」と呼ばれるプログラミング言語を用いた形式検証が急速な広がりについて説明して…