Engineering guide
Build tests from requirements
Requirements-based testing starts with the expected behavior and asks which observations could show it is wrong. The implementation supplies the result under test, not the authority for what should happen.
Start with a decision table
For a transfer requirement, define the expected response and state change for valid funds, insufficient funds, invalid amounts, and retries. Include the assumptions that make each case meaningful, such as the concurrency model and currency representation.
| Illustrative case | Expected observation |
|---|---|
| Valid positive amount, sufficient funds | One debit and one matching credit. |
| Insufficient funds | Rejection; both balances unchanged. |
| Repeated accepted transaction ID | No second transfer. |
| Concurrent requests near the balance bound | No accepted execution violates the approved balance rule. |
These are proposed cases for an illustrative contract. Validate them against the accepted requirement before turning them into an oracle.
Make the assertion distinguish the failure
A test that checks only for a non-nil response can pass while the transfer debits twice. Assert the required output and relevant state, including what must not change on failure. Use the real implementation path and isolate the condition the case is intended to examine.
Trace the test to the governing requirement and obligation. The annotation records ownership; actual execution and the quality of the assertion remain separate questions.
A requirement, five cases and two observed failures
The executed reservation fixture states that a retry with the same key before 24 elapsed hours must return the original reservation. Its author supplied this draft requirement and the expected results; it is not approved customer intent.
| Claim or boundary | Check | Recorded observation |
|---|---|---|
| Preserve the reservation inside the promised window. | Retry at 0, 1, 12 and 23 hours; compare identity and reservation count. | With 24-hour retention, all four pass. With 12-hour retention, the 12- and 23-hour cases create a second reservation. |
| Inspect expiry at exactly 24 hours. | Expect a new reservation at the implementation’s expiry boundary. | Passes in all three snapshots. This case is outside the requirement’s promised window. |
| Preserve behavior across concurrent requests or process restarts. | No such execution is included. | Not established by this fixture. |
Snapshot A passes five cases, B passes three and fails two, and repaired snapshot C passes five. Those are observations of Python and SQLite with an injected clock. The assembled package still lacks traced per-requirement execution records, so a passing test command does not make the Change accepted.
Inspect B’s inputs and observations · Inspect revisions and execution provenance
Use generated vectors with a reviewed harness
proof testgen specs/system transfer --engine heuristic
proof testgen specs/system transfer --check-staleReplace the spec and component with the project's names. Test generation writes case JSON for active formalized requirements. The default engine is Kind2; heuristic generation is explicitly selected above. The staleness command checks existing fixtures without regenerating them.
Generated vectors need a harness that maps model inputs into product calls and compares the right outputs. Review that mapping and any simplifications. Generating fixtures does not execute the product, and check-only audit or documentation paths do not create a generated test suite.
Keep regression and class conclusions separate
When a test exposes a defect, preserve the failing input and expected behavior. Verify the repair on that witness, add a durable regression, and examine related cases where the same mechanism could recur.
One regression establishes an observation for one case. A claim about an entire class requires an explicit model or analysis scope and justified assumptions. Do not turn a single passing test into “all transfers are correct.” Keep evidence tied to the requirement, code revision, configuration, and execution environment.
Continue from here
Inspect witness grounding. Distinguish execution coverage from promise coverage.
Bring one requirement and a test that currently passes without checking its most important failure mode. Bring a change to Proof.