全栈形式化验证成为新趋势，AWS等公司推动软硬件验证全覆盖

最近有几项关于软件和硬件形式验证的公告，既有使用AI进行验证的，也有针对AI系统的：

这些公告的共同点是都致力于实现全栈形式化，要么覆盖整个软件栈，要么覆盖软硬件的组合。过去，验证只针对软件的一小部分核心，或针对实际软件的简化模型。

作为参考，AWS的访问控制语言Cedar有一个运行在生产环境中的Rust实现，以及一个参考实现——最初用Dafny编写，后来改用Lean——该参考实现经过了正确性验证。

一种方法是完全用Lean开发Cedar，编译为C，并将生成的C代码部署到生产环境。除了形式化模型之外，我们还会用Lean编写一个经过优化且功能完整的实现（更仔细地处理错误和消息，为各种格式提供解析器等），然后证明两者等价。这种方法的一个关键好处是，我们可以对部署代码与模型之间的等价性进行形式验证，而不仅仅是测试。但用Lean编写生产应用并部署其生成的C代码存在显著的缺点。Lean是一门新的编程语言，因此开发者群体有限，也缺少主流语言中可用的实用库。调试故障可能需要单步跟踪生成的C代码并将其映射回Lean源码，这要求具备C和Lean的专业知识。如果故障是由手写代码与Lean生成的C代码之间的交互引起的，调试起来可能尤其困难。此外，C是一门内存不安全的语言，因此Lean编译器中的bug可能导致安全问题。 —— How We Built Cedar: A Verification-Guided Approach（2024年4月）

在过去一年里，我一直在谈论liquid types，将其作为我个人偏好的程序验证方案。Liquid types是值依赖类型的一种受限形式，其约束可以使用SMT求解器自动检查。这是我的理想平衡点：你能获得表达性类型系统的诸多好处，可以表达typestate等属性——例如在对象处于错误状态时阻止方法被调用，比如在close()之后调用read()。而且代价要低得多，特别是因为你不需要编写证明：SMT求解器会处理好这些。1

直到几个月前，这种权衡还非常重要：世界上很少有人具备专业知识和时间来承担大型开源项目的完整验证（向seL4团队致敬！）。前沿模型在生成证明方面超越人类的能力已经侵蚀了这道护城河，而补贴的token价格使得现在是进行这些实验的完美时机。我必须承认，我最近幻灯片中使用的上图可能不再有意义了。当token价格上涨时——可能反映其实际成本——它可能再次变得相关，届时我们需要节省时间和token，同时仍然验证我们关心的属性，而不必一直深入到机器码级别。2

目前，如果我们追求全栈验证，可能需要用一种验证优先的语言来编写代码，比如Lean。Dafny和我自己的aeon可以作为候选，但Lean的函数式编程模型以及该项目获得的大量资金使其成为理想候选。Rocq的爱好者可能不喜欢这一点，但在现实世界中，将可执行代码提取到OCaml并不是一个如此显著的优势。

但我们需要Lean变得更好。首先，我们需要更快的类型检查和好得多的优化器。这正是Bend2从一开始就做对的部分——下一门主流语言将同时需要验证和速度。

使用证明组合子，你可以用LiquidHaskell达到与Lean相同的表达能力。反过来，你也可以只用Lean的grind策略来达到与liquid types相同的低成本。在这里，我是按照每种工具的典型用法来考虑的。↩

我确信人们不会阅读源代码，而是会依赖新技术来建立对生成代码的信心。↩