LLM 无法证明你的代码正确，但它们可以撰写实现证明的样板代码
净室验证需要生成并消解证明义务。以下介绍 LLM 如何自动化注解和验证条件生成，让你可以专注于真正困难的证明。
净室软件工程要求你在编译之前就证明代码的正确性。这听起来很高尚，直到你花三个小时为一个对十个整数进行排序的函数编写循环不变式。 瓶颈不在于证明本身，而在于样板代码。生成验证条件、用不变式注解循环、以及为 Dafny、Why3 或 Z3 格式化断言，这些工作枯燥乏味、容易出错，而且毫无乐趣。LLM…
cleanroom-correctness
6 posts
Cleanroom 实现每千行 0.1 个缺陷。你不需要全盘照搬也能达到这个目标。
Cleanroom software engineering 将 defect rate 降低 100 倍，但全面采用需要独立的 test team 和 formal proof。这里介绍一种 pragmatic subset，无需 overhead 即可捕获大部分收益。
Cleanroom software engineering 每千行代码仅产生 0.1 个缺陷。业界平均水平是 10 到 50。问题是，完整的 Cleanroom 要求你将团队拆分为 author 和 verifier，在每个 module 之前编写 formal specification，并禁止…
IBM 的 Zero-Defect Process 实现了每 KLOC 0.1 个 Bug。行业还是抛弃了它。
IBM 的 Cleanroom engineering 达到了比行业平均水平好 100 倍的 defect rate，然后消失在历史中。它的消失与是否有效毫无关系。
IBM 的 Cleanroom software engineering process 实现了每千行代码 0.1 个 defect。当时的行业平均水平在 10 到 50 之间。该 process 被文档化，在多个项目和语言之间 replicate，并经过独立验证。然后它消失了。 不是因为更好的 method…
真的有人验证了 1 万行代码零缺陷吗？IBM 做到了，而且方法比结果更离奇。
Cleanroom software engineering 承诺通过 mathematical verification 而非 debugging 实现零缺陷增量。我们查看 IBM 的实际项目数据，看看这一说法是否成立。
1980 年代软件行业的平均水平是每千行代码 30 到 60 个缺陷。IBM 的 Cleanroom 团队交付了一个 2 万行的编译器增量，在测试中发现了 53 个缺陷。也就是每 KLOC 2.6 个。一些 1 万行的独立增量在进入系统测试时，没有发现任何缺陷。 最离奇的部分？程序员被禁止运行自己的代码。…
你的模块有三层。你可能只写了一层。
Box Structure 强制你将模块的行为、记忆的状态和实现方式定义为三个独立且可验证的层。以下是 Cleanroom 如何利用它们消除调试。
你先写代码，再写测试，然后发现代码是错的。这是标准循环。也是为什么调试会消耗大多数项目时间线的一半。 Box Structure 把这个过程反转。你在写代码之前就定义行为，用数学方式验证这个定义，然后一层一层翻译成代码。结果是"构造即正确"的模块，而不是"测试碰巧通过所以正确"。…
IBM 禁止开发者运行自己的代码，从而交付了每千行代码 0.1 个缺陷的软件
IBM 的 Cleanroom 工程流程通过预防而非发现缺陷，实现了比行业平均水平好 100 倍的缺陷率。以下是它的工作原理、为何几乎无人使用，以及你今天可以借鉴什么。
IBM 交付了一套 NASA 卫星控制系统，每千行代码仅有 0.1 个缺陷。当时的行业平均水平在 10 到 50 之间。他们并非依靠招聘更聪明的工程师或延长工作时间来达成这一目标。他们靠的是禁止开发者运行自己的代码。 这就是 Cleanroom 软件工程，由 IBM 的 Harlan Mills 于 1970…