Smart contract security

Prove your contracts are safe from bugs.

Solbend checks every way an attacker could drain your contracts. You get a proof, or the exact line to fix. No specs to write.

01What we solve

Smart contract audits are hard, expensive, and not bulletproof

Everyone finds out the hard way.

125 months 797 exploits $5.57B lost $44M a month

Drained by hackers since 2016

−$5.57B

797 incidents across 7 bug classes

Access control

A function that should have been locked was callable by anyone.

Poly Network 2021

−$611M

Parity Multisig 2017

−$150M

UPCX 2025

−$70M

Munchables 2024

−$62.5M

Parity Wallet 2017

−$30M

Wintermute 2022

−$17.6M

Table

	Stolen
Poly Network	$611M
Parity Multisig	$150M
UPCX	$70M
Munchables	$62.5M
Parity Wallet	$30M
Wintermute	$17.6M

Total drained

−$1.24B

193 incidents since 2016

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.

02Why Solbend

Scanners only flag. We can prove

Other scanners match patterns and leave you to review the noise. Other provers need experts to write specs by hand. Solbend proves or disproves safety for you.

Scanners compared with Solbend
	Other Scanners	Solbend
When code is safe	Nothing matched a known pattern	Proven safe
When code has a bug	Review it by hand	Unproven, with attack if one exists
On safe code that looks risky	Often flagged as a false positive	Proven safe

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.

392/729: contracts, bug sites and incidents flagged
0: marked safe by mistake, every PROVEN reviewed
98%: of exploitable planted bugs flagged at their line

Vulnerable contracts flagged

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

Flagged
Proven safe, label disputed
Not checked
Marked safe

SmartBugs curated

100% 31/31

SolidiFI

100% 50/50

Not So Smart Contracts

100% 3/3

Consolidated Ground Truth

84.3% 129/153

Table

	Flagged	Proven safe, label disputed	Not checked	Total
SmartBugs curated	31	0	0	31
SolidiFI	50	0	0	50
Not So Smart Contracts	3	0	0	3
Consolidated Ground Truth	105	24	24	153

Planted bugs flagged, by tool

389 exploitable reentrancy bugs planted across 50 real contracts, flagged at their line by each tool. A flag is a warning, not a replayed attack.

Slither

100% 389/389

Solbend

97.9% 381/389

Oyente

86.1% 335/389

Securify

83.8% 326/389

Mythril

66.3% 258/389

SmartCheck

0% 0/389

Table

	Flagged	Total
Slither	389	389
Solbend	381	389
Oyente	335	389
Securify	326	389
Mythril	258	389
SmartCheck	0	389

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.

Bug class

Mythril

Slither

Solbend

Re-entrancySolidiFI line-level, 389 exploitable planted bugs, flagged at their line

66%

100%

98%

Access controlprivileged code callable by anyone

31%

46%+7 warnings

Owner trust / rugpullowner can take user value or access. FOUND counts an owner power only where its own script replayed, which the runs of 2026-10-24 did not record

no check

0%+16 warnings

Arbitrary storage writea write reaches any storage slot

70%

40%

0%+8 warnings

Controlled delegatecallcaller chooses the code that runs

89%

100%

0%+9 warnings

Unprotected initializeranyone can set the authority

30%

20%+7 warnings

Uninitialized storage pointera write lands at slot zero

no check

100%

0%+10 warnings

Upgrade storage collisionan upgrade moves a live slot

no check

100%

84%+4 warnings

Show all 21 classes

Unprotected selfdestructanyone can destroy the contract	78%	89%	11%+5 warnings
Approval draina caller spends an allowance it was not given	60%	40%	0%+10 warnings
Oracle manipulationa price can be moved before value moves	no check	no check	0%+14 warnings
Double claimthe same claim pays more than once	0%	no check	0%+9 warnings
Repeatable withdrawala withdrawal can be repeated	25%	no check	13%+7 warnings
Read-only reentrancya view is read while a callback is live	no check	no check	100%
Solvencythe contract cannot pay what it owes	0%	11%	11%+7 warnings
Weak randomnessa caller can predict or choose the outcome	42%	58%	0%+11 warnings
State-variable shadowingtwo declarations disagree	no check	100%	0%+9 warnings
Roundingrounding moves value in the wrong direction	no check	0%	0%+9 warnings
Strict balance equalityforced ETH breaks an equality	no check	100%	0%+13 warnings
Griefing / DoSa caller can block another user	20%	20%	0%+10 warnings
No free lunchvalue is created without a matching debit	11%	no check	11%+6 warnings

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, measured before the build that produced them was recorded.

