2026年7月9日 AutoVerus将40小时的证明编写变成3次LLM调用。诀窍在于知道何时放弃。 AutoVerus利用LLM智能体网络为Rust代码生成Verus正确性证明，通过由SMT求解器反馈驱动的生成-修复-消除循环，自动化超过90%的证明义务。 model-checkingautoverusrustverification
2026年7月8日 LLM可以生成Rust代码，但形式化证明完全是另一回事。 大语言模型能写出质量惊人的Rust代码，但当你要求形式化证明时，它们会幻觉出不变量，并编造出没有任何验证器接受的语法。本文介绍它们真正做对了什么、在哪里崩溃，以及如何善用它们。 model-checkingllmrustformal-proofs
2026年7月7日 干等 race condition 是最烂的测试策略 model checking 如何在数秒内碾压你在生产环境跑几天才能发现 concurrency bug 的做法，以及如何把它用在自己的代码上。 model-checkingrace-conditionsconcurrencytesting
2026年7月6日 无需学习时序逻辑即可对代码进行模型检验 像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。 model-checkingtemporal-logicformal-methodsverification
2026年7月5日 不写一行证明也能证明 Rust 代码正确，但状态空间就是代价 像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。 model-checkingrustverificationformal-methods
2026年7月4日 无法对分布式协议做单元测试，但可以做模型检验 分布式缺陷在部署后修复成本高昂。模型检验能让你在写下第一行实现代码之前就发现它们。以下是如何使用 TLA+ 做到这一点。 model-checkingdistributed-systemstlaplusprotocol-design
