cf-invariants

Stateful invariant testing for Cairo / Starknet contracts, with AI-suggested invariants.

cf-invariants is a sidecar to Starknet Foundry (snforge) that adds two capabilities snforge does not have:

1. Stateful invariant testing — drive sequences of external calls against a deployed contract and check an invariant between every transition. snforge's built-in fuzzer generates random scalar arguments to a single function; cf-invariants generates random sequences of external calls and asserts a property over the resulting state.
2. AI-suggested invariants — given a contract's ABI and storage layout, propose candidate invariants from a versioned library of patterns (conservation, monotonicity, access-control, solvency, etc.). All AI output is labeled [AI-SUGGESTED, UNVERIFIED] until accepted by the developer.

---

Status

Working artifact, pre-1.0. Used to ship the Starknet sepolia reference suite under STARKNET_SEPOLIA_DEPLOYMENTS.md and the matching findings report at STARKNET_SEPOLIA_FINDINGS.md.

What is live in this build:

• cf-invariants version resolves cf-invariants's own semver and detects snforge --version.
• cf-invariants run <scarb-project> parses Scarb.toml, ingests target/dev/*.contract_class.json ABI artifacts, invokes snforge test (or emits an empty scorecard with snforge_version: unavailable if no snforge is on PATH), and writes both scorecard.json and scorecard.md.
• cf-invariants suggest <scarb-project> loads the versioned prompt (prompts/invariant_suggestion_v1.txt), calls the AI module (Anthropic Claude Sonnet 4.6 on the live path, mock transport on the offline demo path), parses the strict-JSON candidate list, enforces the per-call budget cap, writes an audit-log entry, and renders a candidate file carrying the [AI-SUGGESTED, UNVERIFIED] label.
• snforge stdout parser with fixture coverage (PASS / FAIL / IGNORE / fuzz runs / Tests: summary / Fuzzer seed:).
• Scorecard markdown renderer with AI-disclosure line emitted whenever any AI-suggested invariant is included.
• Six reference contracts under references/, each with a planted bug on a different surface and each deployed + source-verified on Starknet sepolia (see STARKNET_SEPOLIA_DEPLOYMENTS.md):
  • erc20_planted_bug/ — ERC20 conservation (manual).
  • governance/ — proposal-vote-execute / access-control monotonicity (AI-suggested, author-accepted).
  • single_side_amm/ — constant-product AMM / k-monotone (AI-suggested, author-accepted).
  • erc4626_ref/ — vault share/asset conservation (AI-suggested, author-accepted).
  • multisig_ref/ — multisig threshold monotonicity (AI-suggested, author-accepted).
  • erc721_ref/ — NFT token-id uniqueness (AI-suggested, author-accepted).
• Cost-budget regression test asserts per-call cost stays under $0.05 and that the 3-contract demo cumulative cost stays under $0.25.
• Fixture-drift CI early-warning test (fixture_drift_*) — fires only when CF_INVARIANTS_SNFORGE_LIVE=1 is set, otherwise greppable canaries run inline against captured fixtures.
• Paired clean / planted CI — every reference runs twice in CI: once on the default (planted) build asserting INVARIANT VIOLATED surfaces and rc != 0, once on --features clean asserting zero markers and rc == 0. Both legs across all 12 references are required for green. See §"Paired clean / planted CI" below.

See docs/architecture.md for the full design. See docs/cookbook/ for the developer cookbook (15-minute quickstart + four archetype walkthroughs + adapt-to-your-protocol guide).

Pinned toolchain

Reproduce-from-fresh-clone is verified against the following pinned versions (see .tool-versions for the asdf-managed pin):

• Cairo 2.18.0
• scarb 2.18.0
• sncast 0.60.0
• snforge 0.61.0 (starknet-foundry)
• Rust 1.79+ stable (workspace Cargo.toml MSRV)

Earlier minor versions of snforge / scarb may work but are not exercised by the fixture-drift CI test.

Install

cargo install --path crates/cf-invariants-cli

Quick start

# Detect snforge version
cf-invariants version

# Ask the AI module for candidate invariants (offline mock by default; set
# CF_INVARIANTS_AI_LIVE=1 + ANTHROPIC_API_KEY to hit the live endpoint).
cf-invariants suggest references/erc20_planted_bug \
  --contract ERC20Ref \
  --prompt prompts/invariant_suggestion_v1.txt \
  --audit-log-dir .cf-invariants/ai-log \
  --out tests/invariants/cf_ai_candidates.md

# Run cf-invariants against a Scarb project (executes accepted invariants
# via snforge and emits a scorecard).
cf-invariants run references/erc20_planted_bug --runs 64 --seed 42 \
  --out scorecard.json

Outputs scorecard.json (CI-consumable) and scorecard.md (human-readable, with an AI-disclosure line whenever any AI-suggested invariant appears).

End-to-end demo (ERC20 planted bug)

# 1. Build the reference contract so target/dev/ ABI artifacts exist.
cd references/erc20_planted_bug && scarb build && cd ../..

# 2. Ask the AI module for candidate invariants on the ERC20 contract.
cf-invariants suggest references/erc20_planted_bug --contract ERC20Ref

# 3. Run cf-invariants against the reference contract (snforge executes
#    the synthesized stateful driver and emits the scorecard).
cf-invariants run references/erc20_planted_bug --runs 64 --seed 42 \
  --out scorecard.json

On the planted-bug variant the scorecard reports invariants_violated: 1 with a counterexample sequence; on the clean variant (snforge test --features clean, or the equivalent scarb build --features clean) all invariants hold. The expected output shape lives at references/erc20_planted_bug/scorecard.expected.md.

Paired clean / planted CI

Every reference under references/*/ ships as a single source tree that compiles to either variant of the planted bug, gated by a clean scarb feature each Scarb.toml declares ([features] clean = []). At the contract level a CLEAN_TWIN: bool const is defined via #[cfg(feature: 'clean')] and the buggy line is wrapped in if CLEAN_TWIN { /* corrected */ } (or its negation, depending on the bug shape). Where a clean-variant fix would make an existing fuzz transition revert (e.g. erc721 mint rejects duplicate token_ids under clean), the test driver mirrors the same feature gate and skips the unsafe transition.

