Most Bugs Hide in the Gap Between “What It Should Do” and “What It Actually Does”
You write the code first, then write the tests, then discover the code was wrong. That is the standard loop. It is also why debugging consumes half of most project timelines.
Box structures invert this. You define behavior before you write it, verify that definition mathematically, then translate it into code one layer at a time. The result is a module that is correct by construction, not correct because the tests happened to pass.
This sounds impossible until you see how small each layer is.
What Is a Box Structure?
A box structure describes a software module at three levels of abstraction, each a strict refinement of the last:
- Black box: What stimulus produces what response? No state. No implementation. Just a pure function from history to output.
- State box: What state does the module remember, and how does each stimulus transform that state and produce a response?
- Clear box: The actual code.
You design from the outside in. The black box is the contract. The state box is the data model. The clear box is the code. At each step, you prove that the lower layer satisfies the upper layer before you move on.
This is not documentation after the fact. The black box and state box are formal specifications. They are the design. The code comes last.
The Black Box: History Determines Everything
A black box defines a module by its stimulus history and its response. The response to any stimulus depends on every stimulus that came before it.
Consider a simple token bucket rate limiter. The black box specification says:
| Stimulus | Condition on History | Response |
|---|---|---|
request(n) | tokens available >= n | grant(n) |
request(n) | tokens available < n | deny |
add_tokens(k) | any history | no response, update history |
The black box does not say how tokens are tracked. It says: given this history of stimuli, this is the required response.
You can verify this before any code exists. Write sequences of stimuli, compute the expected responses by hand, and check that the specification behaves correctly. No compiler. No test runner. Just logic.
The State Box: Adding Memory Without Adding Assumptions
The state box refines the black box by introducing a state variable that makes the history implicit. Instead of carrying the full stimulus history around, the module remembers a compressed representation.
For the rate limiter, the state box introduces tokens, the current number of available tokens. The specification becomes:
| Stimulus | Precondition on State | Response | New State |
|---|---|---|---|
request(n) | tokens >= n | grant(n) | tokens - n |
request(n) | tokens < n | deny | tokens (unchanged) |
add_tokens(k) | any | no response | tokens + k |
The critical step is proving that this state box is equivalent to the black box. The state variable tokens must faithfully represent the relevant history. If applying the black box’s rules produces the same responses as the state box’s counter, the refinement is valid.
This proof is usually short. You are verifying a one-page specification, not a thousand-line codebase.
The Clear Box: Code That Cannot Surprise You
The clear box is the implementation. It is written in a structured language with no gotos and no hidden control flow. Every clear box is built from sequence, alternation (if-then-else), and iteration (while, for).
Here is a clear box implementation in Python:
class TokenBucket:
def __init__(self, capacity: int, refill_rate: float):
self.capacity = capacity
self.tokens = capacity
self.refill_rate = refill_rate
self.last_refill = time.monotonic()
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) -> str:
self._refill()
if self.tokens >= n:
self.tokens -= n
return f"grant({n})"
return "deny"
def add_tokens(self, k: int) -> None:
self.tokens = min(self.capacity, self.tokens + k)Notice that _refill was not in the state box. Time does not exist in the black box or state box. Those models assume tokens appear by magic when add_tokens is called. The clear box must bridge that gap.
This is where most bugs live. The state box says tokens increases by k. The clear box must also handle continuous refilling and the capacity cap while still conforming to the state box.
How Cleanroom Proves Correctness Without Running Tests
In Cleanroom, you do not write unit tests for the clear box. You perform a verification.
For every control structure, you write a predicate that must hold before and after it executes. For a sequence S1; S2, you prove the postcondition of S1 implies the precondition of S2. For an if-then-else, you prove both branches satisfy the overall postcondition. For a while loop, you find an invariant and prove it holds on entry, is preserved by each iteration, and implies the desired postcondition when the loop terminates.
This is not a proof assistant. It is pencil and paper. If you have ever argued informally that a recursive function terminates, you have done 90 percent of a Cleanroom proof already.
Why Most Teams Do Not Use This
The obvious objection is time. Writing a black box, a state box, and a hand proof sounds slower than just writing the code and fixing the bugs.
Harlan Mills, who developed Cleanroom at IBM, measured the opposite. Cleanroom teams delivered code with an order of magnitude fewer defects than control teams, and their total development time was shorter because they spent almost no time in the debugger.
The less obvious objection is cultural. Box structures force you to think before you type. Most developers find this uncomfortable. The specification feels like bureaucracy. It is not. It is the design. In Cleanroom, the design is written in a notation precise enough to verify, not in a diagram that the first implementation draft ignores.
When Box Structures Are Worth the Overhead
You do not need to specify every utility function this way. Box structures shine where a bug costs more than the time to write a specification: payment processing, authorization, distributed consensus, protocols, and workflow engines. They also help teams that ship the same category of bug repeatedly and never catch it in tests.
A Lightweight Way to Start
You do not need to adopt the full Cleanroom process. Borrow the box structure idea for a single module.
Pick a function that has caused production issues. Write its black box: a table of inputs, conditions, and expected outputs. Do not look at the existing code. Write what it should do, not what it does.
Then write the state box. What state does it need? How does each input transform that state? Compare it to your implementation. Where they differ, you have found a bug or an undocumented assumption.
Here is a minimal template in Python you can adapt:
"""
Black Box Specification: Rate Limiter
Stimuli: request(n), add_tokens(k)
History: sequence of all stimuli received
Rules:
1. After any sequence of stimuli, tokens available =
sum(add_tokens.k) - sum(grant.n)
2. request(n) grants iff tokens available >= n
3. tokens available never exceeds capacity
State Box Refinement:
State: tokens (integer, 0 <= tokens <= capacity)
Invariant: tokens accurately represents available tokens
"""
class TokenBucket:
"""Clear box implementation of the rate limiter state box."""
def __init__(self, capacity: int):
self.capacity = capacity
self.tokens = capacity
def request(self, n: int) -> str:
if n <= 0:
raise ValueError("request must be positive")
if self.tokens >= n:
self.tokens -= n
return f"grant({n})"
return "deny"
def add_tokens(self, k: int) -> None:
if k < 0:
raise ValueError("cannot add negative tokens")
self.tokens = min(self.capacity, self.tokens + k)The comments are the specification. The code is the implementation. Keeping them in the same file makes the refinement visible and reviewable.
The Real Value Is the Separation of Concerns
Box structures are not magic. They will not catch every bug. What they do is force a discipline that most development processes skip: defining what correct means before you build it.
The black box separates the module’s contract from its internals. The state box separates the data model from the code. The clear box separates implementation from proof. Each layer has one job, and you verify it before you move to the next.
That is why you should care. The gap between “what it should do” and “what it does” is where your bugs live, and box structures are a systematic way to close that gap before you write a single test.
If you want to go deeper, Mills’ Cleanroom Software Engineering and the original IBM technical reports are still the clearest references. The ideas are old. The bugs they prevent are not.