Forge Proof
Forge Proof combines Claude Opus with formal verification to find smart contract vulnerabilities with mathematical proof.
Core trick
Claude writes Halmos symbolic tests from a threat model so an SMT solver proves invariants or returns concrete counterexamples.
Description
Forge Proof combines Claude Opus with formal verification to find smart contract vulnerabilities with mathematical proof.
One command runs a two-stage agentic pipeline on the Claude Agent SDK with specialized sub-agents, constrained tools per agent, structured JSON output, and Skills for preloading FV domain knowledge:
Threat Model — An Opus agent explores the codebase using pre-computed static analysis (call graphs, CEI ordering, auth checks, AST), identifies threats from attacker perspectives, and outputs a ranked threat model with code traces.
Analyze — A second Opus agent writes formal verification tests, runs SMT solvers across all possible inputs, interprets counterexamples to distinguish real bugs from bad specs, and falls back to fuzz testing when the solver hits bounds.
Tested against 3 production DeFi protocols with active bug bounties: 41 formally verified proofs and 4 violations with concrete counterexamples. Total cost: ~$47. Vulnerabilities were responsibly disclosed
README excerpt
# Forge Proof
AI-powered smart contract security analysis with formal verification. Uses Claude Opus with 1M context + Halmos symbolic execution to find real bugs with mathematical proof, not pattern matching.
```
___ ___ __
/ __\___ _ __ __ _ ___ / _ \_ __ ___ ___ / _|
/ _\/ _ \| '__/ _` |/ _ \ /_)/ '__/ _ \ / _ \ |_
/ / | (_) | | | (_| | __/ ___/| | | (_) | (_) | _|
\/ \___/|_| \__, |\___\/ |_| \___/ \___/|_|
|___/
```
## Benchmark: Damn Vulnerable DeFi — 18/18 Challenges Found
Tested against [Damn Vulnerable DeFi v4](https://www.damnvulnerabledefi.xyz/) — the industry-standard benchmark for smart contract security tools.
```
Score: 18/18 challenges — 100% detection rate (19 threats, 2 on Shards)
Halmos Proofs: 16 vulnerabilities with concrete counterexamples
Verified Safe: 8 properties mathematically proven to hold
Zero Timeouts: All 24 symbolic tests completed within solver bounds
Cost: $10.81 ($4.18 threat model + $6.63 verification)
Runtime: ~2 hours
```
### Per-Challenge Results
| # | Challenge | Severity | Verification | Method | Properties | Status |
|---|-----------|----------|-------------|--------|------------|--------|
| 1 | Unstoppable | High | Donation breaks flash loan invariant | Halmos | 3 (1 violation, 2 verified) | PROVEN |
| 2 | Naive Receiver | Critical | Multicall msg.sender spoofing | Code review | — | CONFIRMED |
| 3 | Truster | Critical | Arbitrary call