6 posts
AutoVerus利用LLM智能体网络为Rust代码生成Verus正确性证明，通过由SMT求解器反馈驱动的生成-修复-消除循环，自动化超过90%的证明义务。
形式化验证中最困难的部分从来不是验证器本身，而是编写证明。 给一位资深Rust工程师Verus——微软研究院开发的基于SMT的验证器——他可以在一个下午内为函数添加前置条件和后置条件注释。然后验证器会以机械确定性告诉他，该函数是否对所有可能的输入满足这些契约。这部分令人满意。…
大语言模型能写出质量惊人的Rust代码，但当你要求形式化证明时，它们会幻觉出不变量，并编造出没有任何验证器接受的语法。本文介绍它们真正做对了什么、在哪里崩溃，以及如何善用它们。
LLM能写出可以编译甚至通过的Rust代码。但它们目前还无法可靠地写出形式化证明，来证实代码对所有可能的输入都是正确的。…
model checking 如何在数秒内碾压你在生产环境跑几天才能发现 concurrency bug 的做法，以及如何把它用在自己的代码上。
在生产环境里等 race condition 冒出来，那不叫测试。那叫披着勤奋外衣的侥幸。 你可以把应用跑上几周，盯着 metrics dashboard，最后照样发布一个 concurrency bug——它只会在两个 request 刚好打进同一个 cache eviction window…
像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。
使用模型检验器不需要学习线性时序逻辑。Kani、CBMC和Alloy等工具允许你用普通的断言和关系约束来验证性质。你放弃了证明活性性质的能力，换来的是以小时而非周为单位的学习曲线，而对于大多数软件错误来说，这是一笔值得的交易。…
像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。
不写一行证明也能证明 Rust 代码正确。干这活的工具叫做模型检验器，目前对 Rust 最实用的一个是 AWS 开发的 Kani。你写普通的 Rust 断言，Kani 把它们转成数学命题，对所有可能的输入进行检验。不需要定理证明器，不需要证明辅助工具，也不需要一头扎进 Coq 半年出不来。…
分布式缺陷在部署后修复成本高昂。模型检验能让你在写下第一行实现代码之前就发现它们。以下是如何使用 TLA+ 做到这一点。
你无法对分布式协议做单元测试。单元测试在一台机器上以一个顺序运行一个进程。而你的协议在五台机器上以十个进程、以你无法控制的顺序运行。这两种现实之间的鸿沟，正是缺陷藏身之处。 模型检验弥合了这一鸿沟。它穷举协议可能到达的每一种状态的所有可能交错。如果存在两条副本不一致的路径、存在领导者选举陷入死锁的路径、或存在…