LLM可以生成Rust代码，但形式化证明完全是另一回事。
大语言模型能写出质量惊人的Rust代码，但当你要求形式化证明时，它们会幻觉出不变量，并编造出没有任何验证器接受的语法。本文介绍它们真正做对了什么、在哪里崩溃，以及如何善用它们。
LLM能写出可以编译甚至通过的Rust代码。但它们目前还无法可靠地写出形式化证明，来证实代码对所有可能的输入都是正确的。…
想法与洞见
探索 AI 优先开发、编码护栏和可处置架构。
干等 race condition 是最烂的测试策略
model checking 如何在数秒内碾压你在生产环境跑几天才能发现 concurrency bug 的做法，以及如何把它用在自己的代码上。
在生产环境里等 race condition 冒出来，那不叫测试。那叫披着勤奋外衣的侥幸。 你可以把应用跑上几周，盯着 metrics dashboard，最后照样发布一个 concurrency bug——它只会在两个 request 刚好打进同一个 cache eviction window…
无需学习时序逻辑即可对代码进行模型检验
像Kani这样的有界模型检验器和像Alloy这样的关系模型查找器允许你用普通的断言和约束来验证性质。你放弃了活性证明，换来的是以小时而非周为单位的学习曲线。
使用模型检验器不需要学习线性时序逻辑。Kani、CBMC和Alloy等工具允许你用普通的断言和关系约束来验证性质。你放弃了证明活性性质的能力，换来的是以小时而非周为单位的学习曲线，而对于大多数软件错误来说，这是一笔值得的交易。…
不写一行证明也能证明 Rust 代码正确，但状态空间就是代价
像 Kani 这样的模型检验工具让你可以用断言代替形式化证明来验证 Rust 性质。棘手之处在于，当你的循环没有小的边界时会发生什么。
不写一行证明也能证明 Rust 代码正确。干这活的工具叫做模型检验器，目前对 Rust 最实用的一个是 AWS 开发的 Kani。你写普通的 Rust 断言，Kani 把它们转成数学命题，对所有可能的输入进行检验。不需要定理证明器，不需要证明辅助工具，也不需要一头扎进 Coq 半年出不来。…
无法对分布式协议做单元测试，但可以做模型检验
分布式缺陷在部署后修复成本高昂。模型检验能让你在写下第一行实现代码之前就发现它们。以下是如何使用 TLA+ 做到这一点。
你无法对分布式协议做单元测试。单元测试在一台机器上以一个顺序运行一个进程。而你的协议在五台机器上以十个进程、以你无法控制的顺序运行。这两种现实之间的鸿沟，正是缺陷藏身之处。 模型检验弥合了这一鸿沟。它穷举协议可能到达的每一种状态的所有可能交错。如果存在两条副本不一致的路径、存在领导者选举陷入死锁的路径、或存在…
跨环境复制 `.env` 文件不是配置策略
基础设施团队如何使用按上下文划分的 DSL 来管理 dev、staging 和 production 之间的配置，使环境差异显式且类型安全。
staging 环境运行正常。production 环境运行异常。它们的 文件之间的差异高达 400 行，其中一半是从无人再相信的注释。上个月有人往 staging 里加了 。没人往 production 里加。应用程序还是启动了，使用了硬编码的默认值，现在你的功能标志不同步了。…
语法约束解码: 让每个 token 都强制 LLM 输出有效语法
LLM 会对语法产生幻觉，因为它们以概率方式采样 token。语法约束解码在每一步过滤词表，只输出保持语法有效性的 token。
让 LLM 生成一个 JSON 对象，它最终一定会输出一个末尾逗号、字符串里未转义的换行符，或者在一个本该有引号键的位置输出 bare word。这个错误不是模型的 bug。它是自回归采样工作方式的必然结果：在每一步，模型都会把自己的词表里每个 token 都当作候选，包括那些会让部分输出在语法上 invalid 的…
从英语翻译到主题很容易。使其具备确定性才是真正的问题。
你可以从简单的英语描述中生成设计令牌，但前提是将该描述视为带有模式契约和快照测试的限界上下文DSL。
是的，你可以用英语描述一个主题，并得到一个可用的设计系统。关键在于，这段英语描述不是提示词。它是源文件。和任何源文件一样，它需要编译器、类型系统和测试。…
丢掉语法文件：用纯 TypeScript 写你的 DSL 解析器
对于大多数 bounded-context 的 DSL 来说，解析器生成器是大材小用。解析器组合子让你可以用与应用相同的语言构建可用的解析器，无需生成代码，也无需构建步骤。
如果你曾经打开过 Yacc 的语法文件，并疑惑为什么构建一门语言需要学习第二门语言，那么你并不孤单。解析器生成器很强大，但对于在 bounded context 中自然涌现的小型 DSL 来说，它们几乎总是大材小用。 你可以用与应用其余部分相同的语言来编写解析器。没有构建步骤，没有语法文件，没有你无法调试的生成代码。…
运行时配置错误是你选择允许的生产故障
如何使用模式验证和构建时检查，在应用程序开始处理流量之前捕获配置错误。
你的应用程序在周五晚上三小时后抛出了 。堆栈跟踪指向配置对象中一个深层嵌套的属性。值是 。有人在未更新验证逻辑的情况下，将 更改推送到了生产环境。 这不是运行时缺陷。这是策略失败。你让不受信任的数据未经检查就进入了系统。 大多数团队被动地验证配置。缺少环境变量会导致崩溃。无效的 URL 字符串会一直传播，直到…