EncribeSmart contract security
Prove your contracts are safe from reentrancy.
solbend checks every way an attacker could gain control of your Solidity code. You get a proof, or the exact line that breaks the assumptions. Fully automatic, with no specs or lemmas to write.
$458M drained from crypto projects by reentrancy since 2016
01What we solve
The oldest vulnerability in Solidity language is still unsolved.
Reentrancy is like an ATM that hands you cash before updating your bank balance, allowing a fast thief to keep asking for withdrawals mid-transaction until all the funds are gone. It has happened 63+ times since 2016.
The largest reentrancy attacks
Value stolen at the time. Each name links to the incident's write-up.
Table
| Stolen | |
|---|---|
| Fei Rari | $80M |
| Curve | $69.3M |
| The DAO | $60M |
| GMX | $42M |
| Grim Finance | $30M |
| Penpie | $27M |
| Lendf.Me | $25M |
| Cream Finance | $18.8M |
| Agave and Hundred Finance | $11.7M |
| Origin Protocol | $8M |
| BurgerSwap | $7.2M |
| Conic Finance | $4.2M |
| Voltage Finance | $4M |
| dForce | $3.7M |
| EraLend | $3.4M |
| Orion Protocol | $3M |
| Stars Arena | $2.9M |
| Solv | $2.7M |
| Revest Finance | $2M |
| Akropolis | $2M |
| GemPad | $1.9M |
| Sovryn | $1.1M |
| Sturdy Finance | $0.8M |
| Midas Capital | $0.7M |
| Clober | $0.5M |
Sources: rekt.news leaderboard, with The DAO and Lendf.Me from CoinDesk and Decrypt. Totals from the DeFiLlama hacks database.
02Why we're better
Scanners only flag. We can prove.
Scanners like Slither are fast and cover many bug types. solbend goes beyond static analysis and can prove absence or presence of bugs. Other formal tools can prove too, but need experts to write specs by hand, while solbend does it automatically.
| Other Scanners | solbend | |
|---|---|---|
| When no issues are found | Nothing matched a known pattern | Proven safe |
| When an issue is found | Review it by hand | The exact line, and the attack if one exists |
| On safe code that looks risky | Often flagged as false positive | Cleared |
| Covers | Many bug types, in seconds | Reentrancy, in depth, in minutes |
Tested on three public research datasets
SmartBugs curated (143 contracts), SolidiFI (50 contracts) and Not So Smart Contracts (25 contracts). Collections of known-vulnerable contracts that researchers use to measure security tools.
84 /85- vulnerable contracts caught
- 0
- marked safe by mistake
97% - of exploitable planted bugs found
Vulnerable contracts caught
Contracts each dataset lists as open to reentrancy.
- Caught
- Not checked
- Marked safe
Table
| Caught | Not checked | Marked safe | Total | |
|---|---|---|---|---|
| SmartBugs curated | 31 | 0 | 0 | 31 |
| SolidiFI | 49 | 1 | 0 | 50 |
| Not So Smart Contracts | 4 | 0 | 0 | 4 |
Planted bugs found, by tool
389 exploitable reentrancy bugs planted in 50 real contracts (SolidiFI).
Table
| Found | Total | |
|---|---|---|
| Slither | 389 | 389 |
| solbend | 379 | 389 |
| Oyente | 335 | 389 |
| Securify | 326 | 389 |
| Mythril | 258 | 389 |
| SmartCheck | 0 | 389 |
Every bug class, not just reentrancy
SolidiFI plants seven bug types across these 50 contracts. Share of planted bugs each tool catches, scored line by line. solbend and Slither both re-run locally (2026-10-10).
| Bug class | Slither | solbend |
|---|---|---|
| Re-entrancy (re-enterable .call bugs) | 100% | 97% |
| Overflow-Underflow | 0% | 30% |
| TOD | 0% | 100% |
| Timestamp-Dependency | 82% | 100% |
| Unchecked-Send | 100% | 100% |
| Unhandled-Exceptions | 67% | 100% |
| tx.origin | 100% | 100% |
Method
- solbend ff7351a, 2026-10-10, default settings. 212 of 218 contracts could be checked. Not So Smart Contracts' DAO.sol predates Solidity 0.4 and runs with --port-legacy.
- Datasets:SmartBugs curated 230e649 (140 of 143 checked), SolidiFI 4b0573e (49 of 50 checked), Not So Smart Contracts 020dbdb (23 of 25 checked).
- Slither was re-run locally (2026-10-10) and finds every planted bug. The other tools' numbers are the reports published with SolidiFI (2020), scored the same way (a bug counts as found when the report points inside it); Oyente, Securify, Smartcheck and Manticore are unmaintained, so those remain current.
- Across all seven SolidiFI bug classes, solbend and Slither were both re-run locally (2026-10-10); the table above is the share of planted bugs each catches, scored line by line. Slither has no detector for integer overflow or transaction ordering on these pre-0.8 contracts, so it scores zero there. Mythril, a bounded symbolic executor, is slow and timeout-sensitive: the 2020 SolidiFI paper measured it at 66% on reentrancy, and it flags none of these overflow patterns even with a generous budget.
- Counting all 1,343 planted bugs, solbend finds 28% and Slither 100%. The other 954 use send() or transfer(), which pass too little gas to call back in, so solbend treats them as safe. Manticore was tested on a different set and is not shown.
- Not checked:
parity_wallet_bug_2.sol(model too large for Bend to check),0x663e…14c3.sol(assigns a fixed-size array struct member),buggy_24.sol(emitter stack overflow),list_dos.sol(does not compile on any 0.4 solc).
03How it works
A proof, or a precise warning.
solbend writes the proof itself, with no annotations from you. If it cannot prove a contract safe, it shows exactly where, then looks for a real attack.
- Proven safe
- A checked proof that calling back in reaches nothing normal use could not already reach.
- Not proven
- solbend could not prove it. You get the function, the external call and the state it changes afterwards.
- Attack found
- solbend then searches for a real attack. When one exists, you get every call, step by step.
A contract that uses code solbend cannot model yet gets no verdict. That was 6 of 218 in testing.
$ 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 other 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 other 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.
04Pricing
Pay per project.
Professional
$999per month
For smart contract developers and crypto projects.
- Every contract in a repository
- An automatic reentrancy proof, or the exact line in the way
- Working attack replays
- Accounting, stuck funds and upgrade checks
- Private repositories
Enterprise
Custom
For auditing firms and teams with many projects.
- Everything in a project scan
- Volume pricing
- Your own rules, proven
- Runs in your own infrastructure
- Priority support
05FAQ
Questions, answered.
Do I need to write specs or proofs?
No. Unlike Certora prover, solbend generates invariants and proofs automatically. You just connect a repository and pick a branch.
What does solbend check?
It specializes in reentrancy and checks it in depth. Scans also cover accounting, access control, stuck funds and upgrades.
What if it cannot prove a contract safe?
It says so. It never assumes safety. You get the function, the external call and the state it changes afterwards, and a real attack when one exists.
Can I check a proof myself?
Yes. Download a scan's .tar.gz proof files and run them with Bend's formal verification on any machine.
Is my code safe with solbend?
solbend only reads repositories you administer. Your code is never run.
Which Solidity versions are supported?
Solidity 0.4.11 and newer.