The structure
A clean pair is two contracts and one test file.
CaliperForge harnesses ship the same structural unit. Take a contract that is supposed to satisfy some rule , a conservation law, an access control, a solvency bound. Write the clean version: the version that actually satisfies it. Write the planted version: the same contract, with exactly one defect injected that breaks the rule. Keep the test file byte-identical between the two. Run the same invariant property against both.
The expected outcome:
- Clean leg: zero violations. The property holds. The fuzzer does not find a counterexample.
- Planted leg: at least one violation, with a counterexample. The same property, against the same inputs, finds the defect.
CI asserts both outcomes on every push. A green badge on the matrix means both legs passed: the clean side held, and the planted side actually broke when it should. Either leg’s failure is a real regression: the invariant started passing on a broken implementation, or it started failing on a correct one.
The deterministic violation record is the checkable artifact ,
an INVARIANT VIOLATED marker on stdout in the
Foundry-twin repos, a scorecard recording the violation count
in the Echidna-campaign repos. Anyone who clones the repo and runs
the planted campaign target gets the same result without
installing CI, without trusting a badge, without reading the
property description in prose. The record is the evidence.
Why both legs
A passing clean is only half the claim.
A property test that passes on the clean reference tells you the fuzzer did not find a counterexample under the campaign budget. That is a useful signal. It is not the full claim.
The planted twin answers the question the clean leg cannot: does the property actually catch the bug class it is supposed to catch? A property that passes on both the clean and the planted implementation is a broken property, it is not testing what it claims to test. By requiring the planted leg to fire, the methodology keeps the test honest. The harness is only as good as its ability to break on known-bad code.
This is the invariants-as-tests pattern Trail of Bits’ Building Secure Smart Contracts corpus teaches, and ChainSecurity’s published findings reinforce: the value of an invariant is not the moment you state it; it is the loop you wire it into so it gets re-checked on every subsequent change. The planted twin is the loop’s self-check.
Worked example
From hyperevm-safety v0.1 to M2 in the same week.
The current portfolio illustrates the pace.
hyperevm-safety
v0.1 shipped with six HyperCore-boundary invariants as
CI-runnable property tests. At v0.1, the JELLY (Mar 2025) mark-price manipulation
reproduction shipped as a clean / planted twin against
a minimal lending-market reference, and the precompile gas DoS
and CoreWriter solvency window classes carried inline
broken-reference tests demonstrating the bug class
deterministically.
Planted twins for D-3 SzDecimalsRoundTrip and
D-6 ChainlinkAdapterDefeatsStaleness were
listed as M2 roadmap at the v0.1 flip. They shipped the same
day. The updated state, from the README’s callout:
three marker-firing counterparts now run on the same CI run:
the D-3 SzDecimalsRoundTrip and
D-6 ChainlinkAdapterDefeatsStaleness planted twins
(landed M2) and the JELLY (Mar 2025) mark-price
manipulation reproduction (covering D-1 OracleStaleness
and D-2 OracleDeviation against a minimal lending-market
reference). D-4 PrecompileGasDoS and
D-5 CoreWriterSolvencyWindow carry inline broken-reference
tests that demonstrate the bug class deterministically, with
marker-armed properties whose planted hunks are documented in
NatSpec but not yet wired as CI-firing twins.
The same week,
cf-invariants-verus-bridge-conservation
shipped: a bridge-class reference anchored on the
Verus–Ethereum bridge exploit of 2026-05-18 (reported
losses USD 11.58M, per Halborn’s post-mortem). The
conservation rule existed in the bridge’s spec as prose.
It was never expressed as a machine-checkable invariant. This
repo is what lifting it looks like: one property, two
contracts, one CI matrix.
The pattern is the same in each case. Same-source twin. One localized planted change. Byte-identical test file. Both legs asserted in CI.
What this is not
Not an audit. Not a runtime monitor. Not formal verification.
The planted-twin methodology is a pre-deploy CI gate. Three non-claims worth stating plainly.
Not an audit. An audit covers the full protocol surface: all state transitions, all roles, all edge cases the auditor can identify. A planted-twin harness covers the invariant classes it encodes. A passing CI run on a fork of one of these repos against a production protocol does not certify the protocol is safe. The residual surface , the bug classes the properties do not encode, is the protocol’s.
Not a runtime monitor. These properties run pre-deploy in CI, against a fuzz campaign, before code goes live. They do not watch the chain after deployment. The monitoring lane belongs to a different class of tool.
Not formal verification. Coverage-guided fuzzing under a campaign budget is not exhaustive. Finding zero violations in 50,000 calls is evidence the rule holds under that surface; it is not a proof. Halmos symbolic specs and Certora CVL specs are on the roadmap for future work; they are not in-tree today.
What the methodology does claim: for the invariant classes it
encodes, a runnable property exists that surfaces a deterministic
violation on known-bad code and
holds on the clean reference, in CI, on every push. That
claim is checkable by anyone who can run
git clone.
Repos
Apache-2.0. Run it locally.
The full portfolio is on the CaliperForge GitHub org. Two repos from the worked example above:
- caliperforge/hyperevm-safety , HyperEVM lending invariants. Six HyperCore-boundary classes; three marker-firing planted or incident-reproduction twins now in-tree (D-3 SzDecimalsRoundTrip, D-6 ChainlinkAdapterDefeatsStaleness, JELLY reproduction). Apache-2.0.
- caliperforge/cf-invariants-verus-bridge-conservation , bridge conservation invariant reference, anchored on the 2026-05-18 Verus–Ethereum exploit. One property, two contracts, CI matrix. Apache-2.0.