PROOF-GATED CONTRACT UPGRADES · NEAR
No proof,
no upgrade.
AI agents will write contract patches. Emet lets a contract take one only with a machine-checked proof. A Lean proof checker runs inside a NEAR contract. A second contract holds the only right to upgrade a third, and uses it only after the checker accepts a proof for the patch. Anyone can supply the proof, an AI agent included. Nobody can upgrade without it, us included.
ASK THE CONTRACT
Pick a patch for one line of NEAR Intents.
The line computes how much of a deposit goes back when the receiver asks for a refund. The proof checker gets a proof that the patch meets the refund rule, or a counterexample.
The page looks for a proof checker…
The answer of the contract
01 · THE CASE
Eighty credits with nothing behind them.
The incident of 29 September to 1 October 2026 was an exploit of NEAR Intents through its deposit notifications. Its team found the cause, recovered the funds, fixed the contract and published a post-mortem (coverage). Emet found none of this. It uses that code as a test subject for a gate.
To reproduce the failure, a NEAR Intents engineer pushed a temporary commit to the branch of pull request #362. The commit is 35044fd, “TEMP change that reflects deployed state”. It puts the deployed refund expression, balance_left.min(requested_refund), back on top of the main branch. With that expression the regression test of the pull request fails as production did. The team reverted the commit 26 minutes later. The main branch capped the refund from 23 March (#240).
The old and the fixed contract here are builds of those two commits, unmodified: the temporary one, and its parent. A batch in the shape of that regression test has eighty transfers of 1 that each ask for 1035 back. On the old code the refund event of that batch outgrows the 16,384-byte log limit, and the callback fails. The token contract returns the tokens to the sender, and the credit made on deposit stays.
The team's response went further than this one line. The same day it limited a batch to ten tokens (#364). On 7 October it removed deposit notifications (#374). We model neither change here.
02 · THE RULE
The comment, written as a theorem.
The contract sizes the refund event when a deposit arrives. It assumes that a refund is never larger than the deposit. In November 2025 one pull request (#150) added a comment above the expression: refunds are capped by deposited amounts. It also added an expression that did not cap them (release v0.4.2 shows both lines). A compiler cannot refuse a comment. Here that comment is the second line of a Lean statement, and the proof checker refuses the old expression with a counterexample:
def Rule (a : Args) (r : Nat) : Prop := r ≤ a.requested ∧ r ≤ a.deposited ∧ r ≤ a.balance ∧ (r = a.requested ∨ r = a.deposited ∨ r = a.balance)
It holds for every request, deposit and balance that fits in a u128. The four lines leave one answer and no other: the smallest of the three amounts.
The property that failed
The same environment holds a second theorem, about the event itself. Take any patch that meets the rule and any batch of tokens. The two lists of the refund event are then not longer than those of the deposit event, which the contract checked on deposit. The old expression has no such bound.
theorem refund_event_fits (e : Expr) (h : meetsRule e) (xs : List Item)
(hx : ∀ x ∈ xs, InRange x.inputs) : burnBytes e xs ≤ mintBytes xs
The theorem is about a model of two JSON lists, not about the contract. The model gives the real length of every recorded event to the byte. The refund event of the batch that a local node refused has 17,353 bytes. For the same batch on testnet it has 17,519 bytes. The content and the limits of the theorem →
03 · THE GATE
The same account, before and after.
The page loads the upgrade record…
04 · THE AGENT
05 · A LARGER STATEMENT
Two theorems of NEAR Proof Arena, checked on testnet.
WHAT THIS IS NOT
A proof about one expression.
- The proof is about a Lean expression that a small extractor reads from one line of Rust. It is not a proof about the binary, the callback, or the NEAR Intents contract.
- The gate's deployer registers the binaries that the gate can install, and pairs each with its source. The chain checks the proof and does not check that pairing. The binaries here rebuild to the same bytes on macOS and Linux, so anyone can check the pairing.
- One gate installs one upgrade. The gate cannot install a patch that nobody registered, whoever proves it.
- With the comment as its rule, a gate refuses that code at the first attempt to install it. A gate does not write the rule. It also does not deploy the March fix sooner. A gate is not the emergency path: that path is the guardian's pause, shown above.
- We trust or test the compiler, the extractor, the proof checker and the gate's own code. We did not prove them.