Cleanroom software engineering 每千行代码仅产生 0.1 个缺陷。业界平均水平是 10 到 50。问题是，完整的 Cleanroom 要求你将团队拆分为 author 和 verifier，在每个 module 之前编写 formal specification，并禁止 developer 运行自己的代码，直到独立的 test team 对其进行统计验证。

大多数 engineering manager 看到这套流程，快速算了一下 headcount，便认为质量不值得付出这么多 overhead。他们对了一半。完整的 Cleanroom process 确实很沉重。但其 underlying principles 是轻量的，你可以在不雇佣 verification army、不禁止 cargo test 的情况下采纳它们。

Cleanroom 到底是什么

Cleanroom 是 1970 年代由 IBM 的 Harlan Mills 开发的一种 software development process。名字来源于半导体制造：你预防产生缺陷的条件，而不是事后再 inspect 出来。核心主张是，如果你设计得足够谨慎，使得 bug 在代码写出之前就变为不可能，那么软件就可以通过 construction 达到 correct。

该方法建立在三种实践之上：statistical process control 下的 incremental development、box structures 的 function-theoretic design、以及由独立团队执行的 statistical usage testing。这三种实践相互依赖。打破其中一个，其他两个就会失去力量。

正是这种 interdependency 催生了 overhead 的 myth。团队以为要么全部采纳，要么完全不采纳。事实并非如此。这些实践相互 reinforcement，但各自独立也能产生价值。

真正的 overhead 在哪里

人们所恐惧的 80% overhead 来自两项具体要求。

第一，no-execution rule。在完整的 Cleanroom 中，编写代码的 developer 不编译、不运行、不写 unit test。独立的 verification team 负责所有执行。这迫使 developer 在敲键盘之前把每种情况都推理清楚，也正是代码第一次就能跑对的原因。但这同时也要求你将 engineering headcount 翻倍，或将现有团队拆成两个互相怨恨的组。

第二，formal verification step。在编写 clear box implementation 之前，团队先写 black box specification 和 state box refinement，然后手工证明 state box 与 black box 等价。这是 pencil-and-paper proof，不是 proof assistant。它确实有效，但大多数团队没有那么多时间和 training。

第三项实践，statistical process control 下的 incremental development，如果你已经在做 sprint，那它实际上是免费的。你交付小的 increment，测量每个 increment 的 defect density，当某个 increment 超出缺陷目标时就叫停，找出方法哪里出了问题。这不过是定义更严格的 “done” 的 data-driven retrospective。

务实子集：保留结构，砍掉官僚

只要保留 structural discipline、抛弃 organizational mandates，你就能获得 Cleanroom 的大部分缺陷削减效果。

以下是该保留的。

先写 contract，再写 code。 不是 Z notation 的 formal specification。只需清晰描述 input、output、precondition 和 postcondition。如果你写不出 correct 意味着什么，就不可能写出 correct 的代码。

显式 encode 状态机。 大多数 bug 藏在 developer 认为不可能发生的 state transition 里。在写逻辑之前，先用 table 或 data structure 定义好状态和转换。

让别人测试你的 logic。 authorship 和 verification 的分离是 Cleanroom 最强大的思想。你不需要独立的 team，只需要一个没写过这段代码的人来设计 test case。自己测试自己的代码，测的只是自己的 assumption。

按 increment 测量 defect density。 追踪每个 phase 漏掉多少 bug。如果 integration bug 总是漏网，问题不在于 developer 粗心，而在于你的 process 允许 integration bug 存在。

以下是该砍掉的。

砍掉 no-execution rule。 让 developer 运行自己的代码。先推理再执行的 discipline 即使允许事后快速 sanity check 也依然有价值。关键是编译前先想清楚，而不是假装编译器不存在。

砍掉 formal hand proof。 除非你在写 avionics software，否则 pencil-and-paper proof 是 overkill。用 property-based tests 和 type-driven design 替代。它们是同一套推理的 mechanized version，而且能在 CI 里跑。

砍掉 statistical usage testing 的要求。 完整 Cleanroom 针对 usage profile 而不是 code coverage 做测试。如果你有数据，这很好。如果没有，property-based testing 和 mutation testing 用你现有的工具就能给你几乎同样的 confidence。

Python 中的轻量 Cleanroom 工作流

下面展示单个 module 的实际做法。从 contract 开始。

"""
Black Box: Token Bucket Rate Limiter

Stimuli: request(n), add_tokens(k)
Precondition: n > 0, k >= 0, capacity > 0
Postcondition:
  - request(n) grants iff available tokens >= n
  - request(n) reduces available tokens by n if granted
  - add_tokens(k) increases available tokens by k, capped at capacity
  - available tokens never negative, never exceeds capacity
"""

