2026年7月6日 无需学习时序逻辑即可对代码进行模型检验 像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 不写一行证明也能证明 Rust 代码正确，但状态空间就是代价 像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。 model-checkingrustverificationformal-methods
2026年6月15日 差分测试无需形式化证明也能奏效，但共模故障才是隐患 差分测试让你无需知道正确答案就能发现 bug。问题在于，相关的错误看起来像是达成一致。以下是如何发现盲点。 n-version-programmingdifferential-testingformal-methodstrust
2026年6月14日 测试无法证明两个函数等价。以下方法才能真正做到。 N-version programming 假设你的实现结果一致。我们来看为什么测试远远不够，SMT solvers 如何真正证明等价性，以及如何在‘足够好’和形式化验证之间取舍。 n-version-programmingequivalence-testingformal-methodsverification
