Web3 真正值得信賴的條件是什麼？

上週的 @HeliosStaking 播客邀請到 @RosuGrigore，討論可驗證性、形式方法，以及為去中心化基礎設施的未來建立可證明系統的相關議題。

↓ 以下是重點整理：

從 @NASA 到 blockchain 基礎建設：@RosuGrigore 一開始將形式方法應用於 NASA 的任務關鍵系統。如今，這些工具正被用於需要可證明正確性的區塊鏈系統。

Runtime Verification 的誕生：@RosuGrigore 創立了 @rv_inc，旨在將形式方法帶入實際應用系統。起初在測試和形式方法會議中都遭到拒絕，後來「runtime verification」這個術語重新定義了這一方法——結合運行時觀察與正確性保證。如今，它已成為系統保證的一個完整分類。

為何語義重要：沒有正式語義，程式語言就像是移動的目標。Pi Squared 使用 K Framework 和 Matching Logic，以數學精確度定義並推理程式行為。

來自 @IOHK_Charles 和 @VitalikButerin 的支持：IOHK 資助了早期在 K 語言中形式化語言的工作。Vitalik 也提供資金，用於驗證 Ethereum 的 Casper 協議、Vyper、Uniswap 以及 ETH2 存款合約——這些都是該領域內最早的正式驗證努力。

無需排序的可驗證性：Pi Squared 引入一個去中心化的結算層，讓 rollups、AI 代理或交易所的聲明都能獨立且並行地進行驗證，無需全局排序。只需證明。

“沒有可驗證性，就不是 Web3。”

正確性變得可攜帶。
真相變得可程式化。