9 posts
AutoVerus利用LLM智能体网络为Rust代码生成Verus正确性证明，通过由SMT求解器反馈驱动的生成-修复-消除循环，自动化超过90%的证明义务。
形式化验证中最困难的部分从来不是验证器本身，而是编写证明。 给一位资深Rust工程师Verus——微软研究院开发的基于SMT的验证器——他可以在一个下午内为函数添加前置条件和后置条件注释。然后验证器会以机械确定性告诉他，该函数是否对所有可能的输入满足这些契约。这部分令人满意。…
大语言模型能写出质量惊人的Rust代码，但当你要求形式化证明时，它们会幻觉出不变量，并编造出没有任何验证器接受的语法。本文介绍它们真正做对了什么、在哪里崩溃，以及如何善用它们。
LLM能写出可以编译甚至通过的Rust代码。但它们目前还无法可靠地写出形式化证明，来证实代码对所有可能的输入都是正确的。…
像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。
不写一行证明也能证明 Rust 代码正确。干这活的工具叫做模型检验器，目前对 Rust 最实用的一个是 AWS 开发的 Kani。你写普通的 Rust 断言，Kani 把它们转成数学命题，对所有可能的输入进行检验。不需要定理证明器，不需要证明辅助工具，也不需要一头扎进 Coq 半年出不来。…
Rust 的标准库向每个依赖授予隐式的文件系统权限。cap-std 将其替换为基于权能的 API，强制代码在打开路径之前证明它有权访问该路径。
你依赖树中的任何一个 crate 都可以打开 、向你的 目录写入内容，或者枚举你项目中的每一个文件。Rust 的标准库不会请求许可。它假设任何能够调用 的代码都有权接触操作系统允许的任何路径。 cap-std 改变了这一假设。它是 Rust I/O module…
抛出的异常会把失败路径从你的类型系统中隐藏起来。下面解释为什么显式返回错误能让代码更诚实，以及如何在不折磨自己的情况下采用这一模式。
你的函数签名说它返回一个 。事实并非如此。它返回一个 ，或者它会爆炸。类型系统根本不知道还有第二条分支。 这正是基于异常的错误处理最根本的不诚实之处。每一个…
一个单字段包装结构体就能在编译期捕获单位混淆和类型错用，不增加哪怕一个字节的开销。
把一个 用户 ID 传给期望 order ID 的函数，Rust 不会报错。两者都是 。编译器看到的是完全相同的类型，所以帮不了你。直到运行时你才会发现，通常是在生产环境，通常是在一次你以为安全的重构之后。 这正是 newtype 模式存在所要消灭的那类 bug。 newtype…
cargo-mutants 能找出那些只是假装在验证代码的测试。本文介绍变异测试在 Rust 中的工作原理、它能捕捉什么问题，以及编译时间成本是否值得。
你有 100% 的行覆盖率。每个分支都执行到了。每个函数都被调用了。然后有人在定价逻辑里把一个 改成了 ，跑了一遍测试，全部通过。 这不是理论问题。它真实发生在你的测试执行了代码，却没有真正验证行为的时候。覆盖率衡量的是哪些行被执行了，而不是哪些输出被检查了。变异测试通过故意引入小的…
基于示例的测试只覆盖你想得到的输入。property-based testing 生成随机数据，检查 invariants，并将失败 shrink 到最小反例。
你写了一个 函数。你用 和 测了它。测试通过。你发布了。 用户传入了一个单元素切片。你的函数把它漏掉了。他们提了 issue。你盯着测试文件，想不通这么明显的问题自己是怎么漏掉的。 你漏掉它，是因为 example-based testing 只能抓住你提前预料到的 bug。测试套件里的每一个…
Rust 会自动剥离 debug assertions，但真正的 design-by-contract 需要的远不止 debug_assert!。本文介绍如何在 Release 二进制文件中实现零成本的 runtime contracts，并让它们彻底消失。
Rust 可以在开发阶段强制执行 runtime contracts，并在 release 构建中将其完全抹除。前提是这门语言并没有把 contracts 当作一等公民。你会拿到所有积木，但得自己把它们拼起来。 是最显而易见的起点。它在 debug 构建中执行，在 release 构建中编译为空。这对简单的…