无需学习时序逻辑即可对代码进行模型检验
像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。
使用模型检验器不需要学习线性时序逻辑。Kani、CBMC和Alloy等工具允许你用普通的断言和关系约束来验证性质。你放弃了证明活性性质的能力，换来的是以小时而非周为单位的学习曲线，而对于大多数软件错误来说，这是一笔值得的交易。…
formal-methods
4 posts
不写一行证明也能证明 Rust 代码正确，但状态空间就是代价
像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。
不写一行证明也能证明 Rust 代码正确。干这活的工具叫做模型检验器，目前对 Rust 最实用的一个是 AWS 开发的 Kani。你写普通的 Rust 断言，Kani 把它们转成数学命题，对所有可能的输入进行检验。不需要定理证明器，不需要证明辅助工具，也不需要一头扎进 Coq 半年出不来。…
差分测试无需形式化证明也能奏效，但共模故障才是隐患
差分测试让你无需知道正确答案就能发现 bug。问题在于，相关的错误看起来像是达成一致。以下是如何发现盲点。
你可以在没有形式化证明的情况下信任差分测试，但前提是你必须清楚它究竟会在哪里失效。 这个弱点叫做共模故障（common-mode failure）。当某个规范的每一个实现都做出同样的错误假设时，它们会全部达成一致，而你的测试框架会将其判定为通过。N 版本编程（N-version…
测试无法证明两个函数等价。以下方法才能真正做到。
N-version programming 假设你的实现结果一致。我们来看为什么测试远远不够，SMT solvers 如何真正证明等价性，以及如何在‘足够好’和形式化验证之间取舍。
你搭建了一个 n-version 系统。同一个关键函数的三个独立实现，一个选择多数结果的 voter，以及一种你已经规避了单点故障的满足感。 但你并没有证明这些函数是等价的。你只证明了它们能编译通过。 N-version programming 的核心思想是：如果某个实现存在 bug，其他实现大概率不会有，因此…