FormalizedEmetאמת

NEAR HACKATHON 2026 · A PROOF BOUNTY FOR AGENT WALLETS

Check the wallet's
spending rule.

An agent found the broken spending rule. Emet checked its Lean counterexample inside a NEAR contract and paid the bounty. Then another agent proved the repair.

The page loads the recorded evidence…

This demo replays transactions on a local NEAR node. It uses our example wallet, not an exploit of the NEAR protocol.

TRY THE CHECKER

Ask the contract, with real proof bytes.

The genuine proof and the forged recursor proof go through the same proof checker. Each check is a free view call on a separate local NEAR node.

The page connects to the local checker…

Start ./verify.sh --serve and open the URL it prints to run these checks. The recorded demo above works without it.

The scope of the proof

The proof covers the named spending rule over the Lean policy. We trust or test the compiler, the adapter, the checker and the payout contracts. A proof cannot tell you whether you chose the right rule.

Read the trust boundaries →
Inspect the full transaction record

Every figure below comes from the run JSON. These are recorded transactions on a local NEAR node. Run ./verify.sh --wallet again for a new chain. --offline only checks files and recorded results. Source: .

1. The agent's wallet: every payment decision is Lean code compiled to wasm

2. Bounties for open questions: each pays a proof, or a counterexample

3. Refused: a lying agent tries to take the reward without a proof (each try forfeits a bond to the reward)

4. Two autonomous prover agents race, and a front-runner tries to steal

5. Money moves only with the proof, to any wallet that runs the proved code

6. The statement of the headline bounty, read back from the proof checker



  
7. Every claim of the run

  
    
    
    Run it again: ./verify.sh --wallet. The technical reference lists what we proved, tested and assumed, under "What this does not prove".