Method

Measured on the public research datasets above and the labelled class matrix (datasets/classes, 437 contracts, 231 buggy and 206 safe), 2026-10-24. A buggy contract counts for Slither and Mythril when a finding of its class lands in the vulnerable function, or in a function it calls internally. For declaration classes a finding anywhere in the contract counts. Solbend's class figure counts only an attack replayed on the EVM at that function. A detector match, a law refuted without a replay, or an attack that needs another party's step first is a warning, shown apart as the warnings under the figure and never counted as found. The Re-entrancy row is the exception: it counts SolidiFI bugs flagged at their line.
A safe contract Solbend proves reentrant is counted in green, and every one of those proofs was attacked on a test chain. Where a dataset label relies on a low-gas payout, an owner-chosen address or a contract the code creates, the report names it.
Slither 0.11.6 and Mythril 0.24.8 run at default settings. A dash in the table means a tool has no check for that class. Solbend's figures are the published 2026-10-24 snapshot, measured before the build that produced them was recorded.

03How it works

A proof, or a precise warning

Solbend writes the proof itself, nothing for you to write. If it cannot prove a contract safe, it shows exactly where, and on Professional it then hunts for a real attack.

Proven: Re-entering reaches only states that plain transactions reach. Each proof is rechecked by Bend's kernel, proven consistent in Lean.
Not proven: No proof and no confirmed attack. You see where the proof breaks, to review by hand.
Attack found: A confirmed bug, on Professional. Z3 finds the attack, Bend and Lean confirm it.

A contract that uses code Solbend cannot model yet gets no verdict.

exit 1

$ 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

04Pricing

Pay per scan, or per repository

Starter

$199per scan

For public repositories.

One contract on main branch
Download proof files as .tar.gz
Public repositories only

Try now

Professional

$999/month per repo

For smart contract developers and crypto projects.

Every contract on any branch
Finds attack counterexamples
Private repositories
CI integration

Try now

Enterprise

Custom

For auditing firms, security researchers and teams with many projects.

Everything in Professional
Volume pricing
No-source bytecode scan
Priority support

05FAQ

Questions and answers

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 overflows, access control, stuck funds, denial of service, front-running, ERC-20 rules and who can upgrade, and flag risky patterns such as tx.origin checks, weak randomness and unchecked calls.

What if Solbend cannot prove a contract as safe?

Solbend will say so, because it never assumes safety. The result is Not proven, with where the proof breaks. On Professional, Solbend also searches for a real attack, and when it confirms one the result is Attack found, with every call step by step.

Can I check a proof myself?

Yes. Download a scan's .tar.gz proof files and check them with Bend on any machine. With --verdict, Bend's kernel, whose logic is proven consistent in Lean, rechecks them too.

Which Solidity versions are supported?

Solidity 0.4.11 and newer.

Does Solbend support Vyper?

Yes, Vyper 0.2.16 and newer. Solbend proves a Vyper contract from the bytecode Vyper compiles, and replays any attack it finds on that same bytecode. A contract that uses delegatecall is not supported yet, because the code it runs is not known until the call happens.

Are Foundry and Hardhat projects supported?

Yes. Solbend detects a Foundry or Hardhat project and installs its git submodules and npm packages in an isolated sandbox before the scan. Setup commands from a .solbend.yml, or saved for the repository on the dashboard, run there too. Tested on OpenZeppelin, Uniswap v3 and v4, Aave v3, Safe, Compound, Morpho, Solady and Solmate.

Can I run Solbend in CI?

Yes. Install the Solbend GitHub App to get a check on every pull request, or run the solbend-ci command (npx @encribe/solbend-ci) or the encribe/solbend-action GitHub Action from any CI on Professional.

Get Started

Only scan your own repositories. Scanning other code is against our ToS.