Live verification results — regenerated by CI on every push to main. Every row is a real solver run: safe references must prove, known exploits must produce a counterexample. How it works
| Case | Class | Expected | Result |
|---|---|---|---|
| ✅ TokenPool (safe) | reference | proved | proved |
| ✅ TokenPoolBuggy (missing balance check) | underflow-drain | violated | violated |
| ✅ SafeVault (safe) | reference | proved | proved |
| ✅ ApprovalDrain (missing allowance check) | approval-drain | violated | violated |
| ✅ UnbackedMintVault (infinite mint) | unbacked-mint | violated | violated |
| ✅ BurnDesyncVault (totalShares desync) | accounting-desync | violated | violated |
| ✅ AMMSwap (safe) | amm-reference | proved | proved |
| ✅ AMMPriceManipulation (drain) | amm-manipulation | violated | violated |
| ✅ LendingPool (safe) | lending-reference | proved | proved |
| ✅ LendingUnbackedBorrow (no health check) | lending-unbacked | violated | violated |
| ✅ StakingPool (safe) | staking-reference | proved | proved |
| ✅ StakingInfiniteReward (no balance check) | staking-exploit | violated | violated |
| ✅ OracleSafe (safe) | oracle-reference | proved | proved |
| ✅ OracleManipulation (manipulate) | oracle-exploit | violated | violated |
| ✅ GovernanceTimelock (safe) | governance-reference | proved | proved |
| ✅ GovernanceNoTimelock (no timelock) | governance-exploit | violated | violated |
| Case | Class | Expected | Result |
|---|---|---|---|
| ✅ fei-protocol-reentrancy ($80.0M) | reentrancy | violated | violated |
| ✅ cream-finance-reentrancy ($130.0M) | reentrancy | violated | violated |
| ✅ pancake-bunny-flashloan ($45.0M) | flash-loan | violated | violated |
| ✅ open-leverage-access-control ($0.23M) | access-control | violated | violated |
| ✅ belt-finance-arithmetic ($6.3M) | arithmetic | violated | violated |
| Case | Class | Expected | Result |
|---|---|---|---|
| ✅ UniswapV2Swap | real-contract | proved | proved |
| ✅ UniswapV2SwapCore | real-contract | proved | proved |
| ✅ AaveLending | real-contract | proved | proved |
| ✅ CompoundCToken | real-contract | proved | proved |
| Case | Class | Expected | Result |
|---|---|---|---|
| ✅ PaymentChannel | valuepacket | proved | proved |
| ✅ CrossChainSettlement | valuepacket | proved | proved |
| ✅ SubscriptionManager | valuepacket | proved | proved |