# Machine-Checkable Spec · 机器可检规格

> Use before you let an agent generate anything non-trivial. A spec an agent can act on is not prose;
> it is intent plus a boundary plus acceptance assertions a checker can run, plus the counter-examples
> that must fail. If an assertion cannot be machine-checked, mark it and route it to a human judge.

## 1. Intent

| Field | Fill |
|---|---|
| What this produces |  |
| Who / what consumes it |  |
| Done means |  |
| Explicitly out of scope |  |

## 2. Boundary

| Constraint | Value | Hard / soft |
|---|---|---|
| Inputs it may read |  | hard / soft |
| Outputs it may write |  | hard / soft |
| Must never do |  | hard |
| Reversible? |  | — |

## 3. Acceptance Assertions

Each row is a claim a checker can evaluate to pass / fail. No "looks fine" allowed.

| # | Assertion (machine-checkable) | How verified | Owner |
|---|---|---|---|
| A1 |  | test / type / lint / oracle |  |
| A2 |  | test / type / lint / oracle |  |
| A3 |  | test / type / lint / oracle |  |

## 4. Counter-Examples (must fail)

Inputs or behaviors that must be rejected. A spec with no counter-examples is not yet load-bearing.

| # | Counter-example | Expected rejection |
|---|---|---|
| N1 |  |  |
| N2 |  |  |

## 5. Human-Judgment Residue

- Assertions that cannot be machine-checked yet: 
- Who signs off on those: 
- Irreversible actions requiring an explicit gate: 

---

Status: **Ship** (assertions pass, counter-examples fail) · **Hold** (an assertion is not yet
checkable) · **Stop** (a counter-example passes, or the irreversible gate has no owner).