5 posts
Cleanroom software engineering 承诺通过 mathematical verification 而非 debugging 实现零缺陷增量。我们查看 IBM 的实际项目数据，看看这一说法是否成立。
1980 年代软件行业的平均水平是每千行代码 30 到 60 个缺陷。IBM 的 Cleanroom 团队交付了一个 2 万行的编译器增量，在测试中发现了 53 个缺陷。也就是每 KLOC 2.6 个。一些 1 万行的独立增量在进入系统测试时，没有发现任何缺陷。 最离奇的部分？程序员被禁止运行自己的代码。…
AutoVerus利用LLM智能体网络为Rust代码生成Verus正确性证明，通过由SMT求解器反馈驱动的生成-修复-消除循环，自动化超过90%的证明义务。
形式化验证中最困难的部分从来不是验证器本身，而是编写证明。 给一位资深Rust工程师Verus——微软研究院开发的基于SMT的验证器——他可以在一个下午内为函数添加前置条件和后置条件注释。然后验证器会以机械确定性告诉他，该函数是否对所有可能的输入满足这些契约。这部分令人满意。…
像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。
使用模型检验器不需要学习线性时序逻辑。Kani、CBMC和Alloy等工具允许你用普通的断言和关系约束来验证性质。你放弃了证明活性性质的能力，换来的是以小时而非周为单位的学习曲线，而对于大多数软件错误来说，这是一笔值得的交易。…
像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。
不写一行证明也能证明 Rust 代码正确。干这活的工具叫做模型检验器，目前对 Rust 最实用的一个是 AWS 开发的 Kani。你写普通的 Rust 断言，Kani 把它们转成数学命题，对所有可能的输入进行检验。不需要定理证明器，不需要证明辅助工具，也不需要一头扎进 Coq 半年出不来。…
N-version programming 假设你的实现结果一致。我们来看为什么测试远远不够，SMT solvers 如何真正证明等价性，以及如何在‘足够好’和形式化验证之间取舍。
你搭建了一个 n-version 系统。同一个关键函数的三个独立实现，一个选择多数结果的 voter，以及一种你已经规避了单点故障的满足感。 但你并没有证明这些函数是等价的。你只证明了它们能编译通过。 N-version programming 的核心思想是：如果某个实现存在 bug，其他实现大概率不会有，因此…