ProofForge

AI-written financial code that ships with a proof.

Meta's Muse Spark, with Muse Wonder planning the hardest proofs, writes and repairs the logic behind real financial failures, from DeFi exploits to the Knight Capital trading loss, and proves every locked requirement in Lean 4. ProofForge rechecks each proof in a fresh sandbox and issues a Passport. No proof, no merge.

IncidentTaken or lostProved for every inputVulnerable codeMuse repairPassport
Cetus, 2025DEX liquidity mathAbout $223 milliontakenThe overflow check never loses a bit, so a deposit is always charged at least the exact amount it owes.REFUTEDcounterexampleVERIFIED5 of 5 requirements 9131dfdfd3e2
Balancer V2, 2025AMM swap roundingMore than $120 millionacross Balancer and its forksFor any pool math meeting the stated contract, no batch of swaps of any length lowers the pool's value.REFUTEDcounterexampleVERIFIED8 of 8 requirements 48930efdd4d6
Euler Finance, 2023Lending solvencyAbout $197 millionin net profit to the attackerNo sequence of operations leaves any account with more debt than its risk-adjusted collateral.REFUTEDcounterexampleVERIFIED6 of 6 requirements 6de7bb94c38c
Knight Capital, 2012Equity order routing, reconstructed from the SEC order$460 millionrealized lossOn every server and code version, after any sequence of events, the shares sent for an order never exceed its quantity.REFUTEDcounterexampleVERIFIED6 of 6 requirements 98cfed64ae1e
Hundred Finance, 2023Vault share accountingAbout $7 millionin reported lossesNo sequence of operations, donations included, lowers the value of a share while shares are outstanding.REFUTEDcounterexampleVERIFIED10 of 10 requirements 08fe86f17f27

Muse Spark 1.3 wrote each accepted repair, for $0.19 to $4.96 at list prices; for Balancer V2 and Knight Capital, Muse Wonder 1.0 planned the proof. Lean proves the ports, repairs and implementations, not the deployed code: what is and is not proved.

Open the Cetus PassportOpen the live forge sessionRead the results

Balancer V2, Euler Finance, Knight Capital and Hundred Finance, step by step

Balancer V2, 2025

More than $120 million across Balancer and its forks, as OpenZeppelin reports; The Block reports estimates of over $128 million. OpenZeppelin, The Block, Certora

A swap for an exact amount out rounded that amount down before pricing it, so 17 wei of osETH, worth 17.988 of the pool's units, was priced as 17.

Certora writes that its 2022 verified properties of these pools “did not constrain the relationship between individual swaps or rounding behavior”. The locked requirements here are about exactly that.

The attack, with the state after each step

  1. The attacker sells BPT for the pool's tokens, 22 swaps in one batch. BPT swaps, joins and exits are not modeled.67,000 wei of WETH and 67,000 of osETH
  2. It takes osETH out until 18 wei are left.
  3. It takes 17 wei of osETH out. At the cached osETH rate that is 17.988 of the pool's units; the pool rounds it down and prices 17.
  4. It takes WETH out, paid with osETH, and repeats the three swaps, 30 rounds in all.889 wei of WETH and 1,472 of osETH
  5. It buys BPT back at the collapsed price. This step is not modeled; the specification states the property it relied on.
REFUTEDDeployed swap path of the osETH/WETH pool

The kernel checks that four rounds of these swaps lower the pool's value from 4,749,898,000 to 297,229,191, and that the port, run with a port of StableMath, charges exactly the logged amount of all 90 swaps of the attack.

Kernel-checked counterexample and Passport d65bd405a13b

VERIFIEDMuse Spark 1.3 repair, planned by Muse Wonder 1.0

The repair rounds the amount out up before pricing it and refuses the swap unless that amount is below the pool's balance. It proves all 8 requirements, among them that for any pool math meeting the stated contract, no batch of swaps of any length lowers the pool's value. Attempt 1, 2,344 s, $2.51 at list prices.

