Prove your contracts are safe from bugs.

Amounts from the DefiLlama hacks database, on EVM chains since 2016, by its primary class, plus a few large attacks the database misses, recorded by hand from the reports. Incidents link to rekt.news where its archive covers them and to the project's own report where it does not.

Tested on four public research datasets

SmartBugs curated (143 contracts), SolidiFI (50 contracts), Not So Smart Contracts (25 contracts) and Consolidated Ground Truth (1422 contracts), the public benchmarks researchers use to measure security tools.

Vulnerable contracts caught

Contracts the datasets call reentrant. Green is a contract the dataset called safe that Solbend proved reentrant, each attack written out and checked on a test chain.

Safe contracts proven safe

Contracts the datasets call safe, plus generated variants built to be safe. A flag on one is a false alarm, or a pattern Solbend cannot prove yet. Green is a contract the dataset called safe that Solbend proved reentrant, each attack written out and checked. Of the 432 generated variants that are not safe, every one is flagged.

Planted bugs found, by tool

389 exploitable reentrancy bugs planted across 50 real contracts, found by each tool.

Every bug class, not just reentrancy

Solbend can catch different kinds of bugs. Slither has no check at all for 6 of these classes. Mythril has none for 8. Solbend covers every bug class, and where it can, it proves whether the code is safe or not.

The 20 classes are the labelled datasets/classes matrix, run 2026-10-24. Slither 0.11.6 and Mythril 0.24.8 at default settings. The Re-entrancy row is SolidiFI line-level, Mythril from the SolidiFI paper (2020). Solbend's figures are the published 2026-10-24 snapshot.

$ solbend examples/BankDAO.sol

Reentrancy: NOT PROVEN
  ✗ State changed after other code gets control
      withdraw  calls out at BankDAO.sol:16
        then BankDAO.sol:18: balances[msg.sender] = 0
  ✓ Call no untrusted code
      deposit

Invariants: PROVEN without reentrancy
  ✓ sum(balances) <= balance

Counterexample: FOUND  (bend checked it: CEX.bend proves reentrancy_safe false)
    deployed  constructor(), by 0x1
    0x3       deposit(), sending 1 wei
    0x1       deposit(), sending 1 wei
    0x3       withdraw()
                BankDAO.sol:16 sends 1 wei to 0x3, which calls back:
                  0x3  withdraw()
                         BankDAO.sol:16 sends 1 wei to 0x3
  sum(balances) <= balance fails there, and every plain transaction keeps it:
    before  sum(balances) = 2, balance = 2
    after   sum(balances) = 1, balance = 0

$ solbend examples/BankCEI.sol

Reentrancy: PROVEN (bend checked the proof)
  any state that reentrant calls can reach, plain transactions reach too
  ✓ Call no untrusted code
      deposit, transfer
  ✓ Change no state after other code gets control (checks-effects-interactions)
      withdraw  calls out at BankCEI.sol:23

Invariants: PROVEN
  in every state reachable from deployment, with or without reentrancy
  ✓ sum(balances) <= balance

Who can change what  (each restriction proven)
  balances  deposit (only the caller's entry), transfer, withdraw (only the caller's entry)

Funds never stuck
  ✓ balances: withdraw lowers any positive entry of its caller

Every proof and every attack is double-checked by an independent checker.