要让 Web3 变得值得信赖，究竟需要什么？

上周的 @HeliosStaking 播客节目中，@RosuGrigore 探讨了可验证性、形式化方法以及为去中心化基础设施的未来构建可证明的系统。

↓ 以下是亮点：

从 @NASA 到区块链基础设施：@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。”

正确性变得可移植。
真相变得可编程。