Passport 48930efdd4d6

Against the real Solidity code

On a fork of Ethereum taken just before the attack transaction, the attack's first 22 swaps brought the deployed pool to 67,000 wei of each token, as on chain. Then 501 batches (the attack's 90 swaps and 500 generated, 10,385 swaps in all) ran through the deployed Vault, the Lean port and the Muse repair.

  • Deployed Vault and osETH/WETH poolthe pool's invariant falls in 56 batches, and its BPT price with it
    56 of 501
    56 of 501 batches break a requirement
  • Muse repairthe proved component on the same 501 batches
    0 of 501
    0 of 501 batches break a requirement

The real code's output equals its Lean port's on every one of the 501 batches. Recorded violations restated as Lean goals and checked in the kernel: 6 of 6. Report

Euler Finance, 2023

About $197 million in net profit to the attacker, as Cyfrin reports; CoinDesk later reported that all recoverable funds were returned. Cyfrin, Zellic, CoinDesk

donateToReserves moved an account's collateral to the reserves without the liquidity check that withdraw, mint and transfer perform.

The attack, with the state after each step

  1. A lender deposits 8,904,507.
  2. The violator deposits 20,000,000, then mints 200,000,000, repays 10,000,000 and mints 200,000,000.collateral 420,000,000, debt 390,000,000: healthy
  3. The violator donates 100,000,000 eTokens to the reserves. No liquidity check runs.collateral 320,000,000, debt 390,000,000: unhealthy
  4. A second attacker account liquidates 256,000,000 of the debt at the 20% maximum discount.violator: collateral 0, debt 134,000,000
  5. The liquidator withdraws the whole pool, 38,904,507: the lender's entire deposit.
REFUTEDEuler v1 at b1ee326

The kernel checks every state above and that NoBadDebt, StaysHealthy and ActorHealthy are false for the port: 134,000,000 of debt is left with no collateral behind it.

Kernel-checked counterexample and Passport cec7d847f1d0

VERIFIEDMuse Spark 1.3 repair

The repair adds the health check to the donation guard. It proves all 6 requirements, among them that no sequence of operations leaves any account with more debt than its risk-adjusted collateral. Attempt 1, 1,682 s, $0.83 at list prices.

Passport 6de7bb94c38c

Against the real Solidity code

The unmodified contracts at b1ee326 were deployed in a local Foundry test and run on the attack, Euler's three donate test scenarios and 1,000 generated sequences, then compared after every operation with the requirements, with Euler's own liquidity computation and with the Muse repair.

  • Euler v1 at b1ee326, unmodifiedEuler's own liquidity check also reports collateral below liability in 57
    57 of 1,004
    57 of 1,004 sequences break a requirement
  • The same with checkLiquidity(account) addeda local copy, not an upstream release
    0 of 1,004
    0 of 1,004 sequences break a requirement

Recorded violations restated as Lean goals and checked in the kernel: 2 of 2. Report

Knight Capital, 2012

$460 million realized loss, as the SEC order states. SEC order 34-70694, archived copy

New code was not copied to one of eight servers. There, orders carrying a repurposed flag ran dead Power Peg code, which kept sending child orders without counting the executions.

The SEC order reports millions of child orders for 212 parent orders: 4 million executions in 154 stocks, more than 397 million shares, in about 45 minutes.

The attack, with the state after each step

  1. Seven of eight servers run the new code; the eighth still runs the old code (paragraph 15).
  2. A parent order for 100 shares arrives with the repurposed flag, which on the eighth server activates Power Peg (paragraphs 13 and 16).
  3. A routing opportunity for 100 shares arrives. The router sends a 100-share child order, and it is filled.100 of 100 shares executed
  4. Power Peg's count never sees the fill, so the next opportunity sends another 100 shares, and so on for every opportunity.after n rounds: n child orders, 100 × n shares executed
REFUTEDReconstructed Power Peg router

