The asymmetry
A green invariant test is one signal, not two.
A property-based test that finishes a fuzz campaign with no counterexample tells you a specific thing: under the inputs the fuzzer reached, within the budget you gave it, the property you stated did not produce a violation. That is a useful signal. It is also a one-sided signal.
There is a second thing you want to know, and the first leg cannot tell you. You want to know whether the property would have caught a real violation if one had been present. A property that passes when the code is correct and also passes when the code is broken is not a property; it is a comment. Foundry, snforge, Echidna, and Medusa will all happily run a comment to green in CI on every push.
The asymmetry matters because the common failure modes of property tests are silent. A typo in an assertion that elides the inequality. A precondition that quietly excludes the state where the bug would surface. A fuzzer corpus that does not reach the relevant code path within the campaign budget. None of these produce a CI failure. They produce a green badge on a property that is no longer testing the thing it claims to test.
The check that exposes those failure modes is the planted twin, run alongside the clean reference, asserted in CI.
The gate
Two contracts, one property, both legs asserted.
The structure is small. Take the contract you care about. Write two versions of it:
- Clean. The version that actually satisfies the rule.
- Planted. The same code with exactly one localized defect that violates the rule.
Keep the property file byte-identical between the two. Run the same campaign against both. Expect two outcomes:
- Planted leg: the campaign exits non-zero with at least one counterexample. A deterministic violation marker on stdout is what CI grades on. The property catches the planted bug.
- Clean leg: the campaign exits zero with no counterexamples and no violation markers. The property holds on the version that is supposed to be correct.
CI asserts both on every push. A green run means both legs passed: the planted side broke when it was supposed to, and the clean side held when it was supposed to. Either leg's failure is a real regression. The planted leg falling silent means the property has stopped catching the bug class. The clean leg failing means the property is firing on code that is supposed to satisfy the rule, which usually means the property has drifted or the clean reference has acquired a real defect.
The reason this is a gate and not a recommendation is that it pins both edges. A property that only ever has to pass on clean code has no test for whether it would catch anything. A property that only ever has to fire on broken code has no test for whether it false-positives on correct code. The pair is the gate. Either leg alone is a single-sided check, and single-sided checks tend to drift toward the side you remembered to assert.
A working example
A 2×12 matrix, one source tree, two feature flags.
A concrete shape. The
caliperforge/cf-invariants-starknet
repository (Apache-2.0) carries twelve Cairo reference contracts, each with one invariant property,
each wired as a planted/clean pair. The CI workflow runs a 2×12 matrix:
{planted, clean} × 12 references. Every push has to land all of those jobs green.
The wiring is feature-gated rather than two separate trees. Per reference:
# Scarb.toml
[features]
clean = []
// src/lib.cairo (sketch)
#[cfg(feature: 'clean')]
pub const CLEAN_TWIN: bool = true;
#[cfg(not(feature: 'clean'))]
pub const CLEAN_TWIN: bool = false;
// ... in the body, the planted line is wrapped:
if CLEAN_TWIN {
// the corrected behavior
} else {
// the planted defect
}
The test driver runs the same property in both configurations:
| Leg | Command | CI assertion |
|---|---|---|
| planted | snforge test | exit code != 0 AND INVARIANT VIOLATED marker present on stdout |
| clean | snforge test --features clean | exit code == 0 AND zero markers on stdout |
Two things are worth noting about this shape.
First, the test file is byte-identical between the two legs. The only thing that changes is which
branch of the CLEAN_TWIN const is compiled in. That is what makes the comparison honest.
A property that fires on the planted leg and not on the clean leg is responding to one localized code
difference, not to two test files that happen to differ in subtle ways.
Second, the violation marker on stdout is the artifact, not the CI badge. Anyone who clones the repo
and runs snforge test against a planted reference gets the same
INVARIANT VIOLATED line whether or not they trust the CI. The deterministic record is
what makes the claim checkable without re-running the CI infrastructure.
The pattern is in tree on main and is what every push has to land. The first paired
matrix run landed in June 2026 (PR #2, commit 0bff2c4, "CI: paired clean=0 / planted>=1
across 12 references"). The workflow is in
.github/workflows/ci.yml
and the references are under
references/.
Readers can fork it and adopt the shape directly; the structure is small enough to lift.
What you miss without it
Property tests existed. The gate did not.
The argument for the second leg is easier to make against the published record than in the abstract. A recurring pattern across post-mortems of the last two years: the protocol had a property test or invariant suite covering an adjacent rule, and the rule that the exploit actually violated either was not stated as a runnable property, was stated but never asserted on a known-bad reference, or was stated, asserted, and then quietly stopped firing under a corpus that no longer reached the relevant state.
You can read this pattern across the Exploit→Invariant Atlas entries: an oracle freshness check that was present in spec prose but never compiled into a property; a conservation rule that was a comment in the bridge contract; a solvency bound that was tested under preconditions that the exploit path stepped around. In each case the harness, where one existed, would have passed the clean-side leg. None of them had a planted-side leg that would have failed if the property had drifted away from the bug class.
The point is not that a planted twin would have caught every one of these. It would not have. A planted twin catches the bug class it encodes, and only that class. The point is that without the planted leg, you cannot tell, on the day of the push, whether your invariant test is still testing the thing you wrote it to test. The next time the bug class shows up in production, the property either fires or it does not, and you find out which by reading the post-mortem.
A gate that catches drift on every push, against a known-bad reference, is cheaper than a gate that catches drift on the day of the incident.
Non-claims
Three things the clean=0 gate does not give you.
This is a narrow discipline. It is worth stating the non-claims plainly so the gate does not get oversold in either direction.
It is not an audit. The planted leg only catches the bug class the property encodes against the planted defect. Bug classes that no property in the suite encodes are not covered, whether or not the suite is green. A full-surface audit reads code that the property file does not test. These two things are complementary, not substitutes.
It is not a runtime monitor. These properties run pre-deploy, in CI, against a fuzz campaign with a finite budget. They do not watch chain state after deployment. Catching a post-deploy state violation is a different lane: a different cadence, different infrastructure, different signal.
It is not formal verification. A fuzzer that finds zero violations in fifty thousand calls under a campaign is evidence the property holds under that input distribution, not proof that no input violates it. Symbolic and SMT-backed tools (Halmos on the EVM side and Move Prover on the Move side) sit in a different point on the cost/coverage curve. Where they fit, they sit on top of the fuzz layer; they do not replace the planted-twin check that the property is testing what it claims.
What the gate does claim, narrowly: for each invariant class the suite encodes, a property exists
that produces a deterministic violation marker on known-bad code and produces no marker on the clean
reference, asserted on every push. That claim is checkable by git clone and
snforge test. It is also the smallest claim that lets you know, on the day of the push,
that your invariant suite has not silently stopped doing its job.
Repos
Clone it, run both legs, read the markers.
The pattern is in the open under Apache-2.0. Three pointers if you want to lift the shape into your own CI:
caliperforge/cf-invariants-starknetcarries the 2×12 Cairo matrix. Workflow at.github/workflows/ci.yml; references atreferences/. PR #2 (commit0bff2c4) is the first push with both legs asserted; the run page is reachable from the repo's Actions tab.caliperforge/hyperevm-safetycarries the same shape on a Foundry stack: paired clean and planted twins for HyperCore-boundary lending invariants, including the JELLY (March 2025) mark-price manipulation reproduction.caliperforge/cf-invariants-verus-bridge-conservationis a single-property, single-pair reference anchored on the Verus–Ethereum bridge incident of 2026-05-18 (Halborn post-mortem cited in the repo README). It is small enough to read end to end in a session, which is the point if you are deciding whether to adopt the pattern.
To verify the gate without the badge: clone, run the planted leg, confirm you see the violation marker on stdout; switch to the clean leg, confirm the marker is absent and the exit code is zero. That is the whole check. The CI runs the same two commands; everything else is plumbing.
If you adopt this and you would like to compare notes on shapes that did and did not work, the contact for invariant-testing CI discussions is michael@caliperforge.com.