CI runs both legs across all 12 references on every push:

Leg	Build/test command	Assertion
planted	snforge test	rc != 0 AND INVARIANT VIOLATED marker on stdout
clean	snforge test --features clean	rc == 0 AND zero markers on stdout

All 24 invariant legs must pass for the CI run to be green. The single-tree-with-feature-flag shape preserves the existing planted default (so historical deploys, fixtures, and findings READMEs remain bit-identical) while adding the matching clean-twin proof the cf-invariants-anchor / cf-invariants-jito repos ship on the Solana side.

Static analysis pre-flight

Caracal (Crytic's Cairo static analyzer) runs as a separate CI job in advisory mode against all 12 references. Findings are uploaded as artifacts and surfaced in the job log; the job itself never gates merges because the false-positive surface against Cairo 2.18 is not yet pinned. Gating is a follow-up workstream once the suppression set is settled.

What it is not

• Not a fork of snforge. cf-invariants invokes snforge test as a subprocess. We extend, we don't replace.
• Not a formal-verification tool. No proofs, only randomized invariant search.
• Not a coverage-guided fuzzer. Coverage-guided fuzzing for Cairo is a separate problem.
• Not a replacement for snforge's #[fuzzer] tests. cf-invariants is additive.

Architecture

The cf-invariants-ai crate is the AI-suggestion module; the in-repo detail (provenance tagging, audit log, cost budget, how to disable) lives at docs/ai-disclosure.md.

cf-invariants is a Cargo workspace of five Rust crates plus a Cairo dev-dependency package:

crates/
  cf-invariants-cli/           # binary
  cf-invariants-core/          # types + orchestrator trait
  cf-invariants-cairo-meta/    # Scarb.toml + ABI parser
  cf-invariants-snforge/       # subprocess + stdout parser + fixture drift
  cf-invariants-ai/            # Anthropic client + cost budget + mock transport
  cf-invariants-report/        # scorecard renderer
cairo/
  cf_invariants_runtime/       # Cairo dev-dep helpers
prompts/
  invariant_suggestion_v1.txt  # versioned, pinned prompt
references/
  erc20_planted_bug/           # ERC20 + conservation invariant (manual)
  governance/                  # proposal-vote-execute + AC-monotonicity (AI)
  single_side_amm/             # constant-product AMM + k-monotone (AI)
  erc4626_ref/                 # vault share/asset conservation (AI)
  multisig_ref/                # multisig threshold monotonicity (AI)
  erc721_ref/                  # NFT token-id uniqueness (AI)
findings/
  {erc20,governance,amm,erc4626,multisig,erc721}/  # cf-invariants runs + scorecards
scripts/
  deploy_to_sepolia.sh         # declare + deploy reference suite to sepolia

License

Apache-2.0. See LICENSE.

Reporting issues, security contact

Open an issue on the GitHub repository, or email michael@caliperforge.com.

---

cf-invariants is operated by Michael Moffett under the CaliperForge banner. CaliperForge is a sole-operator engineering studio.

Built with AI assistance. Authored and reviewed by Michael Moffett, operator at CaliperForge. Full policy at caliperforge.com/ai-disclosure. See docs/ai-disclosure.md for the in-repo detail on what the AI module does, the audit-log path, and how to disable it.

caliperforge.com