The kernel proves by induction that the reconstructed router sends n child orders for one 100-share order, for every n, while the new code sends exactly one on the same events. It also refutes the obvious patch: counting fills again still sends 200 shares for a 100-share order when two opportunities arrive before a fill.

Kernel-checked counterexample and Passport ca3e7312fe7a

VERIFIEDMuse Spark 1.3 repair, planned by Muse Wonder 1.0

The repair removes the Power Peg path, so every build routes by the shares not yet sent and every fill advances the executed count. It proves all 6 requirements, among them that on every server and code version, after any sequence of events, the shares sent for an order never exceed its quantity. Attempt 2, 4,079 s, $4.96 at list prices.

Passport 98cfed64ae1e

UNRESOLVEDEarlier attempts: tests passed, no Passport

Three earlier Muse attempts produced code whose rebuilt executable passed all 2,001 property cases, but none proved every requirement, so ProofForge issued no VERIFIED Passport: A1, attempt 1 proved 1 of 6 before its wall-clock cap; A1, attempt 2 proved 1 of 6 before its dollar cap; and A2, attempt 1 proved 5 of 6 before its dollar cap.

A1, attempt 1 4fddc1683956, A1, attempt 2 27f4c83221ed, A2, attempt 1 edc4ec8cd40a

Hundred Finance, 2023

About $7 million in reported losses (rekt.news gives $7.4M; this figure was not checked here). rekt.news, BlockSec

redeemUnderlying rounded the shares burned down, so a withdrawal worth 1.99999999992 share units burned 1.

The attack, with the state after each step

  1. The market is emptied: no shares outstanding, 1 satoshi of cash.
  2. The attacker deposits 400,000,000 satoshi (4 WBTC).20,000,000,000 share units
  3. It redeems 19,999,999,998 share units.2 share units backed by 1 satoshi
  4. It sends 50,030,063,816 satoshi straight to the market, so each unit is worth about 250 WBTC, and borrows ETH against its 2 units. Borrowing is not modeled.2 share units backed by 50,030,063,817 satoshi
  5. It withdraws 50,030,063,815 satoshi, worth 1.99999999992 share units. The contract burns 1.1 share unit backed by 2 satoshi
REFUTEDHundred hToken share accounting

The kernel checks that the port breaks REQ-SHARE-VALUE (a share falls from 50,030,063,817 / 2 satoshi to 2) and REQ-WITHDRAW-ROUNDS-UP. The Muse repair burns both share units.

Kernel-checked counterexample

VERIFIEDMuse Spark 1.3 repair

The repair prices shares from the exact ratio of assets to supply and rounds the shares burned up. It proves all 10 requirements, among them that no sequence of operations, donations included, lowers the value of a share while shares are outstanding. Attempt 1, 1,200 s, $0.65 at list prices.

Passport 08fe86f17f27

Against the real Solidity code

On a fork of Optimism at block 90761917, the hWBTC market was emptied as in the attack, and 501 sequences (the attack and 500 generated) ran on the deployed CErc20Delegate bytecode, on the Lean port and on the Muse repair.

  • Deployed hWBTC contractidentical to the Lean port after every operation of all 501
    292 of 501
    292 of 501 sequences break a requirement
  • Muse repairthe proved component, on the same 501 sequences
    0 of 501
    0 of 501 sequences break a requirement

The real code's output equals its Lean port's on every one of the 501 sequences. Recorded violations restated as Lean goals and checked in the kernel: 5 of 5. Report

What is proved, and what is not

Proved

  • Each requirement is a Lean 4 statement about the Lean port of the vulnerable logic, locked by hash. A VERIFIED requirement holds for every input, not a sample.
  • A VERIFIED status comes only from ProofForge's own check: lake comparator --paranoid with six kernels in a fresh sandbox, leanchecker, an axiom audit, and property tests on the executable rebuilt from the same source.
  • Each REFUTED port has a counterexample checked by the Lean kernel.

