EXIT STAGES FOR NEAR CONTRACTS · REGISTRY ON NEAR MAINNET
Can you always
get it back?
Before you, or your agent, deposit into a NEAR contract: who can change its code, who can move or freeze the funds, and is there a proof that you can always withdraw? Exit Proof gives every contract an exit stage. Each stage is defined by evidence that anyone can check again. The top stage takes a Lean theorem tied to the deployed code hash.
ASK THE CHAIN
The exit stage of any NEAR account.
This page runs the scanner of the repository in your browser. Your browser reads public RPC, and nothing is signed. If the chain cannot be read, there is no verdict.
The scanner starts loading when you come near this form: about 10 MB, once per visit.
The whole report
The same answer on the command line: python3 tools/exitproof.py <account>.
THE VIDEO · 1 MIN 43 S
Exit Proof in a minute and a half.
01 · THE STAGES
Four stages, each defined by evidence.
A stage answers one question for a depositor: if I put money into this contract, what guarantees that I can get it back? The ladder follows the idea of L2BEAT's Stages for rollups. What is added here is the top rung: a stage is 2 only with a machine-checked exit theorem tied to the deployed code hash.
| Stage | Meaning | Evidence |
|---|---|---|
| 2 Proven exit | The code cannot change, and a depositor can always withdraw by its own calls. | No code-change path and no access key; an exit theorem registered on chain for the exact code hash by an accepted attestor; the account's state was made by this code: one deployment, or every deployment recorded by the proof. |
| 1 Exit window | The code can change only after a visible delay, long enough to leave. | The code runs the proved upgrade plugin (a certificate or a proof for its code hash), no other code-change method is found by name, and the plugin's delay is set. Names alone give stage 0. |
| 0 Keyholder trust | The code can change with no notice, or exits can be paused and deposits moved. | The scanner names the path and how strongly it is guarded: a DAO vote, a multisig, another contract, several keys, one key. |
| U Unproven | No code-change path was found, and no exit theorem covers this account. | Absence of evidence, stated as such: no theorem for the code hash, or the account has a key or a history the theorem does not cover. |
A report shows how strongly each power is guarded and never lists who holds it. The full rules.
02 · WHERE NEAR STANDS
Most staked NEAR can always leave. Most large contracts can change overnight.
Staked NEAR, by the stage of the pool that holds it
Large contracts: bridges, tokens, DeFi
The numbers on this page are read from the evidence files of the repository when the page loads. Each has a script that produced it and a check that compares it with the documents.
03 · WHAT IS PROVED
A theorem about a model, tied to the deployed bytes.
Three levels of evidence are kept apart everywhere. Proved is a Lean theorem about a model. Tested is the model run against the exact deployed wasm on nearcore's own runtime. Read is chain state or a contract's own answer.
| Subject | Proved in Lean | Not covered |
|---|---|---|
Core staking pool, the code of *.poolv1.near | A delegator can always unstake and withdraw. Nobody else lowers its balance. | Storage staking. That the protocol returns the stake is an assumption. |
wNEAR, wrap.near | A holder can always unwrap, under an invariant of the state. | The rest of the invariant on mainnet, and the code the account ran before 2021. |
Token ledger of NEAR Intents, intents.near | For a standard token and for wNEAR the ledger never exceeds the holdings. Withdrawals settle exactly. A balance falls only in six ways, each with the checks the contract makes. | The multi-token and NFT paths, the swap path (token_diff) and its fees, gas, the signature standards, a proof about the bytes. |
| Token standard, near-contract-standards 5.29.0 | Supply is the sum of balances. Settlement refunds at most what was sent. Only the token settles. | Other library versions: their verdicts come from runs. |
| Upgrade plugin, near-plugins v0.5.1 | No deploy is accepted before a bound that is tight. | Contracts that changed the plugin. |
| Gated upgrades | Every code change installs code that had a certificate. | The gate is as strong as the attestors it accepts. |
One statement, as Lean reads it
theorem T1_ledger_covered (K : Cfg) (S : World) (h : Reach K S) :
total S.L.bals ≤ bal S.c.accts K.me
In every reachable state of the contract together with a standard token, the sum of the ledger balances is at most the token balance of the contract: with anything in flight, at any point of any interleaving, with any receipt failing. The Intents proof has the assumptions and what is not covered.
04 · THE PIPELINE
Proved once for a code hash. Read for every account.
- 01Deployed code
The exact wasm of a contract on mainnet, named by its code hash.
- 02Lean model and theorems
Written from the source. Any receipt may fail, in any order.
- 03Replay
The wasm runs on the nearcore runtime. Every receipt is compared with the model.
- 04Certificate
In a registry on NEAR mainnet, with the command that re-checks it.
- 05An account
Its keys, the methods of its code, its roles, its deployment history.
- 06Scanner
Applies the stage rules and looks the code hash up in the registry.
- 07Exit stage
2, 1, 0 or U, each with the evidence it rests on.
- 08Who asks
A depositor, an agent through MCP, a watch that reports a change.
05 · TOKENS
Does this token behave as the standard?
The proof of the Intents ledger holds for tokens that behave as the proved NEP-141 standard. The token check answers that for one token: the verdict for its code hash from runs of the deployed code, what is switched on right now, and whether its code can change.
06 · ON NEAR MAINNET
The certificates live in a contract nobody can change.
registry.exitproof.near keeps the certificates by code hash. It has no access key and no upgrade method, and it holds nobody's funds. Each certificate pins a hash of the proof directory and names the command that re-checks the proof. The registry records who attests what; it does not check a proof on chain.
| Step | Transaction |
|---|---|
| Deploy the registry | Bb34SR1z… |
2 Exit certificate: the core staking pool, code J1arLz48… | 31oaqvX2… |
2 Exit certificate: wNEAR, code DL2f5xmZ… | 7h4KGyi9… |
| Token-standard certificate: the reference token of near-contract-standards 5.29.0 | 7cnk2Urb… |
| 1 Upgrade-window certificate: the reference vault of the upgrade plugin | BpAq7sGT… |
| Delete the registry's only access key | F6ypQV24… |
The one attestor so far, exitproof.near, is the project's own account with one key: a certificate is its statement plus a command anyone can run. The stage-1 examples and a vault that refused uncertified code are on testnet: the registry and the stage-1 examples, the gated vault.
07 · FOR AGENTS AND TEAMS
Ask before the deposit. Check before the upgrade.
Everything on this page is a command in the repository: Python 3.10 and its standard library, public RPC, nothing signed. An answer always carries a status, and unreadable is never a pass.
An MCP server with three tools: exit_check, exit_plan, token_check.
{"mcpServers": {"exit-proof": {
"command": "python3",
"args": ["tools/mcp_server.py"]}}}Stakes only at stage 2 by default, or, with --min-stage 1, at a certified stage 1 with a window of at least a day; otherwise it refuses and says why.
python3 tools/agent_demo.py \ astro-stakers.poolv1.near 100 # decision: PROCEED, with the # transaction it would sign
Does the proof carry over to the new commit? The replay, the places that write the ledger, the exported methods.
intents-proof/scripts/verify_upgrade.sh \ <commit> # CARRIES OVER, DIVERGES, or # NEEDS REVIEW with the files to re-read
Runs its own wasm on 1 000 traces with 14 monitors of the proved NEP-141 properties and writes a certificate anyone can re-run.
token-monitors/certify.sh \ your.wasm your-config.json
A watch that reports a change of code, stage, keys, upgrade delay, staged code or token tax, and exits with 1.
python3 tools/watch.py wrap.near \ --state watch.json
The numbers of the documents against the evidence files, then the self-test on real accounts: one command, minutes.
./check-all.sh # RESULT: PASS
WHAT THIS IS NOT
A stage is evidence to weigh, not a guarantee.
- Not a proof about the bytes. A theorem is about a Lean model. The tie to the deployed wasm is hash equality plus execution on random traces, and it is measured with one-line changes of the model.
- Not checked on chain. A certificate is an attestor's statement with a command that re-checks it. The one attestor so far is an account with one key.
- Not every risk. A stage is about exits. An oracle, the economic design and a bridge are outside it.
- Not the finder of the 2026 incidents. The teams of those contracts found them, fixed them and published what happened.