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 state machine。 大多數 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 state machine。

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 裡。state machine 是顯式的。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。顯式的 state machine 在程式碼”顯而易見”時感覺像 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、超過三個狀態的 state machine、以及任何在生產環境中引發過兩次 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、一張 state machine table、以及一位測試你 assumption 而非測試你程式碼的同事，就能獲得大部分同樣的效果。