Autonomous Smart Contract Invariant Fuzzing & SMT Symbolic Prover
Built with Ramanujan Mathematical Rigor, Halmos, Z3/Yices SMT Solvers, and Foundry
InvariantForge is an elite formal verification and autonomous fuzzing engine for Web3 smart contracts. Unlike generic LLM auditors that produce noisy, unverified markdown reports, InvariantForge provides mathematical proof guarantees:
-
Dual Verification Architecture:
-
Stateful Invariant Fuzzing (
forge test): Simulates millions of randomized multi-actor state transitions across bounded sequences to uncover race conditions, reentrancy, and insolvency. -
Symbolic SMT Formal Prover (
halmos+Z3/Yices): Mathematically evaluates EVM bytecodes over the universal input domain ($\forall x \in [0, 2^{256}-1]$ ) to formally prove theorem invariants (UNSAT) or extract counterexample exploit models (SAT).
-
Stateful Invariant Fuzzing (
-
Autonomous PoC Generation:
- When an invariant fails in fuzzing or symbolic execution,
InvariantForgeautomatically synthesizes a standalone, deterministictest_PoC_*.t.solreproducer that runs in$< 5\text{ms}$ with 100% green exit status for direct bounty submission to Cantina / Immunefi.
- When an invariant fails in fuzzing or symbolic execution,
-
Ramanujan Invariant Catalog:
- Out-of-the-box formal properties covering ERC-4626 Vault Dilution, Lending Solvency, AMM Constant Invariants, and Precision Loss.
# Clone repository
git clone https://github.com/Ranjeet2063/InvariantForge.git
cd InvariantForge
# Install Python package and dependencies
pip install -e .
# Install Halmos Symbolic Prover
pip install halmosinvariant-forge rulesFormally proves properties for all possible inputs using Halmos with Z3 or Yices:
# Prove SecureVault with Yices/Z3
invariant-forge prove Vault --solver yices
# Run symbolic proof against VulnerableVault (extracts concrete exploit model)
invariant-forge prove VulnerableVault --solver yicesOutput Preview:
โญโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโฎ
โ ๐ฌ InvariantForge Formal Verifier โ Halmos & SMT Symbolic Engine โ
โ Ramanujan Mathematical Rigor & Universal Input Domain Guarantees โ
โฐโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโฏ
โ Target Contract: Vault
โ SMT Solver Selected: YICES
โก Launching Halmos Symbolic Execution (โ inputs in 2^256)...
Symbolic Proof Telemetry โ Vault
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโณโโโโโโโโโณโโโโโโโโโโโโโโโโโณโโโโโโโโโโโโโ
โ Symbolic Theorem / Invariant โ Result โ Paths Explored โ Proof Time โ
โกโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโฉ
โ check_shares_monotonic_scaling โ PASS โ 7 โ 0.06s โ
โ check_shares_never_zero_for_positiveโฆ โ PASS โ 4 โ 0.02s โ
โ check_zero_assets_zero_shares โ PASS โ 1 โ 0.00s โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโดโโโโโโโโโดโโโโโโโโโโโโโโโโโดโโโโโโโโโโโโโ
โญโโโโโโโโโโโโโโโโโโโโโโโโโ Formal Verification Passed โโโโโโโโโโโโโโโโโโโโโโโโโโฎ
โ โ ALL THEOREMS MATHEMATICALLY PROVEN! (UNSAT) โ
โ โข Verified by SMT Solver: YICES โ
โ โข Total Theorems Proven: 3 โ
โ โข Proof Execution Time: 0.10s โ
โ โข Mathematical Invariant: No state input exists in โ x โ [0, 2^256-1] โ
โฐโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโฏ
# Run 1,000 multi-actor fuzz sequences and auto-synthesize PoC on failure
invariant-forge scan testbed/src/VulnerableVault.sol --runs 1000| Contract | Pattern Analyzed | Invariant Result | Formal SMT Result | Generated Proof Artifact |
|---|---|---|---|---|
VulnerableVault.sol |
First-Depositor Share Inflation | ๐จ BREACHED | ๐จ SAT Counterexample | test_PoC_VulnerableVault.t.sol (100% Green in 2ms) |
SecureVault.sol |
Solady Virtual Decimal Offset | โ PASSED | โ PROVEN (UNSAT) | Formal Certificate of Solvency |
invariant-forge/
โโโ invariant_forge/ # Core Engine
โ โโโ parser.py # Solidity AST & Pattern Extractor
โ โโโ invariant_rules.py # Ramanujan Formal Invariant Catalog
โ โโโ runner.py # Foundry Stateful Test Runner
โ โโโ symbolic_runner.py # Halmos + Z3/Yices SMT Formal Prover
โ โโโ generator/ # Code Synthesis Engines
โ โ โโโ handler_gen.py # Multi-Actor Bounded Handler Synthesizer
โ โ โโโ suite_gen.py # Foundry Invariant Suite Synthesizer
โ โ โโโ poc_gen.py # Standalone PoC Reproducer Synthesizer
โ โโโ cli.py # Unified CLI Interface
โโโ testbed/ # Foundry Testbed Environment
โ โโโ src/ # Verified Protocols (SecureVault, VulnerableVault)
โ โโโ test/ # Invariant & Symbolic Test Contracts
โ โโโ foundry.toml # Foundry & Halmos AST Configurations
โโโ tests/ # Python Unit & Verification Test Suite
โโโ .github/workflows/ci.yml # Continuous Integration Pipeline
InvariantForge is built strictly for authorized white-hat security auditing, protocol defense, and formal verification. All synthesized proofs and test cases verify invariant boundaries to harden smart contracts prior to mainnet deployment.
MIT License. Built with mathematical precision by Ranjeet2063.
