Assumptions weaken properties18 hours agohttps://buttondown.com/hillelwayne/archive/assumptions-weaken-properties/性质/测试的强度通过逻辑蕴含来定义：更强的性质保证更弱的性质。向规约添加假设总会使结果性质变弱，形式化为：Prop ⇒ (Assumption ⇒ Prop)。假设较少的系统更健壮，适用范围更广（例如，Unicode JSON 解析器与仅支持 ASCII 的解析器相比）。依赖假设的三个常见原因：强性质无法实现、成本过高或难以直接验证。大多数假设涉及外部“外程序”因素（环境、硬件、用户输入），这使得它们的验证与系统逻辑的验证截然不同，通常也更困难。
Kani: A Model Checker for Rust22 days agohttps://arxiv.org/abs/2607.01504Kani 是一个开源的 Rust 模型检查器，它通过有界模型检查来验证安全属性和功能正确性。它将 Rust 代码从中级中间表示（MIR）编译到 CBMC 的验证引擎中，无需用户标注即可自动检查安全属性。Kani 提供了一种规范语言，具有函数合约、循环合约、量词和函数存根等特性，可将验证从有界域扩展到无界域。针对工业 Rust 项目的案例研究表明了其可行性，验证范围从恐慌自由升级到功能正确性，并发现了六个先前未知的错误。它在生产持续集成中具有可扩展性，在 Rust 标准库验证活动中，每次代码更改可验证超过 16,000 个测试套件。