Found automatically: the Oct 2026 NEAR Intents mechanism, in 8 steps

Finds ghost funds in NEAR contracts, or proves there are none.

A Lean 4 model of NEAR async execution and NEP-141. A bounded search finds the shortest attack and the Lean kernel re-checks it; fixed contracts are proven solvent for every trace of the model; every trace is replayed on real Rust contracts in the NEAR sandbox.

Watch the attack, step by step →Source, proofs and docs

8 stepsthe Oct 2026 mechanism, found automatically in 26,191 states (about 45 ms)

2 theoremsfor all traces: the fixed vault stays solvent, and leaves no funds stuck (under stated assumptions)

8 / 8sandbox replays on real Rust contracts match the model after every transaction

0uses of sorry or native_decide; standard axioms only

The opening case

A deposit is credited. The notification fails. The token refunds. The credit stays.

A minimal model of the mechanism in the NEAR Intents postmortem (Oct 2026), written from scratch. It is not their contract. According to the postmortem, an attacker's contract deliberately failed deposit notifications; the token refunded each deposit while the ledger kept the credit; about $3.8M of unbacked balances was withdrawn (summary of the postmortem; the funds were returned).

Asked only whether the attacker can cash out more than she put in, exorcist check incident-2026-10 finds the whole exploit, deposit through to cash-out. The Lean kernel re-runs the trace (decide). The fixed contract credits only after the notification succeeded; it is clean in 1,289,374 states and proven solvent for every trace of our NEAR execution model.

Open the trace viewer →

$ exorcist check incident-2026-10
RESULT: VIOLATION (attacker_profit) at depth 8, 26191 states explored

1. eve sends tx: token.ft_transfer_call(vault, 100, "notify hook") (+1 yocto)
     ledger: alice=300 eve=0 (total 300) | tokens: vault=300 alice=0 eve=100
2. run #0 token.ft_transfer_call(vault, 100, "notify hook")  ⇒ returns a promise
     ledger: alice=300 eve=0 (total 300) | tokens: vault=400 alice=0 eve=0
3. run #1 vault.ft_on_transfer(eve, 100, "notify hook")  ⇒ returns a promise
     ledger: alice=300 eve=100 (total 400) | tokens: vault=400 alice=0 eve=0
4. FAIL #3 hook.on_deposit(eve, 100)  ⇒ adversary makes it fail
     ledger: alice=300 eve=100 (total 400) | tokens: vault=400 alice=0 eve=0
5. run #2 token.ft_resolve_transfer(eve, vault, 100)  ⇒ ok, returns 0  — refunds 100 vault → eve
     ledger: alice=300 eve=100 (total 400) | tokens: vault=300 alice=0 eve=100   ⚠ INSOLVENT (ledger > tokens held)
6. eve sends tx: vault.withdraw(100)
     ledger: alice=300 eve=100 (total 400) | tokens: vault=300 alice=0 eve=100   ⚠ INSOLVENT (ledger > tokens held)
7. run #5 vault.withdraw(100)  ⇒ ok (no value)
     ledger: alice=300 eve=0 (total 300) | tokens: vault=300 alice=0 eve=100
8. run #6 token.ft_transfer(eve, 100)  ⇒ ok (no value)
     ledger: alice=300 eve=0 (total 300) | tokens: vault=200 alice=0 eve=200   ⚠ INSOLVENT (ledger > tokens held)

  ✓ checked by the Lean kernel (decide)

Everything in one command

make demo

Finds every attack, checks each witness in the kernel, proves the fixes, and replays the traces on Rust contracts in the NEAR sandbox.

Results

Attacks found, fixes proven

Model	Result	Label
`incident-2026-10`	attack found: eve cashes out 200 from a 100 deposit	depth 8 · 26,191 states
`incident-2026-10-fixed`	solvent; the same attack ends with the refund and a rejected withdraw	proven for all traces
`deposit-vulnerable`	insolvent after a failed notification	depth 5 · 444 states
`noreturn-vulnerable`	insolvent with no failure at all (hook returns nothing)	depth 5 · 438 states
`withdraw-vulnerable`	user funds stuck after a failed payout	depth 5 · 3,622 states
`deposit-fixed, noreturn-fixed, withdraw-fixed`	no violation (1.04M / 0.84M / 11.2M states); solvent	bounded to depth 10proven for all traces
`withdraw-fixed, noreturn-fixed`	no stuck funds: tokens held = ledger whenever nothing is in flight. Assumes callbacks don't fail and no plain ft_transfer donations	proven for all traces (under those assumptions)
`withdraw-fixed-callback-fail`	if callbacks may fail, funds get stuck (the token's resolve runs out of gas); solvency still holds	depth 4 · 167 states
`sandbox (near-workspaces, Rust)`	8 trace replays match the model after every transaction; the negative control passes	real contracts
`NEAR testnet`	the attack drains the vulnerable vault; the fixed vault rejects the cash-out (4/4 transactions final)	testnet
`agent gate (MCP)`	an AI coding agent is blocked from deploying the vulnerable vault and allowed after the fix	tested

What is proven

For every trace of our NEAR execution model

Solvent forever

fixed_vault_solvent_forever: any accounts, any amounts, arbitrary attacker contracts and any receipt failing. After every trace, Σ ledger ≤ tokens held by the vault.

No stuck funds

fixed_vault_no_stuck_funds: whenever nothing is in flight, tokens held = Σ ledger. Assumes callbacks don't fail and no plain ft_transfer donations; withdraw-fixed-callback-fail shows the first assumption is needed.

Small trusted base

Checked by the Lean 4 kernel. #print axioms shows only propext, Classical.choice and Quot.sound. The explorer is not trusted: its traces are re-checked.

Limits

What Exorcist does not claim

Results are about models, written by hand and reviewed. Each model is checked against the Rust on the replayed traces, not in general. Gas, storage staking and deleted accounts are not modelled. Bounded results cover the stated actors, amounts and transactions only. exorcist draft, which has NEAR AI draft a model from Rust, is experimental. The full list, and a claims table mapping every claim to a command, are in the README.