Not proved

  • The deployed Solidity and Move code is not itself proved.
  • The Lean ports are reviewed hand translations. They are tested against the real code on the stated inputs (2,007 inputs for Cetus, 501 batches for Balancer V2, 1,004 sequences for Euler Finance and 501 sequences for Hundred Finance); the translation is not machine-checked.
  • Each port models only the logic its task README names: for example, Euler has one asset and no interest, and Hundred's borrowing is not modeled.
  • Knight Capital is reconstructed from the SEC's findings (Release No. 34-70694) because Knight's code is not public; nothing in the task is Knight's code, and every Knight Passport says so.
  • Loss figures are quoted from the sources each task README cites.

How a repair counts

  1. LockThe owner's requirements, hashed.
  2. RepairA Muse model fixes the code and proves each one.
  3. CheckFresh Comparator, kernel replay and property tests.
  4. PassportStatuses come only from that check.

The benchmark: 59 repair tasks in six areas

Beyond the incidents, the benchmark has 23 development, 6 validation and 30 test tasks. The test areas never appear in development or in any prompt used to build the agents. Every task has two reference solutions, a buggy start candidate and seeded attacks.

Seeded bad repairs accepted, out of 247

E2 checks the same candidate artifacts three ways.

  • Ordinary checkingThe project builds, theorem names are present, the axiom audit is clean.
    233 of 247
  • Rebuild and property tests onlyThe executable rebuilt from the locked project passes the task's property tests.
    1 of 247
  • ProofForgeTree check, implementation scan, Comparator in a fresh sandbox, leanchecker, rebuild and tests.
    0 of 247

Correct repairs rejected: 0 of 239 by every method. The one bad repair the tests accept drops the remainder for seven or more recipients; the test generator never produces more than five. Every bad case is a seeded attack written by the build team, so these counts describe this suite, not repairs in general.

Test tasks repaired by Muse Spark 1.3, out of 30

E1 runs three agent setups on the frozen test tasks under the same budget.

  • A0: Compile-and-retryMuse Spark sees Lean errors and the axiom audit only.
    28 of 30
  • A1: ProofForge harnessBehavior first, one dialog per proof obligation, snippet checks and property tests.
    30 of 30
  • A2: Harness and plannerA1 with Muse Wonder proposing helper lemmas.
    30 of 30

A repair counts when the judge accepts the final candidate and its rebuilt executable passes 2,000 property cases. The arms do not differ significantly (McNemar exact p = 0.50 for A1 or A2 against A0), so this shows that Muse Spark reliably produces repairs that pass the check, not that one setup beats another. The 90 runs cost $70.09 at standard list prices.

The smallest task: a payout splitter pays 100 cents to three recipients. The code under repair loses a cent while each share looks right; Muse Spark's proved repair conserves the total.
= 99REFUTED
= 100VERIFIED

Released bugs in Spliit, go-money and moneyphp

These bugs shipped in released versions of open-source money code. Each release's own code, at a pinned commit, was run on generated inputs and its outputs compared with a reference implementation whose requirements are proved in Lean 4. The projects' code was tested against the proved reference; it was not itself proved.

Spliit

Function getBalances (src/lib/balances.ts), tested at 2 releases.

  • 1.21.03659d7c241REFUTED

    Released with the bug. 977 of 2,001 inputs violate a requirement.

    Example: 100 allocated by ratios 1, 1, 1, violates REQ-CONSERVATION, confirmed in Lean

    Release output
    sum 99
    Proved reference
    sum 100
  • 1.22.0c3d8d3e505PASS

    The fixed release. 0 of 2,001 inputs violate a requirement.

Proved reference: Muse repair repair-A2-3 (Passport 6ae5595df2f580ad). Lean confirms 2 of 2 recorded violations. ProofForge refutes 1 of 1 Lean ports of the buggy releases, each with a kernel-checked counterexample. Reports: issue 374, issue 547, pull request 562.