然后 encode 状态机。

from enum import Enum, auto

class RateLimitState(Enum):
    READY = auto()      # tokens >= 1, requests may grant
    DEPLETED = auto()   # tokens == 0, requests deny

# Transitions depend on token count, not external events
# READY -> DEPLETED when tokens reach 0
# DEPLETED -> READY when tokens added above 0

然后写 implementation。

import time
from dataclasses import dataclass

@dataclass
class TokenBucket:
    capacity: int
    tokens: int
    refill_rate: float
    last_refill: float

    def _refill(self) -> None:
        now = time.monotonic()
        elapsed = now - self.last_refill
        added = int(elapsed * self.refill_rate)
        if added > 0:
            self.tokens = min(self.capacity, self.tokens + added)
            self.last_refill = now

    def request(self, n: int) -> bool:
        if n <= 0:
            raise ValueError("request must be positive")
        self._refill()
        if self.tokens >= n:
            self.tokens -= n
            return True
        return False

    def add_tokens(self, k: int) -> None:
        if k < 0:
            raise ValueError("cannot add negative tokens")
        self.tokens = min(self.capacity, self.tokens + k)

contract 放在 docstring 里。状态机是显式的。implementation 很短，可以通过 inspection 验证。这不是完整 Cleanroom，也不是 cowboy coding。

你真正可以做的 verification step

在完整 Cleanroom 中，独立团队基于 usage profile 写统计测试。在务实版本中，你写 property-based tests，然后请同事 review。

from hypothesis import given, strategies as st

@given(
    capacity=st.integers(min_value=1, max_value=1000),
    initial=st.integers(min_value=0, max_value=1000),
    requests=st.lists(st.integers(min_value=1, max_value=100), max_size=50),
)
def test_token_bucket_never_overdrafts(capacity, initial, requests):
    bucket = TokenBucket(
        capacity=capacity,
        tokens=min(initial, capacity),
        refill_rate=0.0,
        last_refill=time.monotonic(),
    )

    for n in requests:
        granted = bucket.request(n)
        assert bucket.tokens >= 0
        if granted:
            # tokens were deducted, so pre-request balance was sufficient
            pass
        else:
            # request denied, current tokens insufficient
            assert bucket.tokens < n

这个 test 不检查具体 output，而是检查 invariant：bucket 永远不会批准超过其持有量的 token。这就是 Cleanroom proof 的 property-based 版本。它自动运行，能发现你想不到的 edge case，而且不需要独立的 verification team。

trade-off 是真实存在的

务实的 Cleanroom 不是免费的。先写 contract 需要 discipline。显式的状态机 在代码”显而易见”时感觉像 boilerplate。让别人测试你的 logic 需要协调。

它也确实不如真家伙强大。完整 Cleanroom 的 no-execution rule 能强制一种深度推理，而当你离 REPL 只有一个 keystroke 时，这种深度是无法复制的。formal proof 能抓住 property-based tests 可能漏掉的逻辑错误——前提是你的 properties 本身没错。

但比较对象不是务实 Cleanroom 对完整 Cleanroom，而是务实 Cleanroom 对你现在的做法。如果你现在的 process 每千行出 20 个缺陷，而务实 Cleanroom 能把你降到 5，那就是用一小部分 overhead 换来了 4 倍提升。

什么时候值得这样做

别在每个 utility function 上都用这套。把它用在 bug 代价高的代码上：authorization、billing、distributed protocol、超过三个状态的状态机、以及任何在生产环境中引发过两次 incident 的东西。

需要这套方法信号不是复杂度，而是反复出现的意外。如果你的团队在 test 或 production 里不断发现同一类 bug，问题不是 developer 粗心，而是这段 code 的 contract 从未被定义，因此 “correct” 从未被 specified。

从一个 module 开始

你不需要管理层批准，也不需要 overhaul process。挑一个以前咬过你的 module。在碰 implementation 之前，先在 docstring 里写好 contract。定义状态和转换。请一位同事不看你的代码来写测试。在 CI 里跑 property-based tests。

就这些。没有独立团队，没有 formal notation，没有禁止运行自己代码的规定。

Cleanroom 每千行 0.1 个缺陷不是 magic。它是一个强迫人们在动手之前先定义 correct 的 process 的 output。你用一份 docstring、一张 状态机表、以及一位测试你 assumption 而非测试你代码的同事，就能获得大部分同样的效果。