Bend 2 与 vibe-coding 陷阱：在调研之前造完了一门语言和编译器
Bend 2 的 demo 要用 58 行声明「定律」、442 行写证明。作者用形式验证领域的 SPARK 重做同一程序，只需写明不变量，GNATprove 一次通过 12 项检查。
形式化验证
更多 形式化验证
首页用 Lean 写 Zstandard 解压器：当 LLM 把「证明成本」压下来
Adam Langley 用 Lean 写了一个 Zstandard 解压器，把类型级不变量写成类型签名，再让 LLM 去补证明体， 并记下它在哪些步骤上真的省了事。