Problem
"A test that cannot fail is not evidence" is the central discipline of any
verification flow, and the engine has no way to express it. Proving a test bites
means: run it green, apply a patch that breaks the invariant, assert it now
fails, restore, assert green again.
Today that is bespoke shell written by hand for every invariant — copy the file,
sed the mutation in, run the filter, grep the output, copy the file back. It
is easy to write, easy to get subtly wrong, and impossible for a gate to verify
afterwards, because all that survives is prose describing what happened.
Why it matters more than it sounds
In one relay campaign, every hand-written mutation proof was narrower than the
claim it supported:
- A call-site guard was described as scanning "a generous window around the
call." It anchored on a log string two lines above, covering 10 lines of a
38-line arm. A regression added to the other 28 lines passed the guard and
the full 1,298-test suite.
- Three wire constants were "unified behind one predicate." Renaming all three
values left 25 Rust tests and 9 vitest cases green, because every test
compared through the symbol rather than the literal.
- A commit claimed "4 of 4 pre-existing tests still pass" under a mutation. The
filter used matched 4 of the 14 relevant tests.
Each mutation was real and each result was real. The scope of each proof was
asserted in a commit message and checked by nobody.
Proposal
Make the mutation the declaration, so the engine performs it and owns the
result:
f.run('cargo test -p broker --lib delivery_retry', {
proves: {
// each entry: the invariant must FAIL when this patch is applied
'retry cap is reachable': {
file: 'crates/broker/src/runtime/delivery.rs',
replace: 'current.failed_attempts = current.failed_attempts.saturating_add(1);',
with: '',
},
},
})
The engine then: runs green → applies patch → runs → asserts red → restores
→ asserts green, and journals all four results. A mutation that does not turn
the step red fails the step, with the message "this test cannot fail."
Properties that matter:
- The restore is the engine's responsibility, not the agent's. A half-restored
tree is a real hazard when agents share one checkout.
- The result is structured, so a later gate can require "every invariant has at
least one killed mutant" instead of grepping a document.
- Scope becomes explicit: the patch is in the flow definition and reviewable,
rather than described after the fact.
Relationship to #531
#531 makes evidence unforgeable. This makes the right evidence cheap to
produce. Together they turn "prove it bites" from a discipline someone has to
remember into a property of the step.
Problem
"A test that cannot fail is not evidence" is the central discipline of any
verification flow, and the engine has no way to express it. Proving a test bites
means: run it green, apply a patch that breaks the invariant, assert it now
fails, restore, assert green again.
Today that is bespoke shell written by hand for every invariant — copy the file,
sedthe mutation in, run the filter, grep the output, copy the file back. Itis easy to write, easy to get subtly wrong, and impossible for a gate to verify
afterwards, because all that survives is prose describing what happened.
Why it matters more than it sounds
In one relay campaign, every hand-written mutation proof was narrower than the
claim it supported:
call." It anchored on a log string two lines above, covering 10 lines of a
38-line arm. A regression added to the other 28 lines passed the guard and
the full 1,298-test suite.
values left 25 Rust tests and 9 vitest cases green, because every test
compared through the symbol rather than the literal.
filter used matched 4 of the 14 relevant tests.
Each mutation was real and each result was real. The scope of each proof was
asserted in a commit message and checked by nobody.
Proposal
Make the mutation the declaration, so the engine performs it and owns the
result:
The engine then: runs green → applies patch → runs → asserts red → restores
→ asserts green, and journals all four results. A mutation that does not turn
the step red fails the step, with the message "this test cannot fail."
Properties that matter:
tree is a real hazard when agents share one checkout.
least one killed mutant" instead of grepping a document.
rather than described after the fact.
Relationship to #531
#531 makes evidence unforgeable. This makes the right evidence cheap to
produce. Together they turn "prove it bites" from a discipline someone has to
remember into a property of the step.