用 PDD Kit 形式化验证智能体编写的全栈 Web 应用

概览 把形式化方法用在日常软件里。 PDD Kit 帮你把意图变成一份形式化规格，然后证明智能体写的代码对任意输入都满足这份规格；证明覆盖不到的地方，再用测试补上。它把形式化方法从少数专家的小众工作，带给了没有形式化方法背景的工程师，也带给了日常应用——就像这里展示的这个全栈 Web 应用。 随着 AI 智能体生成的代码越来越多，逐行人工审阅已经很难规模化。计划本该是你和编程智能体之间的契约，但实际上没有什么能强制智能体遵守它。智能体自己写的测试，通常检验的是它造出来的东西，而不是你要求的东西。PDD Kit 让智能体守住计划：它和你一起把意图写成 Verus 形式化规格，证明智能体的代码对任