cf-invariants on Starknet Sepolia — twelve references, paired clean/planted CI green.

The suite at twelve

Six new contract families — the most-shipped Cairo shapes not in the original six.

The Day-1 launch post stood up cf-invariants as a Rust sidecar that adds stateful invariant testing on top of snforge for Cairo 2.x, with three Voyager-verified references on Starknet Sepolia. The three-to-nine expansion took the suite to nine on 2026-06-02. As of 2026-06-04 the suite is twelve. The six new families fill in the most-shipped Cairo shapes the original six did not cover.

The original six (per git ls-tree 679a5ac references/ at the OSS-launch commit on 2026-06-01): erc20_planted_bug, erc4626_ref, erc721_ref, governance, multisig_ref, single_side_amm. The six added in this expansion: lending_ref, oracle_ref, payment_splitter_ref, staking_ref, timelock_ref, vesting_ref. All twelve are on-chain on Starknet Sepolia and Voyager source-verified, with addresses + verification links in STARKNET_SEPOLIA_DEPLOYMENTS.md.

One invariant, one planted bug per new family

Each reference is small enough to read end-to-end.

The discipline that carried the original six carries through here: a single hand-authored or AI-proposed invariant per reference, a single planted bug sitting at named lines in src/lib.cairo, and an scorecard.expected.md that names what the harness is expected to surface on the buggy variant.

• lending_ref — per-user solvency. The clean lending market enforces an LTV cap on both borrow and withdraw. withdraw_collateral in the planted variant correctly debits the caller's collateral and total_collateral but skips the post-write LTV re-check; a borrower can borrow up to cap, then withdraw collateral to zero while still holding the quote. The invariant invariant_per_user_solvency fires. (README.)
• staking_ref — stake/slash conservation across the staking pool and the slashed pool. slash(victim) zeroes the victim's stake and debits total_staked but never credits slashed_pool; the slashed funds vanish from accounting. The conservation invariant catches the LHS/RHS drift. (README.)
• vesting_ref — claimed ≤ vested at any time. The clean linear vesting contract gates claim() on vested_at(now); the planted claim() pays out total_grant - claimed regardless of schedule. The first claim before end_ts drives claimed > vested_at(now) and breaks the supply cap. (README.)
• timelock_ref — delay respected. The clean timelock requires now ≥ queued_at(tx_id) + delay at execute time. The planted execute(tx_id) checks admin and tx-existence but drops the delay gate; the admin can queue and execute in the same block. invariant_delay_respected fires. (README.)
• payment_splitter_ref — proportional release. The clean three-recipient splitter pays each caller their share-weighted entitlement. The planted release() pays the caller total_received - released[caller] outright, the entire un-released pool to whoever calls first, ignoring share weights. invariant_proportional_release catches the over-payment. (README.)
• oracle_ref — last_update_ts monotonicity. The clean push-update oracle gates each write on new_ts > last_update_ts; the planted update_price enforces publisher access but skips the freshness check, so a stale push rewinds the freshness clock backward. invariant_last_update_ts_monotone fires. (README.)

Each reference is a single src/lib.cairo plus a single tests/cf_invariant_….cairo driver. The corrected line in each planted variant is preserved in a comment block at the end of the function, so the diff between clean and planted is one paragraph long and readable on a phone.

The CI green light

Paired clean/planted across all twelve, plus a Caracal pre-flight.

The repo did not have a GitHub Actions workflow when the three-to-nine expansion shipped — the proof was local snforge test output plus the Voyager verification links. The first end-to-end CI workflow landed on 2026-06-04 and went green on run 26971094124 at commit 5ac98a9, 13/13 jobs. That first shape asserted the planted leg only: every reference's snforge test was expected to exit non-zero with the INVARIANT VIOLATED marker on stdout. It did not yet assert that the clean twin runs clean.

That gap closed on 2026-06-07 when PR #2 squash-merged. The PR adds a clean scarb feature to every reference's Scarb.toml and a CLEAN_TWIN: bool const gated on #[cfg(feature: 'clean')] in each contract module, so the same source tree compiles in two variants. CI now runs a 24-leg matrix (twelve references × two variants), plus the Rust workspace tests and a Caracal static-analysis pre-flight job in advisory mode. The expectation per leg:

• Planted leg — default scarb build; snforge test is expected to fail with INVARIANT VIOLATED <reason> on stdout. CI inverts the exit code and asserts the marker is present.
• Clean leg — scarb build --features clean + snforge test --features clean. CI asserts rc == 0 AND no INVARIANT VIOLATED marker on stdout.

Run 27075213962 at commit 003e33c is 26 of 26 green: the workspace job, the Caracal advisory job, and the 24 reference legs. The workflow file is .github/workflows/ci.yml and is the substantive reference an external Cairo dev can lift. The clean-variant convention — one clean scarb feature gating one CLEAN_TWIN branch per reference — is the pattern the snforge docs PR #4409 (opened 2026-06-04, pending first-time-contributor maintainer approval) proposes for upstream as a worked recipe. The PR is opened, not merged; the CI on it is pending maintainer approval.

The sibling ship

Third real Jito program harnessed on the same Crucible rails.

One day after the suite expansion, cf-invariants-jito-priorityfee went public — the third real Jito Foundation program harnessed on Crucible, on the same anchor-lang 1.0.1 / platform-tools v1.52 / Crucible v0.2.0 rails as cf-invariants-jito (tip-distribution) and cf-invariants-jito-tippayment (tip-payment). One hand-authored invariant (transfer_increments_total_state_update), paired clean/planted, CI green on the first push at commit a32c1d3, run 26919123180. Three Jito programs, one rail — the specialization-velocity claim as an existence proof, not a forecast. Bundled hand-off via Jito intro issue #163 (opened 2026-06-04, awaiting maintainer reply).

What this is not

Not a fork. Not an audit. Not autonomous discovery. Not formal verification.

Four framings each repo's README is explicit about, mirrored here so this post does not drift:

• Not a fork of snforge. snforge is the stateful-invariant test runner. cf-invariants is the Rust sidecar that orchestrates references, drives the clean-vs-planted twin convention, and scores results. Credit for the Cairo invariant testing engine and the INVARIANT VIOLATED marker contract belongs to the starknet-foundry team. The repo pulls snforge as an external dependency; nothing is vendored.
• Not an audit of these contract patterns. Each reference is a deliberately small implementation shaped around one invariant and one planted bug. The planted bugs are authored in our reference copies for the harness to fire on; no claim is made about the security of any production lending / staking / vesting / timelock / payment splitter / oracle contract on Starknet.
• Not autonomous AI discovery. The invariants in the new six were drafted with AI assistance under operator review, then frozen as hand-authored fixtures — each reference's test-driver header names the AI source and the scorecard carries an AI-disclosure block. The harness is what checks them; no candidate reaches a CI assertion without an operator pass.
• Not formal verification. Stateful randomized invariant testing under snforge's fuzzer budget, not proofs. The CI green light is evidence that the harness surfaces each planted bug within budget on the planted variant and finds no violation on the clean variant — not a proof that no violation exists under any input.

Repo: github.com/caliperforge/cf-invariants. Sepolia deployment + Voyager verification index: STARKNET_SEPOLIA_DEPLOYMENTS.md. Apache-2.0. Issues and PRs are open.

— Michael Moffett. Built with AI assistance; the harness scaffolds, the reference fixtures, and the AI-suggester orchestration were drafted with an AI coding assistant under operator review, with full repo attribution. AI policy at caliperforge.com/ai-disclosure.