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月5日 不写一行证明也能证明 Rust 代码正确，但状态空间就是代价 像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。 model-checkingrustverificationformal-methods
2026年6月26日 你的依赖可以读取磁盘上的任何文件。cap-std 让它们先请求权限。 Rust 的标准库向每个依赖授予隐式的文件系统权限。cap-std 将其替换为基于权能的 API，强制代码在打开路径之前证明它有权访问该路径。 capability-based-securityrustcap-stdsandboxing
2026年6月22日 别再抛出你的类型检查器看不见的错误 抛出的异常会把失败路径从你的类型系统中隐藏起来。下面解释为什么显式返回错误能让代码更诚实，以及如何在不折磨自己的情况下采用这一模式。 type-level-correctnesserror-handlingtypescriptrust
2026年6月21日 Rust newtype 在编译期让非法状态无法表示，且零开销 一个单字段包装结构体就能在编译期捕获单位混淆和类型错用，不增加哪怕一个字节的开销。 type-level-correctnessrustnewtypeszero-cost-abstractions
2026年5月28日 Rust 的变异测试确实能用，但你的编译时间会恨你 cargo-mutants 能找出那些只是假装在验证代码的测试。本文介绍变异测试在 Rust 中的工作原理、它能捕捉什么问题，以及编译时间成本是否值得。 deep-divesmutation-testingrustcargo-mutantstest-quality
2026年5月23日 Rust 中的 property-based tests 能找到单元测试漏掉的 bug 基于示例的测试只覆盖你想得到的输入。property-based testing 生成随机数据，检查 invariants，并将失败 shrink 到最小反例。 deep-divesrustproperty-based-testingquickcheckproptest
2026年5月21日 Rust 的 Runtime Contracts 可以在 Release 构建中零开销，但编译器不会替你实现 Rust 会自动剥离 debug assertions，但真正的 design-by-contract 需要的远不止 debug_assert!。本文介绍如何在 Release 二进制文件中实现零成本的 runtime contracts，并让它们彻底消失。 deep-divesrustruntime-contractsperformance
