# 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.

Five real financial failures with more than $1 billion taken or lost, as the cited sources report. Each vulnerable version is refuted by a kernel-checked counterexample, and each was repaired by Muse Spark 1.3 (Meta), with Muse Wonder 1.0 planning where stated, and checked by ProofForge. Machine-readable version: /evidence.json. Source: https://github.com/davidwilliam/proof_forge

## Cetus, 2025-05-22

- Loss: about $223 million taken, as The Block reports from Cetus's incident report. Sources: https://www.theblock.co/post/355795/sui-dex-cetus-open-source-library-flaw-smart-contract-223-million-usd-exploit, https://dedaub.com/blog/the-cetus-amm-200m-hack-how-a-flawed-overflow-check-led-to-catastrophic-loss/
- Bug: The overflow check in checked_shlw tested against a 256-bit limit instead of a 192-bit limit, so a shift that lost bits reported no overflow.
- Property proved in Lean 4 (REQ-DELTA-A-COVERS): The overflow check never loses a bit, so a deposit is always charged at least the exact amount it owes.
- Vulnerable code (Original checked_shlw): REFUTED. On the attack deposit it charges 1 unit of token A; the exact amount owed, rounded up, is 31572840708638430117170542 units. Kernel-checked counterexample: realworld/tasks/rw-cetus-shlw/witnesses/buggy_original.lean. Passport b79e965381258ef8a287983b492911da0c4dc7b7437bfc538c14ad196aadfad3 (results/cetus-1/passports/original-port.json)
- Same-day hotfix (pull request 6, merged 14:37 UTC): REFUTED. It refuses the attack deposit, but checkedShlw(2^192) = (0, false): 2^192 shifted left by 64 bits wraps to 0 and no overflow is reported. A deposit with liquidity × price difference = 2^192 is charged 0. Passport d489c01595c307394d75579753303817724f7d586cffd2b7bb3b8cfe83f5e3e2 (results/cetus-1/passports/pr6-port.json)
- Final fix (pull request 7, merged 16:09 UTC): VERIFIED. All five requirements proved for every 256-bit input and every u128 price and liquidity. Passport 37d236fb45a80f418f9cfd7b63296b25c6326bb4a8517b86f8b7e806cdfa5e48 (results/cetus-1/passports/pr7-port.json)
- Muse repair: VERIFIED, 5 of 5 requirements, 6 kernels, 2001 property cases; attempt 1, 428 s, 23 model calls, $0.1871 at list prices, $0.0111 charged. Passport 9131dfdfd3e27da8145cd70972c65748a5447585ce2c625dee404b1506239852 (results/cetus-1/repair-A1-1/passport.json)
- Proved separately (results/cetus-1/repair-A1-1/Equivalence.lean, axioms propext, Quot.sound): theorem muse_eq_pr7 : ∀ n : BitVec 256, museShlw n = pr7Shlw n
- Reproduce: bin/proofforge verify results/cetus-1/repair-A1-1/passport.json --candidate results/cetus-1/repair-A1-1/final.lean
- Real code: The real checked_shlw and get_delta_a, unmodified at each pinned commit, ran with Sui CLI 1.83.0 (sui move test) on 2,007 inputs: 7 documented values and 2,000 generated by the task oracle.
  - Original: 658 of 2007 inputs break a requirement; 2007 equal the Lean port; 1317 equal the proved repair (the attack deposit returns 1)
  - Pull request 6: 33 of 2007 inputs break a requirement; 2007 equal the Lean port; 1974 equal the proved repair (32 of them at n = 2^192)
  - Pull request 7: 0 of 2007 inputs break a requirement; 2007 equal the Lean port; 2007 equal the proved repair (identical to the Muse repair on every input)
- Not proved: The Move code is run on 2,007 inputs and compared with the Lean ports and the proved component; it is not itself proved. get_delta_b, the tick math and the rest of the pool (positions, swaps, fees) are not specified.
- Task: realworld/tasks/rw-cetus-shlw/README.md

## Balancer V2, 2025-11-03

