botsec

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