Web3を信頼できるものにするには、実際に何が必要なのか？

先週の @HeliosStaking ポッドキャストでは、@RosuGrigore が verifiability（検証性）、formal methods（形式手法）、そして分散型インフラの未来に向けた証明可能なシステムの構築について語りました。

↓ ここに特に印象的だったポイントをまとめました：

NASAからブロックチェーンインフラへ：@RosuGrigore は、NASAのミッションクリティカルなシステムにformal methodsを適用することからキャリアをスタートさせました。現在では、これらのツールは証明可能な正確性を求めるブロックチェーンに応用されています。

Runtime Verificationの誕生：@RosuGrigore は @rv_inc を設立し、formal methodsを実世界のシステムに導入しました。当初はテストやformal methodsの会議から拒否されていましたが、「runtime verification（ランタイム検証）」という用語が登場し、実行時の観察と正確性保証を融合させるアプローチに再定義されました。これにより、システム保証のカテゴリー全体が形成されました。

セマンティクスの重要性：formal semantics（形式的意味論）がなければ、プログラミング言語は動く標的となります。Pi Squaredは、K FrameworkとMatching Logicを用いて、プログラムの挙動を数学的に定義し、推論しています。

@IOHK_Charles と @VitalikButerin の支援：IOHKはK言語の正式化に関する初期研究に資金提供し、VitalikはEthereumのCasperプロトコル、Vyper、Uniswap、ETH2のdeposit contractなどの検証に対して助成金を提供しました。これらは、ブロックチェーン分野における最初期のformal verificationの取り組みです。

順序付けなしの検証性：Pi Squaredは、rollups、AIエージェント、取引所からのclaim（主張）を独立かつ並列に検証できる分散型の決済層を導入しています。グローバルな順序付けは不要です。必要なのは証拠だけ。

「検証性なしにWeb3は成り立たない。」

正確性は持ち運び可能に。
真実はプログラム可能になる。