- Loss: more than $120 million across Balancer and its forks, as OpenZeppelin reports; The Block reports estimates of over $128 million. Sources: https://www.openzeppelin.com/news/understanding-the-balancer-v2-exploit, https://www.theblock.co/post/377863/balancer-identifies-rounding-error-as-root-cause-of-multi-chain-defi-exploit, https://www.certora.com/blog/breaking-down-the-balancer-hack
- Bug: 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.
- Context: 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.
- Property proved in Lean 4 (REQ-BATCH-KEEPS-VALUE): For any pool math meeting the stated contract, no batch of swaps of any length lowers the pool's value.
- Vulnerable code (Deployed swap path of the osETH/WETH pool): REFUTED. Four rounds of the attack's three swaps lower the pool's value from 4,749,898,000 to 297,229,191. Kernel-checked counterexample: realworld/tasks/rw-balancer-upscale/witnesses/attack_batch.lean. Passport d65bd405a13bfd4feaef838e4cc60dea2560bc47ff78cad8dfda591aaf26cb71 (results/balancer-1/passports/port.json)
- Muse repair, planned by Muse Wonder 1.0: VERIFIED, 8 of 8 requirements, 6 kernels, 2001 property cases; attempt 1, 2344 s, 151 model calls, $2.5115 at list prices, $0.4087 charged. Passport 48930efdd4d67460bfd22bb15dfa9625caafc36cd6fca3a8fee444d5f3b204ba (results/balancer-1/repair-A2-1/passport.json)
- Reproduce: bin/proofforge verify results/balancer-1/repair-A2-1/passport.json --candidate results/balancer-1/repair-A2-1/final.lean
- Real 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 pool: 56 of 501 batches break a requirement; 501 equal the Lean port; 194 equal the proved repair (the pool's invariant falls in 56 batches, and its BPT price with it)
  - Muse repair: 0 of 501 batches break a requirement (the proved component on the same 501 batches)
- Not proved: The requirements hold for any pool math meeting a stated contract; a constant-product pool is proved to meet it, StableMath is not, so results with StableMath are tested. BPT swaps, joins and exits are not modeled. The deployed contracts are run on 501 batches on a fork; they are not themselves proved.
- Task: realworld/tasks/rw-balancer-upscale/README.md

## Euler Finance, 2023-03-13

- Loss: about $197 million in net profit to the attacker, as Cyfrin reports; CoinDesk later reported that all recoverable funds were returned. Sources: https://www.cyfrin.io/blog/how-did-the-euler-finance-hack-happen-hack-analysis, https://www.zellic.io/blog/euler-finance-exploit-analysis, https://www.coindesk.com/business/2023/04/03/euler-says-all-recoverable-funds-stolen-in-200m-hack-have-been-returned
- Bug: donateToReserves moved an account's collateral to the reserves without the liquidity check that withdraw, mint and transfer perform.
- Property proved in Lean 4 (REQ-NO-BAD-DEBT): No sequence of operations leaves any account with more debt than its risk-adjusted collateral.
- Vulnerable code (Euler v1 at b1ee326): REFUTED. The attack sequence leaves 134,000,000 of debt with no collateral behind it. Kernel-checked counterexample: realworld/tasks/rw-euler-donate/witnesses/buggy_original.lean. Passport cec7d847f1d0b6a6f9cdb0e46fd149430807f86e14ce746054484ccee3a3a050 (results/euler-1/rw-euler-donate/passports/port.json)
- Muse repair: VERIFIED, 6 of 6 requirements, 6 kernels, 2001 property cases; attempt 1, 1682 s, 40 model calls, $0.8324 at list prices, $0.0489 charged. Passport 6de7bb94c38cf23a31ba08174d7505b4b8d54dddc9ffbd6d177dde4981b82002 (results/euler-1/rw-euler-donate/repair-A1-1/passport.json)
- Reproduce: 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
- Real 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, unmodified: 57 of 1004 sequences break a requirement; 947 equal the proved repair (Euler's own liquidity check also reports collateral below liability in 57)
  - The same with checkLiquidity(account) added: 0 of 1004 sequences break a requirement; 1004 equal the proved repair (a local copy, not an upstream release)
- Not proved: One asset priced at 1, an eToken exchange rate fixed at 1 and no interest; flash loans, sub-accounts and multiple collateral assets are not modeled. The contracts are run on 1,004 sequences and compared with the requirements and the proved component; they are not themselves proved.
- Task: realworld/tasks/rw-euler-donate/README.md

## Knight Capital, 2012-08-01

- Reconstructed: 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: $460 million realized loss, as the SEC order states. Sources: https://www.sec.gov/files/litigation/admin/2013/34-70694.pdf, https://web.archive.org/web/20201212052325/https://www.sec.gov/litigation/admin/2013/34-70694.pdf
- Bug: 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.
- Context: 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.
- Property proved in Lean 4 (REQ-NEVER-OVERROUTE): On every server and code version, after any sequence of events, the shares sent for an order never exceed its quantity.
- Vulnerable code (Reconstructed Power Peg router): REFUTED. For every n, n rounds of a 100-share routing opportunity and a fill send n child orders and 100 × n shares for one 100-share order. Kernel-checked counterexample: realworld/tasks/rc-knight-router/witnesses/buggy_original.lean. Passport ca3e7312fe7af22f53f52fbd08f53dfc85bde86ebe49a96e0e9751e4f365a6b8 (results/knight-1/start/passport.json)
- Muse repair, planned by Muse Wonder 1.0: VERIFIED, 6 of 6 requirements, 6 kernels, 2001 property cases; attempt 2, 4079 s, 256 model calls, $4.96 at list prices, $0.9788 charged. Passport 98cfed64ae1ec596e517299b422a5fb0beac571cdce89c18ea2e5660845bc178 (results/knight-1/A2-2/passport.json)
- Earlier attempt A1, attempt 1: UNRESOLVED; its executable passed all 2001 property cases, but it proved 1 of 6 requirements before its wall-clock cap, so no VERIFIED Passport. Passport 4fddc1683956e92f1f0a7e97eb48bdc238e233b55b9e430dda47062bfaac5e74 (results/knight-1/A1-1/passport.json)
- Earlier attempt A1, attempt 2: UNRESOLVED; its executable passed all 2001 property cases, but it proved 1 of 6 requirements before its dollar cap, so no VERIFIED Passport. Passport 27f4c83221ed220ea8e52e955a82a45bd73f9d8eed2d0136081096a4b09afb6c (results/knight-1/A1-2/passport.json)
- Earlier attempt A2, attempt 1: UNRESOLVED; its executable passed all 2001 property cases, but it proved 5 of 6 requirements before its dollar cap, so no VERIFIED Passport. Passport edc4ec8cd40a2db0fb8b77a2c959e5d9e4cb236403e5ce4e3cb2778bd5279c9b (results/knight-1/A2-1/passport.json)
- Reproduce: bin/proofforge verify results/knight-1/A2-2/passport.json --candidate results/knight-1/A2-2/final.lean
- Real code: none: the code is not public
- Not proved: The mechanism by which fills stopped reaching Power Peg's count is one interpretation of paragraphs 14 and 16 of the order; other mechanisms with the same outcome are possible. Prices, venues, order types, timing and cancellations are not modeled. The executable wrapper is tested, not proved.
- Task: realworld/tasks/rc-knight-router/README.md

## Hundred Finance, 2023-04-15

- Loss: about $7 million in reported losses (rekt.news gives $7.4M; this figure was not checked here). Sources: https://rekt.news/hundred-rekt2, https://blocksec.com/blog/6-hundred-finance-incident-catalyzing-the-wave-of-precision-related-exploits-in-vulnerable-forked-protocols
- Bug: redeemUnderlying rounded the shares burned down, so a withdrawal worth 1.99999999992 share units burned 1.
- Property proved in Lean 4 (REQ-SHARE-VALUE): No sequence of operations, donations included, lowers the value of a share while shares are outstanding.
- Vulnerable code (Hundred hToken share accounting): REFUTED. After the attack's own amounts, the last share unit is backed by 2 satoshi. Kernel-checked counterexample: realworld/tasks/rw-hundred-vault/witnesses/hundred_attack.lean
- Muse repair: VERIFIED, 10 of 10 requirements, 6 kernels, 2001 property cases; attempt 1, 1200 s, 67 model calls, $0.6513 at list prices, $0.037 charged. Passport 08fe86f17f27c49d60bda786d1498200d333c1c8d63d2f858ab668cd4f7fe7c4 (results/vault-1/repair-A1-1/passport.json)
- Reproduce: bin/proofforge verify results/vault-1/repair-A1-1/passport.json --candidate results/vault-1/repair-A1-1/final.lean
- Real 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 contract: 292 of 501 sequences break a requirement; 501 equal the Lean port; 209 equal the proved repair (identical to the Lean port after every operation of all 501)
  - Muse repair: 0 of 501 sequences break a requirement (the proved component, on the same 501 sequences)
- Not proved: Only share accounting is modeled; the comptroller, borrowing, liquidation, interest and reserves are not. The specification states the share-value property the borrow relied on. The deployed contract is run on 501 sequences on a fork and compared with the port and the requirements; it is not itself proved.
- Task: realworld/tasks/rw-hundred-vault/README.md

## Implemented from the specification alone

- cetus: VERIFIED, 5 of 5 requirements. Passport b2cf6c2de4f91b8ea0f1505463e5301f28783d87a103c0a3e7d1d3f791a7dd7a (results/implement-flagships-1/rw-cetus-shlw/passport.json). Reproduce: bin/proofforge verify results/implement-flagships-1/rw-cetus-shlw/passport.json --candidate results/implement-flagships-1/rw-cetus-shlw/final.lean
- euler: VERIFIED, 6 of 6 requirements. Passport 27d4ec2838e9bbfc938278e29e8eac89570d1f14a9468de15b03514cbdd4286e (results/implement-flagships-1/rw-euler-donate/passport.json). Reproduce: bin/proofforge verify results/implement-flagships-1/rw-euler-donate/passport.json --candidate results/implement-flagships-1/rw-euler-donate/final.lean
- hundred: VERIFIED, 10 of 10 requirements. Passport eee7e2cdbedf658d81afc95f07966d5d37a9e6f7a27cabbccd6dd0dc5ba6e3c6 (results/implement-flagships-1/rw-hundred-vault/passport.json). Reproduce: bin/proofforge verify results/implement-flagships-1/rw-hundred-vault/passport.json --candidate results/implement-flagships-1/rw-hundred-vault/final.lean
- balancer: VERIFIED, 8 of 8 requirements. Passport 65d5a81fef2352eb67a72f032ade091fd051b30ebf44c310b1d0c6dcb1b84d3d (results/balancer-1/implement-2/passport.json). Reproduce: bin/proofforge verify results/balancer-1/implement-2/passport.json --candidate results/balancer-1/implement-2/final.lean
- Benchmark: 30 of 30 test tasks implemented from the specification alone (9 base specifications in ledgers, permissions and queues; the variants differ only in code implement mode never sees; results/implement-1/implement.json).

## Benchmark

- 59 repair tasks in six families: payouts (9), ledgers (10), transfer batches (10), permissions (10), rate limiters (10), queues (10); 23 development, 6 validation, 30 test.
- E1 (results/e1-test-1/e1.json): on the 30 frozen test tasks, A0 Compile-and-retry completed 28, A1 ProofForge harness completed 30, A2 Harness and planner completed 30; McNemar exact p = 0.5 against A0, so the arms are not shown to differ. 90 runs cost $70.09 at list prices.
- E2 (results/e2-all-1/e2.json): seeded bad repairs accepted, out of 247: Ordinary checking 233, Rebuild and property tests only 1, ProofForge 0. Correct repairs rejected, out of 239: Ordinary checking 0, Rebuild and property tests only 0, ProofForge 0. Every bad case is a seeded attack written by the build team.

## Not claimed

- The deployed Solidity and Move code is not itself proved. Each incident's Lean 4 port is a reviewed hand translation, tested against the real code on the stated inputs; the translation is not machine-checked.
- A requirement covers exactly what its Lean statement says. Each port models only the logic named in its task README.
- Loss figures are quoted from the sources each task README cites.
- The JSON wrapper around each proved function is tested, not proved.
- 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.

## Reproduce

    git clone https://github.com/davidwilliam/proof_forge && cd proof_forge
    docker build -t proofforge-lean:4.35.0 -f infra/docker/Dockerfile.lean infra/docker
    bin/proofforge verify results/cetus-1/passports/original-port.json --candidate realworld/tasks/rw-cetus-shlw/attacks/buggy_original.lean
    bin/proofforge verify results/cetus-1/repair-A1-1/passport.json --candidate results/cetus-1/repair-A1-1/final.lean
    bin/proofforge verify results/cetus-1/passports/pr6-port.json --candidate realworld/tasks/rw-cetus-shlw/attacks/pr6_mask_only.lean
    bin/proofforge verify results/cetus-1/passports/pr7-port.json --candidate realworld/tasks/rw-cetus-shlw/reference/SolutionA.lean
    bin/proofforge verify results/balancer-1/passports/port.json --candidate realworld/tasks/rw-balancer-upscale/attacks/balancer_port.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/passports/port.json --candidate realworld/tasks/rw-euler-donate/candidate/Solution.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/start/passport.json --candidate realworld/tasks/rc-knight-router/candidate/Solution.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

## Pages

- /: overview with the five incidents
- /forge: live forge session (replay of a recorded Muse repair, then a fresh check)
- /results: E1 and E2 per arm, family and case