Rhymond/go-money

Function Money.Split (money.go), tested at 3 releases.

  • v1.0.32e1877f22fREFUTED

    Released with the bug. 750 of 2,002 inputs violate a requirement.

    Example: -101 split 4 ways, violates REQ-VALID-SUCCEEDS, confirmed in Lean

    Release output
    panic: runtime error: index out of range [4] with length 4
    Proved reference
    sum -101
  • v1.0.5e8fc0e2828REFUTED

    Released with the bug. 110 of 2,002 inputs violate a requirement.

    Example: -2 split 3 ways, violates REQ-CONSERVATION, confirmed in Lean

    Release output
    sum 2
    Proved reference
    sum -2
  • v1.0.6affffaf9f8PASS

    The fixed release. 0 of 2,002 inputs violate a requirement.

Proved reference: Muse repair repair-A2-1 (Passport b336a739207fe2d6). Lean confirms 9 of 9 recorded violations. ProofForge refutes 2 of 2 Lean ports of the buggy releases, each with a kernel-checked counterexample. Reports: pull request 94, issue 106, pull request 107.

moneyphp/money

Function Money::allocate (src/Money.php), tested at 4 releases.

  • v3.0.91507938933REFUTED

    Released with the bug. 1,344 of 2,003 inputs violate a requirement.

    Example: 5 allocated by ratios 0, 7, 3, violates REQ-WITHIN-ONE-UNIT, confirmed in Lean

    Release output
    sum 5
    Proved reference
    sum 5
  • v3.1.0ec7a460336REFUTED

    Released with the bug. 1,314 of 2,003 inputs violate a requirement.

    Example: 1 allocated by ratios 1, 1, violates REQ-VALID-SUCCEEDS, confirmed in Lean

    Release output
    ErrorException: Undefined offset: 2
    Proved reference
    sum 1
  • v3.2.053ce6e4b9aREFUTED

    Released with the bug. 1,312 of 2,003 inputs violate a requirement.

    Example: 9999 allocated by ratios 75, 25, violates REQ-LARGEST-REMAINDER, confirmed in Lean

    Release output
    sum 9999
    Proved reference
    sum 9999
  • v3.2.1f6085de6c5PASS

    The fixed release. 0 of 2,003 inputs violate a requirement.

Proved reference: build-team reference (reference/SolutionA.lean). Lean confirms 16 of 16 recorded violations. ProofForge refutes 3 of 3 Lean ports of the buggy releases, each with a kernel-checked counterexample. Reports: issue 436, issue 466, pull request 467, pull request 492, pull request 526.

Check the evidence yourself

Open the Cetus PassportStatuses for all 5 requirements, hashes, kernels, axioms and the command that reproduces it. sha256 9131dfdfd3e27da8Open the live forge sessionReplay a recorded Muse Spark repair, then watch a fresh check of its final candidate assign every status.Read the resultsE1 and E2 per arm, per task family and per case, with the seeded attacks named.

Reproduce a Passport

From a clone of the repository with the pinned Lean image built (see the README). verify rebuilds the project, reruns every check and compares each hash and status.

bin/proofforge verify results/cetus-1/repair-A1-1/passport.json --candidate results/cetus-1/repair-A1-1/final.lean
bin/proofforge verify results/balancer-1/repair-A2-1/passport.json --candidate results/balancer-1/repair-A2-1/final.lean
bin/proofforge verify results/euler-1/rw-euler-donate/repair-A1-1/passport.json --candidate results/euler-1/rw-euler-donate/repair-A1-1/final.lean
bin/proofforge verify results/knight-1/A2-2/passport.json --candidate results/knight-1/A2-2/final.lean
bin/proofforge verify results/vault-1/repair-A1-1/passport.json --candidate results/vault-1/repair-A1-1/final.lean

For agents: llms.txt and evidence.json list every claim, figure, Passport hash, source file and command on this page.