Agglayer Bridge Claim Nullifier Guarantee
A claim can succeed only for a committed exit-tree leaf, and that leaf becomes single-use.
AgglayerBridge lets users move assets and messages between networks through exit-tree leaves. A deposit or message adds a leaf to a local exit tree. A later claim proves that leaf belongs to an accepted Global Exit Root, then marks the leaf as claimed.
The verified property covers both claimAsset and claimMessage. If either function succeeds, the modeled bridge has checked the Merkle path against an accepted root and consumed the decoded bitmap nullifier.
What the spec helpers mean
validClaimLeaf_spec is the "this claim really came from the bridge tree" check. It says the claim leaf was rebuilt from the claim inputs, the Global Exit Root was accepted by the bridge, and the Merkle proof connects that leaf to the selected root.
nullifierConsumed_spec is the "this claim was used up" check. It says the bridge updated the bitmap position for the decoded source network and leaf index, so the same leaf cannot be accepted again.
Context
The bridge has two public claim paths. claimAsset releases or mints bridged value. claimMessage delivers a bridged message and optional value. Both paths call the same verification logic before any transfer, mint, or callback effect.
The unit at risk is the claim leaf. If a forged leaf were accepted, value or messages could be released without a matching deposit. If a real leaf could be claimed twice, the same bridge deposit could be spent more than once.
Why this matters
A bridge claim is a withdrawal rule. The bridge must only honor leaves that were committed into a trusted exit root. It must also reject repeat claims for the same source network and leaf index.
The proof checks both sides of that rule. A successful claim has an accepted Global Exit Root, a valid decoded global index, the right asset or message leaf hash, and a proof path to the selected root. After those checks pass, the nullifier bitmap changes in the word and bit position implied by the decoded leaf.
What this invariant covers
The model covers the verification path shared by claimAsset and claimMessage: leaf construction, Global Exit Root lookup, global-index decoding, mainnet versus rollup proof selection, and bitmap nullifier consumption.
The proof does not show that ERC-20 transfers, wrapped-token deployment, or receiver callbacks succeed after the nullifier is set. Those effects happen after the membership and nullifier checks in the Solidity source, so they are outside this claim-safety invariant.
How this was modeled / proven
The model follows the Solidity helper names and storage names so it can be reviewed next to the source. The key functions are _verifyLeaf, _setAndCheckClaimed, and _validateAndDecodeGlobalIndex. The Verity model is in Contract.lean.
The proof unfolds the successful execution of each claim path, extracts the runtime guards, and shows that the same conditions appear in validClaimLeaf_spec and nullifierConsumed_spec. A shared lemma proves that every successful call to _setAndCheckClaimed flips the expected bitmap word and rejects the already-claimed case.
The model has several scoped simplifications. They keep this case about claim authorization and replay protection, not about token side effects or proving cryptographic primitives themselves.
How the model differs from Solidity
- Metadata is already hashed. Solidity hashes dynamic
bytesmetadata before leaf construction. The model takesmetadataHashas an input and proves the claim path from that committed value. - Array-param helpers are inlined in claim paths. The helper functions remain in the model for review, but the public claim functions inline their array reads so the proof follows the same checks without an extra helper boundary.
- Words instead of bytes32.
bytes32values are modeled asUint256words, matching the word-level storage and proof inputs relevant to this invariant. - Hashes are deterministic word combiners. The proof preserves which inputs are hashed, but it does not prove the cryptographic implementation of
keccak256. The exact packed dynamic-bytes preimage is outside this case study. - Merkle proofs use one proof step. The model keeps the same branch structure as Solidity, including mainnet versus rollup proof selection, but summarizes the fixed-depth proof loop. The theorem is about the bridge requiring its calculated root to equal an accepted root.
- Post-nullifier side effects are abstracted. Token transfers, wrapped-token deployment, permits, events, and message callbacks happen after the nullifier path and are out of scope for this theorem.
Verify it yourself
git clone https://github.com/lfglabs-dev/verity-benchmark cd verity-benchmark git checkout add-agglayer-bridge-benchmark lake build Benchmark.Cases.Polygon.AgglayerBridge.Compile
If the build succeeds, Lean has checked the stated theorems. Benchmark pull request
Produced as part of the Verity benchmark, an open database of formally specified contract properties.
Proof status
The claim membership and nullifier-consumption theorems are fully proven. The file contains no sorry and no axiom.
| Function | Theorem | Status |
|---|---|---|
| claimAsset | claimAsset_valid_leaf_and_consumes_unique_nullifier | proven |
| claimAsset | claimAsset_valid_leaf_and_nullifier_consumed_direct | proven |
| claimMessage | claimMessage_valid_leaf_and_consumes_unique_nullifier | proven |
| claimMessage | claimMessage_valid_leaf_and_nullifier_consumed_direct | proven |
Assumptions / hypotheses
There are no outside protocol assumptions in the proof. The main theorems start from the broadest possible setup: any bridge state, any claim data, any Merkle proof, and any destination. If the modeled claim reverts, the invariant has nothing to prove. If it succeeds, the proof shows that the bridge must have accepted the leaf and consumed the decoded nullifier.
The direct corollaries write that in a shorter shape: suppose this particular claim call returned success with new state s'. That is not assuming the claim was valid. It is like saying, "if an ATM dispensed cash, prove the PIN and account checks passed." Here: if the bridge claim succeeded, prove the root check and nullifier write happened.
hclaimAsset or claimMessage returns success with post-state s'Operational premise of the direct corollaries
This is the successful execution case being analyzed. The proof does not trust the caller or the proof data. It follows the modeled function body and extracts the checks and storage writes that had to happen for the call to return success.
Learn more
Upstream Solidity source: AgglayerBridge.sol.
Leaf hashing source: DepositContractV2. Merkle proof helper: DepositContractBase.
Full case directory in the Verity benchmark repository.
What is a formal proof? A short explanation for non-specialists.
More research
Rootstock Flyover Quote Lifecycle
Formally verified peg-out quote conservation for Rootstock Flyover refunds.
1delta Caller-Address Integrity
Formally verified caller-address integrity for scoped OneDeltaComposerEthereum transfer and callback fund-pull paths.
Usual DaoCollateral Conservation
Formally verified direct swap and redeem accounting for Usual USD0 DaoCollateral.
