diff --git a/Benchmark/Cases/Polygon/AgglayerBridge/Compile.lean b/Benchmark/Cases/Polygon/AgglayerBridge/Compile.lean
new file mode 100644
index 00000000..db13feef
--- /dev/null
+++ b/Benchmark/Cases/Polygon/AgglayerBridge/Compile.lean
@@ -0,0 +1,6 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Contract
+import Benchmark.Cases.Polygon.AgglayerBridge.Proofs
+
+namespace Benchmark.Cases.Polygon.AgglayerBridge
+
+end Benchmark.Cases.Polygon.AgglayerBridge
diff --git a/Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean b/Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean
new file mode 100644
index 00000000..b8223e32
--- /dev/null
+++ b/Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean
@@ -0,0 +1,379 @@
+import Contracts.Common
+
+namespace Benchmark.Cases.Polygon.AgglayerBridge
+
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+open Verity.Stdlib.Math
+open Contracts
+
+/-!
+AgglayerBridge Merkle/nullifier model.
+
+| what was simplified | why |
+|---|---|
+| `bytes32` is modeled as `Uint256` words | Verity's proof surface is word-oriented; this preserves the storage and hash inputs relevant to the invariant. |
+| Raw `metadata : bytes` is replaced by `metadataHash : Uint256` on claim/model entry points | Dynamic `bytes` hashing and exact dynamic `abi.encodePacked` parity are outside the current convenient Verity core surface; the bridge itself hashes metadata before leaf construction. |
+| `keccak256` / `Hashes.efficientKeccak256` are modeled by deterministic word-combiners (`xor` over the same logical inputs) | Cryptographic collision resistance is a trusted primitive boundary, not the target theorem. |
+| `bytes32[32] calldata` Merkle proofs are modeled as `Array Uint256` | Word-sized array parameters are supported; exact fixed-array ABI shape is not needed for the invariant. |
+| Merkle loops are represented by one-step word-combiner `calculateRoot` | A faithful 32-step loop is expressible, but the Phase 2 invariant only needs the bridge to require the calculated root equals the accepted root. |
+| Public claim functions inline `_verifyLeafAndSetNullifier` / `_verifyLeaf` proof-array reads | Current direct macro helper lowering rejects helper calls with array parameters; helper functions remain present for source review. |
+| `globalExitRootManager.globalExitRootMap` is modeled as ghost storage mapping `globalExitRootMap` | The manager is an external dependency; claim safety only requires the bridge to reject unregistered global exit roots. |
+| Token/native transfers, wrapped-token deployment, permit, events, and message callbacks are abstracted after nullifier setting | They occur after `_verifyLeafAndSetNullifier` and are not needed for Merkle membership or double-claim safety. |
+| Solidity `uint32` / `uint8` are modeled as `Uint256` with caller-side boundedness assumptions | Verity arithmetic is word-oriented; bit reconstruction checks in `_validateAndDecodeGlobalIndex` preserve the relevant global-index shape. |
+
+Local copies of storage slots use the trailing-underscore convention when needed.
+-/
+
+def MAINNET_NETWORK_ID : Uint256 := 0
+def ZKEVM_NETWORK_ID : Uint256 := 1
+def LEAF_TYPE_ASSET : Uint256 := 0
+def LEAF_TYPE_MESSAGE : Uint256 := 1
+def MAX_LEAFS_PER_NETWORK : Uint256 := 4294967296
+def GLOBAL_INDEX_MAINNET_FLAG : Uint256 := 18446744073709551616
+def LOW_32_MASK : Uint256 := 4294967295
+def LOW_8_MASK : Uint256 := 255
+
+def globalIndexForNullifierModel
+    (networkID leafIndex sourceBridgeNetwork : Uint256) : Uint256 :=
+  if networkID == MAINNET_NETWORK_ID && sourceBridgeNetwork == ZKEVM_NETWORK_ID then
+    leafIndex
+  else
+    add leafIndex (mul sourceBridgeNetwork MAX_LEAFS_PER_NETWORK)
+
+def bitmapWordPosModel (index : Uint256) : Uint256 := shr 8 index
+def bitmapBitPosModel (index : Uint256) : Uint256 := and index LOW_8_MASK
+def bitmapMaskModel (index : Uint256) : Uint256 := shl (bitmapBitPosModel index) 1
+
+verity_contract AgglayerBridge where
+  storage
+    -- src: DepositContractBase.sol:40 — `_branch[height]`, flattened from fixed storage array.
+    _branch : Uint256 → Uint256 := slot 0
+    -- src: DepositContractBase.sol:43 — public deposit counter.
+    depositCount : Uint256 := slot 1
+    -- src: AgglayerBridge.sol:68 — local bridge network id.
+    networkID : Uint256 := slot 2
+    -- src: AgglayerBridge.sol:908-914 — ghost of `globalExitRootManager.globalExitRootMap`.
+    globalExitRootMap : Uint256 → Uint256 := slot 3
+    -- src: AgglayerBridge.sol:77 — nullifier bitmap.
+    claimedBitMap : Uint256 → Uint256 := slot 4
+    -- src: AgglayerBridge.sol:74 — last deposit count pushed to the manager.
+    lastUpdatedDepositCount : Uint256 := slot 5
+    -- src: AgglayerBridge.sol:90-93 — gas-token identity used in token branches, retained for fidelity.
+    gasTokenAddressWord : Uint256 := slot 6
+    gasTokenNetwork : Uint256 := slot 7
+
+  function hashPair (a : Uint256, b : Uint256) : Uint256 := do
+    return xor a b
+
+  function getLeafValue (
+      leafType : Uint256,
+      originNetwork : Uint256,
+      originAddress : Address,
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amount : Uint256,
+      metadataHash : Uint256
+    ) : Uint256 := do
+    -- src: DepositContractV2.sol:22-43 — keccak256(abi.encodePacked(...)).
+    let originAddressWord := addressToWord originAddress
+    let destinationAddressWord := addressToWord destinationAddress
+    let leafValue :=
+      xor
+        (xor (xor leafType originNetwork) originAddressWord)
+        (xor (xor destinationNetwork destinationAddressWord) (xor amount metadataHash))
+    return leafValue
+
+  function calculateGlobalExitRoot (mainnetExitRoot : Uint256, rollupExitRoot : Uint256) : Uint256 := do
+    -- src: GlobalExitRootLib.sol:11-16 — efficientKeccak256(mainnetExitRoot, rollupExitRoot).
+    let root ← hashPair mainnetExitRoot rollupExitRoot
+    return root
+
+  function calculateRoot (leafHash : Uint256, smtProof : Array Uint256, index : Uint256) : Uint256 := do
+    -- src: DepositContractBase.sol:129-148 — 32-step sparse Merkle proof calculation (word-combiner summary).
+    let proofHead := arrayElement smtProof 0
+    let root := xor (xor leafHash index) proofHead
+    return root
+
+  function verifyMerkleProof (
+      leafHash : Uint256,
+      smtProof : Array Uint256,
+      index : Uint256,
+      root : Uint256
+    ) : Bool := do
+    -- src: DepositContractBase.sol:114-121 — calculated root must match expected root (array helper call inlined).
+    let proofHead := arrayElement smtProof 0
+    let computedRoot := xor (xor leafHash index) proofHead
+    return computedRoot == root
+
+  function getRoot () : Uint256 := do
+    -- src: DepositContractBase.sol:55-75 — current local exit root from `_branch` and `depositCount` (word-combiner summary).
+    let depositCount_ ← getStorage depositCount
+    let branch0 ← getMappingUint _branch 0
+    let root ← hashPair branch0 depositCount_
+    return root
+
+  function _addLeaf (leaf : Uint256) : Unit := do
+    -- src: DepositContractBase.sol:81-90 — reject full tree and pre-increment `depositCount`.
+    let depositCount_ ← getStorage depositCount
+    require (depositCount_ < 4294967295) "MerkleTreeFull"
+    let size := add depositCount_ 1
+    setStorage depositCount size
+    -- src: DepositContractBase.sol:91-105 — update one frontier node; flattened to the first matched frontier slot.
+    setMappingUint _branch 0 leaf
+
+  function _addLeafBridge (
+      leafType : Uint256,
+      originNetwork : Uint256,
+      originAddress : Address,
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amount : Uint256,
+      metadataHash : Uint256
+    ) : Unit := do
+    -- src: AgglayerBridge.sol:864-884 — hash bridge leaf then append it to the local exit tree.
+    let leafValue ← getLeafValue leafType originNetwork originAddress destinationNetwork destinationAddress amount metadataHash
+    _addLeaf leafValue
+
+  function _updateGlobalExitRoot () : Unit := do
+    -- src: AgglayerBridge.sol:1069-1071 — remember submitted deposit count and call manager.updateExitRoot(getRoot()).
+    let depositCount_ ← getStorage depositCount
+    setStorage lastUpdatedDepositCount depositCount_
+    let root ← getRoot
+    setMappingUint globalExitRootMap root 1
+
+  function bridgeAsset (
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amount : Uint256,
+      originNetwork : Uint256,
+      originTokenAddress : Address,
+      metadataHash : Uint256,
+      forceUpdateGlobalExitRoot : Bool
+    ) : Unit := do
+    -- src: AgglayerBridge.sol:290-380 — token/native branch effects abstracted; resolved origin fields are explicit parameters.
+    let networkID_ ← getStorage networkID
+    require (destinationNetwork != networkID_) "DestinationNetworkInvalid"
+    -- src: AgglayerBridge.sol:382-401 — BridgeEvent omitted; append asset leaf.
+    _addLeafBridge 0 originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash
+    -- src: AgglayerBridge.sol:403-406 — optional global exit root update.
+    if forceUpdateGlobalExitRoot then
+      _updateGlobalExitRoot
+    else
+      pure ()
+
+  function _bridgeMessage (
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amountEther : Uint256,
+      originAddress : Address,
+      metadataHash : Uint256,
+      forceUpdateGlobalExitRoot : Bool
+    ) : Unit := do
+    -- src: AgglayerBridge.sol:480-489 — destination cannot be the local bridge network.
+    let networkID_ ← getStorage networkID
+    require (destinationNetwork != networkID_) "DestinationNetworkInvalid"
+    -- src: AgglayerBridge.sol:491-510 — BridgeEvent omitted; append message leaf.
+    _addLeafBridge 1 networkID_ originAddress destinationNetwork destinationAddress amountEther metadataHash
+    -- src: AgglayerBridge.sol:512-515 — optional global exit root update.
+    if forceUpdateGlobalExitRoot then
+      _updateGlobalExitRoot
+    else
+      pure ()
+
+  function _validateAndDecodeGlobalIndex (globalIndex : Uint256) : Tuple [Uint256, Uint256, Uint256] := do
+    -- src: AgglayerBridge.sol:1138-1140 — last 32 bits are leafIndex.
+    let leafIndex := and globalIndex 4294967295
+    -- src: AgglayerBridge.sol:1141-1163 — branch on mainnet flag and reconstruct to reject unused bits.
+    if and globalIndex 18446744073709551616 != 0 then
+      let indexRollup := 0
+      let sourceBridgeNetwork := 0
+      require (add 18446744073709551616 leafIndex == globalIndex) "InvalidGlobalIndex"
+      return (leafIndex, indexRollup, sourceBridgeNetwork)
+    else
+      let indexRollup := shr 32 globalIndex
+      let sourceBridgeNetwork := add indexRollup 1
+      require (add (shl 32 indexRollup) leafIndex == globalIndex) "InvalidGlobalIndex"
+      return (leafIndex, indexRollup, sourceBridgeNetwork)
+
+  function _verifyLeaf (
+      smtProofLocalExitRoot : Array Uint256,
+      smtProofRollupExitRoot : Array Uint256,
+      globalIndex : Uint256,
+      mainnetExitRoot : Uint256,
+      rollupExitRoot : Uint256,
+      leafValue : Uint256
+    ) : Tuple [Uint256, Uint256] := do
+    -- src: AgglayerBridge.sol:906-919 — global exit root must be known by the manager.
+    let globalExitRoot ← calculateGlobalExitRoot mainnetExitRoot rollupExitRoot
+    let blockHashGlobalExitRoot ← getMappingUint globalExitRootMap globalExitRoot
+    require (blockHashGlobalExitRoot != 0) "GlobalExitRootInvalid"
+    -- src: AgglayerBridge.sol:921-927 — validate/decode globalIndex.
+    let (leafIndex, indexRollup, sourceBridgeNetwork) ← _validateAndDecodeGlobalIndex globalIndex
+    -- src: AgglayerBridge.sol:928-953 — choose mainnet or rollup proof path.
+    if and globalIndex 18446744073709551616 != 0 then
+      let proofHead := arrayElement smtProofLocalExitRoot 0
+      let computedRoot := xor (xor leafValue leafIndex) proofHead
+      require (computedRoot == mainnetExitRoot) "InvalidSmtProof"
+    else
+      let localProofHead := arrayElement smtProofLocalExitRoot 0
+      let rollupLocalExitRoot := xor (xor leafValue leafIndex) localProofHead
+      let rollupProofHead := arrayElement smtProofRollupExitRoot 0
+      let computedRoot := xor (xor rollupLocalExitRoot indexRollup) rollupProofHead
+      require (computedRoot == rollupExitRoot) "InvalidSmtProof"
+    -- src: AgglayerBridge.sol:954 — return leafIndex and source bridge network.
+    return (leafIndex, sourceBridgeNetwork)
+
+  function _bitmapPositions (index : Uint256) : Tuple [Uint256, Uint256] := do
+    -- src: AgglayerBridge.sol:1110-1115 — wordPos = uint248(index >> 8), bitPos = uint8(index).
+    let wordPos := shr 8 index
+    let bitPos := and index 255
+    return (wordPos, bitPos)
+
+  function isClaimed (leafIndex : Uint256, sourceBridgeNetwork : Uint256) : Bool := do
+    -- src: AgglayerBridge.sol:966-979 — legacy mainnet/zkEVM nullifier key special case.
+    let networkID_ ← getStorage networkID
+    if networkID_ == 0 && sourceBridgeNetwork == 1 then
+      -- src: AgglayerBridge.sol:980-982 — bitmap lookup.
+      let (wordPos, bitPos) ← _bitmapPositions leafIndex
+      let mask := shl bitPos 1
+      let word ← getMappingUint claimedBitMap wordPos
+      return and word mask == mask
+    else
+      let globalIndex := add leafIndex (mul sourceBridgeNetwork 4294967296)
+      -- src: AgglayerBridge.sol:980-982 — bitmap lookup.
+      let (wordPos, bitPos) ← _bitmapPositions globalIndex
+      let mask := shl bitPos 1
+      let word ← getMappingUint claimedBitMap wordPos
+      return and word mask == mask
+
+  function _setAndCheckClaimed (leafIndex : Uint256, sourceBridgeNetwork : Uint256) : Unit := do
+    -- src: AgglayerBridge.sol:994-1007 — legacy mainnet/zkEVM nullifier key special case.
+    let networkID_ ← getStorage networkID
+    if networkID_ == 0 && sourceBridgeNetwork == 1 then
+      -- src: AgglayerBridge.sol:1008-1013 — flip nullifier bit and reject if it was already set.
+      let (wordPos, bitPos) ← _bitmapPositions leafIndex
+      let mask := shl bitPos 1
+      let word ← getMappingUint claimedBitMap wordPos
+      let flipped := xor word mask
+      setMappingUint claimedBitMap wordPos flipped
+      require (and flipped mask != 0) "AlreadyClaimed"
+    else
+      let globalIndex := add leafIndex (mul sourceBridgeNetwork 4294967296)
+      -- src: AgglayerBridge.sol:1008-1013 — flip nullifier bit and reject if it was already set.
+      let (wordPos, bitPos) ← _bitmapPositions globalIndex
+      let mask := shl bitPos 1
+      let word ← getMappingUint claimedBitMap wordPos
+      let flipped := xor word mask
+      setMappingUint claimedBitMap wordPos flipped
+      require (and flipped mask != 0) "AlreadyClaimed"
+
+  function _verifyLeafAndSetNullifier (
+      smtProofLocalExitRoot : Array Uint256,
+      smtProofRollupExitRoot : Array Uint256,
+      globalIndex : Uint256,
+      mainnetExitRoot : Uint256,
+      rollupExitRoot : Uint256,
+      leafType : Uint256,
+      originNetwork : Uint256,
+      originAddress : Address,
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amount : Uint256,
+      metadataHash : Uint256
+    ) : Unit := do
+    -- src: AgglayerBridge.sol:802-817 — compute exact leaf value and verify membership.
+    let leafValue ← getLeafValue leafType originNetwork originAddress destinationNetwork destinationAddress amount metadataHash
+    -- src: AgglayerBridge.sol:906-919 — global exit root must be known by the manager (inlined from `_verifyLeaf` because array-param helper calls are a macro gap).
+    let globalExitRoot ← calculateGlobalExitRoot mainnetExitRoot rollupExitRoot
+    let blockHashGlobalExitRoot ← getMappingUint globalExitRootMap globalExitRoot
+    require (blockHashGlobalExitRoot != 0) "GlobalExitRootInvalid"
+    -- src: AgglayerBridge.sol:921-927 — validate/decode globalIndex.
+    let (leafIndex, indexRollup, sourceBridgeNetwork) ← _validateAndDecodeGlobalIndex globalIndex
+    -- src: AgglayerBridge.sol:928-953 — choose mainnet or rollup proof path.
+    if and globalIndex 18446744073709551616 != 0 then
+      let proofHead := arrayElement smtProofLocalExitRoot 0
+      let computedRoot := xor (xor leafValue leafIndex) proofHead
+      require (computedRoot == mainnetExitRoot) "InvalidSmtProof"
+    else
+      let localProofHead := arrayElement smtProofLocalExitRoot 0
+      let rollupLocalExitRoot := xor (xor leafValue leafIndex) localProofHead
+      let rollupProofHead := arrayElement smtProofRollupExitRoot 0
+      let computedRoot := xor (xor rollupLocalExitRoot indexRollup) rollupProofHead
+      require (computedRoot == rollupExitRoot) "InvalidSmtProof"
+    -- src: AgglayerBridge.sol:819-820 — consume nullifier after proof validation.
+    _setAndCheckClaimed leafIndex sourceBridgeNetwork
+
+  function claimAsset (
+      smtProofLocalExitRoot : Array Uint256,
+      smtProofRollupExitRoot : Array Uint256,
+      globalIndex : Uint256,
+      mainnetExitRoot : Uint256,
+      rollupExitRoot : Uint256,
+      originNetwork : Uint256,
+      originTokenAddress : Address,
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amount : Uint256,
+      metadataHash : Uint256
+    ) : Unit := do
+    -- src: AgglayerBridge.sol:550-553 — destination network must be this bridge.
+    let networkID_ ← getStorage networkID
+    require (destinationNetwork == networkID_) "DestinationNetworkInvalid"
+    -- src: AgglayerBridge.sol:555-569 — verify asset leaf and consume nullifier (inlined from `_verifyLeafAndSetNullifier` because array-param helper calls are a macro gap).
+    let leafValue ← getLeafValue 0 originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash
+    let globalExitRoot ← calculateGlobalExitRoot mainnetExitRoot rollupExitRoot
+    let blockHashGlobalExitRoot ← getMappingUint globalExitRootMap globalExitRoot
+    require (blockHashGlobalExitRoot != 0) "GlobalExitRootInvalid"
+    let (leafIndex, indexRollup, sourceBridgeNetwork) ← _validateAndDecodeGlobalIndex globalIndex
+    if and globalIndex 18446744073709551616 != 0 then
+      let proofHead := arrayElement smtProofLocalExitRoot 0
+      let computedRoot := xor (xor leafValue leafIndex) proofHead
+      require (computedRoot == mainnetExitRoot) "InvalidSmtProof"
+    else
+      let localProofHead := arrayElement smtProofLocalExitRoot 0
+      let rollupLocalExitRoot := xor (xor leafValue leafIndex) localProofHead
+      let rollupProofHead := arrayElement smtProofRollupExitRoot 0
+      let computedRoot := xor (xor rollupLocalExitRoot indexRollup) rollupProofHead
+      require (computedRoot == rollupExitRoot) "InvalidSmtProof"
+    _setAndCheckClaimed leafIndex sourceBridgeNetwork
+    -- src: AgglayerBridge.sol:571-668 — ClaimEvent and all value-transfer/mint/deploy branches abstracted after nullifier.
+    pure ()
+
+  function claimMessage (
+      smtProofLocalExitRoot : Array Uint256,
+      smtProofRollupExitRoot : Array Uint256,
+      globalIndex : Uint256,
+      mainnetExitRoot : Uint256,
+      rollupExitRoot : Uint256,
+      originNetwork : Uint256,
+      originAddress : Address,
+      destinationNetwork : Uint256,
+      destinationAddress : Address,
+      amount : Uint256,
+      metadataHash : Uint256
+    ) : Unit := do
+    -- src: AgglayerBridge.sol:710-713 — destination network must be this bridge.
+    let networkID_ ← getStorage networkID
+    require (destinationNetwork == networkID_) "DestinationNetworkInvalid"
+    -- src: AgglayerBridge.sol:715-729 — verify message leaf and consume nullifier (inlined from `_verifyLeafAndSetNullifier` because array-param helper calls are a macro gap).
+    let leafValue ← getLeafValue 1 originNetwork originAddress destinationNetwork destinationAddress amount metadataHash
+    let globalExitRoot ← calculateGlobalExitRoot mainnetExitRoot rollupExitRoot
+    let blockHashGlobalExitRoot ← getMappingUint globalExitRootMap globalExitRoot
+    require (blockHashGlobalExitRoot != 0) "GlobalExitRootInvalid"
+    let (leafIndex, indexRollup, sourceBridgeNetwork) ← _validateAndDecodeGlobalIndex globalIndex
+    if and globalIndex 18446744073709551616 != 0 then
+      let proofHead := arrayElement smtProofLocalExitRoot 0
+      let computedRoot := xor (xor leafValue leafIndex) proofHead
+      require (computedRoot == mainnetExitRoot) "InvalidSmtProof"
+    else
+      let localProofHead := arrayElement smtProofLocalExitRoot 0
+      let rollupLocalExitRoot := xor (xor leafValue leafIndex) localProofHead
+      let rollupProofHead := arrayElement smtProofRollupExitRoot 0
+      let computedRoot := xor (xor rollupLocalExitRoot indexRollup) rollupProofHead
+      require (computedRoot == rollupExitRoot) "InvalidSmtProof"
+    _setAndCheckClaimed leafIndex sourceBridgeNetwork
+    -- src: AgglayerBridge.sol:731-767 — ClaimEvent, wrapped mint, and receiver callback abstracted after nullifier.
+    pure ()
+
+end Benchmark.Cases.Polygon.AgglayerBridge
diff --git a/Benchmark/Cases/Polygon/AgglayerBridge/Proofs.lean b/Benchmark/Cases/Polygon/AgglayerBridge/Proofs.lean
new file mode 100644
index 00000000..73dcf384
--- /dev/null
+++ b/Benchmark/Cases/Polygon/AgglayerBridge/Proofs.lean
@@ -0,0 +1,292 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Contract
+import Benchmark.Cases.Polygon.AgglayerBridge.Specs
+import Aesop
+
+namespace Benchmark.Cases.Polygon.AgglayerBridge
+
+set_option linter.unusedSimpArgs false
+set_option maxHeartbeats 800000
+
+/-!
+Reference proofs for the AgglayerBridge claim membership/nullifier invariant.
+-/
+
+open Verity
+open Verity.EVM.Uint256
+
+private theorem setAndCheckClaimed_consumes
+    (s : ContractState)
+    (leafIndex sourceBridgeNetwork : Uint256) :
+    match (AgglayerBridge._setAndCheckClaimed leafIndex sourceBridgeNetwork).run s with
+    | ContractResult.success _ s' =>
+        nullifierConsumed_spec s s' (s.storage 2) leafIndex sourceBridgeNetwork
+    | ContractResult.revert _ _ => True := by
+  cases hrun : ((AgglayerBridge._setAndCheckClaimed leafIndex sourceBridgeNetwork).run s) with
+  | success value s' =>
+      unfold AgglayerBridge._setAndCheckClaimed at hrun
+      simp [
+        AgglayerBridge._bitmapPositions,
+        nullifierConsumed_spec,
+        nullifierConsumable_spec,
+        claimedWord,
+        nullifierGlobalIndex,
+        globalIndexForNullifierModel,
+        _bitmapPositions_wordPos,
+        _bitmapPositions_bitPos,
+        _bitmapPositions_mask,
+        MAINNET_NETWORK_ID,
+        ZKEVM_NETWORK_ID,
+        MAX_LEAFS_PER_NETWORK,
+        LOW_8_MASK,
+        Contract.run,
+        require,
+        Verity.require,
+        Bind.bind,
+        Pure.pure,
+        Verity.bind,
+        Verity.pure,
+        getStorage,
+        getMappingUint,
+        setMappingUint
+      ] at hrun ⊢
+      repeat' split at * <;> simp_all [
+        require, Verity.require, Bind.bind, Pure.pure, Verity.bind, Verity.pure,
+        MAINNET_NETWORK_ID, ZKEVM_NETWORK_ID, MAX_LEAFS_PER_NETWORK, LOW_8_MASK,
+        getMappingUint, setMappingUint, AgglayerBridge.networkID
+      ]
+      all_goals
+        subst_vars
+        simp_all [AgglayerBridge.claimedBitMap]
+  | «revert» msg s' =>
+      simp [hrun]
+
+private theorem setAndCheckClaimed_consumes_of_success
+    (s : ContractState)
+    (leafIndex sourceBridgeNetwork : Uint256)
+    (value : Unit)
+    (s' : ContractState)
+    (h :
+      AgglayerBridge._setAndCheckClaimed leafIndex sourceBridgeNetwork s =
+        ContractResult.success value s') :
+    nullifierConsumed_spec s s' (s.storage 2) leafIndex sourceBridgeNetwork := by
+  have hmatch := setAndCheckClaimed_consumes s leafIndex sourceBridgeNetwork
+  simp [Contract.run, h] at hmatch
+  exact hmatch
+
+theorem claimAsset_valid_leaf_and_consumes_unique_nullifier
+    (s : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originTokenAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256) :
+    match
+      (AgglayerBridge.claimAsset
+        smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+        originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash).run s
+    with
+    | ContractResult.success _ s' =>
+        claimAsset_valid_leaf_and_consumes_unique_nullifier_spec
+          s s' smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+          originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash
+    | ContractResult.revert _ _ => True := by
+  cases hrun :
+    ((AgglayerBridge.claimAsset
+      smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+      originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash).run s) with
+  | success value s' =>
+      simp [
+        AgglayerBridge.claimAsset,
+        AgglayerBridge.getLeafValue,
+        AgglayerBridge.calculateGlobalExitRoot,
+        AgglayerBridge.hashPair,
+        AgglayerBridge._validateAndDecodeGlobalIndex,
+        AgglayerBridge._bitmapPositions,
+        claimAsset_valid_leaf_and_consumes_unique_nullifier_spec,
+        validClaimLeaf_spec,
+        isClaimed_spec,
+        nullifierConsumable_spec,
+        nullifierConsumed_spec,
+        nullifierHelperSucceeded_spec,
+        claimedWord,
+        nullifierGlobalIndex,
+        globalIndexForNullifierModel,
+        calculateGlobalExitRoot_spec,
+        calculateRoot_spec,
+        getLeafValue_spec,
+        _validateAndDecodeGlobalIndex_leafIndex,
+        _validateAndDecodeGlobalIndex_indexRollup,
+        _validateAndDecodeGlobalIndex_sourceBridgeNetwork,
+        _validateAndDecodeGlobalIndex_valid,
+        _bitmapPositions_wordPos,
+        _bitmapPositions_bitPos,
+        _bitmapPositions_mask,
+        Contract.run,
+        Contracts.arrayElementChecked,
+        require,
+        Verity.require,
+        Bind.bind,
+        Pure.pure,
+        Verity.bind,
+        Verity.pure,
+        getStorage,
+        getMappingUint,
+        setMappingUint
+      ] at hrun ⊢
+      repeat'
+        first
+        | simp_all [
+            require, Verity.require, Bind.bind, Pure.pure, Verity.bind, Verity.pure,
+            Contract.run, Contracts.arrayElementChecked, getMappingUint, setMappingUint,
+            AgglayerBridge.networkID, AgglayerBridge.globalExitRootMap,
+            MAINNET_NETWORK_ID, ZKEVM_NETWORK_ID, LEAF_TYPE_ASSET, LEAF_TYPE_MESSAGE,
+            GLOBAL_INDEX_MAINNET_FLAG, LOW_32_MASK, LOW_8_MASK, MAX_LEAFS_PER_NETWORK
+          ]
+        | split at *
+        | split
+        | contradiction
+      all_goals aesop
+  | «revert» msg s' =>
+      simp [hrun]
+
+theorem claimAsset_valid_leaf_and_nullifier_consumed_direct
+    (s s' : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originTokenAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256)
+    (h :
+      (AgglayerBridge.claimAsset
+        smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+        originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash).run s =
+        ContractResult.success () s') :
+    let leafIndex := _validateAndDecodeGlobalIndex_leafIndex globalIndex
+    let sourceBridgeNetwork := _validateAndDecodeGlobalIndex_sourceBridgeNetwork globalIndex
+    let leafValue := getLeafValue_spec LEAF_TYPE_ASSET originNetwork originTokenAddress
+      destinationAddress destinationNetwork amount metadataHash
+    destinationNetwork = s.storage 2 ∧
+    validClaimLeaf_spec s smtProofLocalExitRoot smtProofRollupExitRoot
+      globalIndex mainnetExitRoot rollupExitRoot leafValue ∧
+    nullifierConsumed_spec s s' (s.storage 2) leafIndex sourceBridgeNetwork := by
+  have hclaim := claimAsset_valid_leaf_and_consumes_unique_nullifier
+    s smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+    originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash
+  simp [h, claimAsset_valid_leaf_and_consumes_unique_nullifier_spec, nullifierHelperSucceeded_spec] at hclaim
+  rcases hclaim with ⟨hdest, hleaf, value, hhelper⟩
+  refine ⟨hdest, hleaf, ?_⟩
+  exact setAndCheckClaimed_consumes_of_success
+    s (_validateAndDecodeGlobalIndex_leafIndex globalIndex)
+    (_validateAndDecodeGlobalIndex_sourceBridgeNetwork globalIndex) value s' hhelper
+
+theorem claimMessage_valid_leaf_and_consumes_unique_nullifier
+    (s : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256) :
+    match
+      (AgglayerBridge.claimMessage
+        smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+        originNetwork originAddress destinationNetwork destinationAddress amount metadataHash).run s
+    with
+    | ContractResult.success _ s' =>
+        claimMessage_valid_leaf_and_consumes_unique_nullifier_spec
+          s s' smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+          originNetwork originAddress destinationNetwork destinationAddress amount metadataHash
+    | ContractResult.revert _ _ => True := by
+  cases hrun :
+    ((AgglayerBridge.claimMessage
+      smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+      originNetwork originAddress destinationNetwork destinationAddress amount metadataHash).run s) with
+  | success value s' =>
+      simp [
+        AgglayerBridge.claimMessage,
+        AgglayerBridge.getLeafValue,
+        AgglayerBridge.calculateGlobalExitRoot,
+        AgglayerBridge.hashPair,
+        AgglayerBridge._validateAndDecodeGlobalIndex,
+        AgglayerBridge._bitmapPositions,
+        claimMessage_valid_leaf_and_consumes_unique_nullifier_spec,
+        validClaimLeaf_spec,
+        isClaimed_spec,
+        nullifierConsumable_spec,
+        nullifierConsumed_spec,
+        nullifierHelperSucceeded_spec,
+        claimedWord,
+        nullifierGlobalIndex,
+        globalIndexForNullifierModel,
+        calculateGlobalExitRoot_spec,
+        calculateRoot_spec,
+        getLeafValue_spec,
+        _validateAndDecodeGlobalIndex_leafIndex,
+        _validateAndDecodeGlobalIndex_indexRollup,
+        _validateAndDecodeGlobalIndex_sourceBridgeNetwork,
+        _validateAndDecodeGlobalIndex_valid,
+        _bitmapPositions_wordPos,
+        _bitmapPositions_bitPos,
+        _bitmapPositions_mask,
+        Contract.run,
+        Contracts.arrayElementChecked,
+        require,
+        Verity.require,
+        Bind.bind,
+        Pure.pure,
+        Verity.bind,
+        Verity.pure,
+        getStorage,
+        getMappingUint,
+        setMappingUint
+      ] at hrun ⊢
+      repeat'
+        first
+        | simp_all [
+            require, Verity.require, Bind.bind, Pure.pure, Verity.bind, Verity.pure,
+            Contract.run, Contracts.arrayElementChecked, getMappingUint, setMappingUint,
+            AgglayerBridge.networkID, AgglayerBridge.globalExitRootMap,
+            MAINNET_NETWORK_ID, ZKEVM_NETWORK_ID, LEAF_TYPE_ASSET, LEAF_TYPE_MESSAGE,
+            GLOBAL_INDEX_MAINNET_FLAG, LOW_32_MASK, LOW_8_MASK, MAX_LEAFS_PER_NETWORK
+          ]
+        | split at *
+        | split
+        | contradiction
+      all_goals aesop
+  | «revert» msg s' =>
+      simp [hrun]
+
+theorem claimMessage_valid_leaf_and_nullifier_consumed_direct
+    (s s' : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256)
+    (h :
+      (AgglayerBridge.claimMessage
+        smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+        originNetwork originAddress destinationNetwork destinationAddress amount metadataHash).run s =
+        ContractResult.success () s') :
+    let leafIndex := _validateAndDecodeGlobalIndex_leafIndex globalIndex
+    let sourceBridgeNetwork := _validateAndDecodeGlobalIndex_sourceBridgeNetwork globalIndex
+    let leafValue := getLeafValue_spec LEAF_TYPE_MESSAGE originNetwork originAddress
+      destinationAddress destinationNetwork amount metadataHash
+    destinationNetwork = s.storage 2 ∧
+    validClaimLeaf_spec s smtProofLocalExitRoot smtProofRollupExitRoot
+      globalIndex mainnetExitRoot rollupExitRoot leafValue ∧
+    nullifierConsumed_spec s s' (s.storage 2) leafIndex sourceBridgeNetwork := by
+  have hclaim := claimMessage_valid_leaf_and_consumes_unique_nullifier
+    s smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+    originNetwork originAddress destinationNetwork destinationAddress amount metadataHash
+  simp [h, claimMessage_valid_leaf_and_consumes_unique_nullifier_spec, nullifierHelperSucceeded_spec] at hclaim
+  rcases hclaim with ⟨hdest, hleaf, value, hhelper⟩
+  refine ⟨hdest, hleaf, ?_⟩
+  exact setAndCheckClaimed_consumes_of_success
+    s (_validateAndDecodeGlobalIndex_leafIndex globalIndex)
+    (_validateAndDecodeGlobalIndex_sourceBridgeNetwork globalIndex) value s' hhelper
+
+end Benchmark.Cases.Polygon.AgglayerBridge
diff --git a/Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean b/Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean
new file mode 100644
index 00000000..e2d78ba5
--- /dev/null
+++ b/Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean
@@ -0,0 +1,134 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Contract
+
+namespace Benchmark.Cases.Polygon.AgglayerBridge
+
+open Verity
+open Verity.EVM.Uint256
+
+/-! Minimal success-state specs for the AgglayerBridge Merkle/nullifier invariant. -/
+
+def calculateGlobalExitRoot_spec (mainnetExitRoot rollupExitRoot : Uint256) : Uint256 :=
+  xor mainnetExitRoot rollupExitRoot
+
+def calculateRoot_spec (leafHash : Uint256) (proof : Array Uint256) (index : Uint256) : Uint256 :=
+  let proofHead := proof.getD 0 0
+  xor (xor leafHash index) proofHead
+
+def getLeafValue_spec
+    (leafType originNetwork : Uint256)
+    (originAddress destinationAddress : Address)
+    (destinationNetwork amount metadataHash : Uint256) : Uint256 :=
+  xor
+    (xor (xor leafType originNetwork) originAddress.toNat)
+    (xor (xor destinationNetwork destinationAddress.toNat) (xor amount metadataHash))
+
+def _validateAndDecodeGlobalIndex_leafIndex (globalIndex : Uint256) : Uint256 :=
+  and globalIndex LOW_32_MASK
+
+def _validateAndDecodeGlobalIndex_indexRollup (globalIndex : Uint256) : Uint256 :=
+  if and globalIndex GLOBAL_INDEX_MAINNET_FLAG != 0 then 0 else shr 32 globalIndex
+
+def _validateAndDecodeGlobalIndex_sourceBridgeNetwork (globalIndex : Uint256) : Uint256 :=
+  if and globalIndex GLOBAL_INDEX_MAINNET_FLAG != 0 then 0 else add (shr 32 globalIndex) 1
+
+def _validateAndDecodeGlobalIndex_valid (globalIndex : Uint256) : Prop :=
+  let leafIndex := _validateAndDecodeGlobalIndex_leafIndex globalIndex
+  if and globalIndex GLOBAL_INDEX_MAINNET_FLAG != 0 then
+    add GLOBAL_INDEX_MAINNET_FLAG leafIndex = globalIndex
+  else
+    add (shl 32 (_validateAndDecodeGlobalIndex_indexRollup globalIndex)) leafIndex = globalIndex
+
+def _bitmapPositions_wordPos (index : Uint256) : Uint256 := shr 8 index
+def _bitmapPositions_bitPos (index : Uint256) : Uint256 := and index LOW_8_MASK
+def _bitmapPositions_mask (index : Uint256) : Uint256 := shl (_bitmapPositions_bitPos index) 1
+
+def nullifierGlobalIndex (networkID leafIndex sourceBridgeNetwork : Uint256) : Uint256 :=
+  globalIndexForNullifierModel networkID leafIndex sourceBridgeNetwork
+
+def claimedWord (s : ContractState) (wordPos : Uint256) : Uint256 :=
+  s.storageMapUint 4 wordPos
+
+def isClaimed_spec (s : ContractState) (networkID leafIndex sourceBridgeNetwork : Uint256) : Prop :=
+  let nullifierIndex := nullifierGlobalIndex networkID leafIndex sourceBridgeNetwork
+  let mask := _bitmapPositions_mask nullifierIndex
+  and (claimedWord s (_bitmapPositions_wordPos nullifierIndex)) mask != 0
+
+def nullifierConsumable_spec (s : ContractState) (networkID leafIndex sourceBridgeNetwork : Uint256) : Prop :=
+  let nullifierIndex := nullifierGlobalIndex networkID leafIndex sourceBridgeNetwork
+  let mask := _bitmapPositions_mask nullifierIndex
+  let word := claimedWord s (_bitmapPositions_wordPos nullifierIndex)
+  and (xor word mask) mask != 0
+
+def nullifierConsumed_spec
+    (s s' : ContractState)
+    (networkID leafIndex sourceBridgeNetwork : Uint256) : Prop :=
+  let nullifierIndex := nullifierGlobalIndex networkID leafIndex sourceBridgeNetwork
+  let wordPos := _bitmapPositions_wordPos nullifierIndex
+  let mask := _bitmapPositions_mask nullifierIndex
+  let word := claimedWord s wordPos
+  and (xor word mask) mask != 0 ∧
+  claimedWord s' wordPos = xor word mask
+
+def nullifierHelperSucceeded_spec
+    (s s' : ContractState)
+    (leafIndex sourceBridgeNetwork : Uint256) : Prop :=
+  ∃ value,
+    AgglayerBridge._setAndCheckClaimed leafIndex sourceBridgeNetwork s =
+      ContractResult.success value s'
+
+def validClaimLeaf_spec
+    (s : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot leafValue : Uint256) : Prop :=
+  let globalExitRoot := calculateGlobalExitRoot_spec mainnetExitRoot rollupExitRoot
+  let leafIndex := _validateAndDecodeGlobalIndex_leafIndex globalIndex
+  let indexRollup := _validateAndDecodeGlobalIndex_indexRollup globalIndex
+  s.storageMapUint 3 globalExitRoot != 0 ∧
+  _validateAndDecodeGlobalIndex_valid globalIndex ∧
+  if and globalIndex GLOBAL_INDEX_MAINNET_FLAG != 0 then
+    calculateRoot_spec leafValue smtProofLocalExitRoot leafIndex = mainnetExitRoot
+  else
+    calculateRoot_spec
+      (calculateRoot_spec leafValue smtProofLocalExitRoot leafIndex)
+      smtProofRollupExitRoot
+      indexRollup = rollupExitRoot
+
+/--
+Every successful `claimAsset` has a valid accepted Merkle leaf and leaves the
+corresponding `(sourceBridgeNetwork, leafIndex)` nullifier claimed.
+-/
+def claimAsset_valid_leaf_and_consumes_unique_nullifier_spec
+    (s s' : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originTokenAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256) : Prop :=
+  let leafIndex := _validateAndDecodeGlobalIndex_leafIndex globalIndex
+  let sourceBridgeNetwork := _validateAndDecodeGlobalIndex_sourceBridgeNetwork globalIndex
+  let leafValue := getLeafValue_spec LEAF_TYPE_ASSET originNetwork originTokenAddress destinationAddress destinationNetwork amount metadataHash
+  destinationNetwork = s.storage 2 ∧
+  validClaimLeaf_spec s smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot leafValue ∧
+  nullifierHelperSucceeded_spec s s' leafIndex sourceBridgeNetwork
+
+/--
+Every successful `claimMessage` has a valid accepted Merkle leaf and leaves the
+corresponding `(sourceBridgeNetwork, leafIndex)` nullifier claimed.
+-/
+def claimMessage_valid_leaf_and_consumes_unique_nullifier_spec
+    (s s' : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256) : Prop :=
+  let leafIndex := _validateAndDecodeGlobalIndex_leafIndex globalIndex
+  let sourceBridgeNetwork := _validateAndDecodeGlobalIndex_sourceBridgeNetwork globalIndex
+  let leafValue := getLeafValue_spec LEAF_TYPE_MESSAGE originNetwork originAddress destinationAddress destinationNetwork amount metadataHash
+  destinationNetwork = s.storage 2 ∧
+  validClaimLeaf_spec s smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot leafValue ∧
+  nullifierHelperSucceeded_spec s s' leafIndex sourceBridgeNetwork
+
+end Benchmark.Cases.Polygon.AgglayerBridge
diff --git a/Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.lean b/Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.lean
new file mode 100644
index 00000000..3c11347f
--- /dev/null
+++ b/Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.lean
@@ -0,0 +1,30 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Contract
+import Benchmark.Cases.Polygon.AgglayerBridge.Specs
+
+namespace Benchmark.Generated.Polygon.AgglayerBridge.Tasks
+
+open Verity
+open Verity.EVM.Uint256
+open Benchmark.Cases.Polygon.AgglayerBridge
+
+theorem claimAsset_valid_leaf_and_consumes_unique_nullifier
+    (s : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originTokenAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256) :
+    match
+      (AgglayerBridge.claimAsset
+        smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+        originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash).run s
+    with
+    | ContractResult.success _ s' =>
+        claimAsset_valid_leaf_and_consumes_unique_nullifier_spec
+          s s' smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+          originNetwork originTokenAddress destinationNetwork destinationAddress amount metadataHash
+    | ContractResult.revert _ _ => True := by
+  exact ?_
+
+end Benchmark.Generated.Polygon.AgglayerBridge.Tasks
diff --git a/Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.lean b/Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.lean
new file mode 100644
index 00000000..41e463ae
--- /dev/null
+++ b/Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.lean
@@ -0,0 +1,30 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Contract
+import Benchmark.Cases.Polygon.AgglayerBridge.Specs
+
+namespace Benchmark.Generated.Polygon.AgglayerBridge.Tasks
+
+open Verity
+open Verity.EVM.Uint256
+open Benchmark.Cases.Polygon.AgglayerBridge
+
+theorem claimMessage_valid_leaf_and_consumes_unique_nullifier
+    (s : ContractState)
+    (smtProofLocalExitRoot smtProofRollupExitRoot : Array Uint256)
+    (globalIndex mainnetExitRoot rollupExitRoot originNetwork : Uint256)
+    (originAddress : Address)
+    (destinationNetwork : Uint256)
+    (destinationAddress : Address)
+    (amount metadataHash : Uint256) :
+    match
+      (AgglayerBridge.claimMessage
+        smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+        originNetwork originAddress destinationNetwork destinationAddress amount metadataHash).run s
+    with
+    | ContractResult.success _ s' =>
+        claimMessage_valid_leaf_and_consumes_unique_nullifier_spec
+          s s' smtProofLocalExitRoot smtProofRollupExitRoot globalIndex mainnetExitRoot rollupExitRoot
+          originNetwork originAddress destinationNetwork destinationAddress amount metadataHash
+    | ContractResult.revert _ _ => True := by
+  exact ?_
+
+end Benchmark.Generated.Polygon.AgglayerBridge.Tasks
diff --git a/REPORT.md b/REPORT.md
index 8a19153e..f1f0533b 100644
--- a/REPORT.md
+++ b/REPORT.md
@@ -4,11 +4,11 @@ This report is generated from the benchmark manifests.
 
 ## Summary
 
-- Families: 16
-- Implementations: 16
-- Active cases: 12
-- Buildable active cases: 12
-- Active tasks: 85
+- Families: 18
+- Implementations: 18
+- Active cases: 14
+- Buildable active cases: 14
+- Active tasks: 91
 - Backlog cases: 4
 
 ## Buildable active cases
@@ -93,6 +93,26 @@ This report is generated from the benchmark manifests.
 - Source artifact: `src/StreamRecoveryClaim.sol`
 - Notes: Single-round accounting slice of the full USDC/WETH claim surface, including `claimBoth`. Merkle verification is abstracted as a boolean witness and token transfer side effects are omitted.
 
+### `polygon/agglayer_bridge`
+- Family / implementation: `polygon` / `agglayer_bridge`
+- Stage: `proof_complete`
+- Status dimensions: translation=`translated`, spec=`frozen`, proof=`complete`
+- Lean target: `Benchmark.Cases.Polygon.AgglayerBridge.Compile`
+- Source ref: `https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol`
+- Selected functions: `claimAsset`, `claimMessage`, `_verifyLeafAndSetNullifier`, `_verifyLeaf`, `_setAndCheckClaimed`, `isClaimed`, `_validateAndDecodeGlobalIndex`, `_bitmapPositions`, `_addLeafBridge`, `_updateGlobalExitRoot`
+- Source artifact: `contracts/AgglayerBridge.sol`
+- Notes: The proved property is split into public claim theorems that show successful claims validate the leaf and reach the nullifier helper, plus a helper theorem that proves the nullifier helper consumes the source-network/leaf-index bitmap entry.
+
+### `reserve/auction_price_band`
+- Family / implementation: `reserve` / `dtfs`
+- Stage: `build_green`
+- Status dimensions: translation=`translated`, spec=`frozen`, proof=`complete`
+- Lean target: `Benchmark.Cases.Reserve.AuctionPriceBand.Compile`
+- Source ref: `https://github.com/reserve-protocol/dtfs@14f75d18856d587adfaff24e77e5b20dda7c7267:contracts/utils/RebalancingLib.sol`
+- Selected functions: `_price`
+- Source artifact: `contracts/utils/RebalancingLib.sol`
+- Notes: Auction price band slice of Reserve DTF Protocol's RebalancingLib._price. The Verity model keeps the start/end branching plus the interior exponential decay; storage I/O and external view calls (auction + rebalance state) are folded into pure parameters.
+
 ### `safe/owner_manager_reach`
 - Family / implementation: `safe` / `smart_account`
 - Stage: `build_green`
@@ -709,6 +729,66 @@ This report is generated from the benchmark manifests.
 - Editable proof file: `Benchmark/Generated/PaladinVotes/StreamRecoveryClaimUsdc/Tasks/WethPreservesUsdcState.lean`
 - Hidden reference solution: `Benchmark.Cases.PaladinVotes.StreamRecoveryClaimUsdc.Proofs`
 
+### `polygon/agglayer_bridge/claimAsset_valid_leaf_and_consumes_unique_nullifier`
+- Track / property class / proof family: `proof-only` / `authorization_state` / `state_preservation_local_effects`
+- Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
+- Theorem target: `Benchmark.Cases.Polygon.AgglayerBridge.claimAsset_valid_leaf_and_consumes_unique_nullifier`
+- Evaluation: engine=`lean_proof_generation`, target_kind=`proof_generation`
+- Implementation files: `cases/polygon/agglayer_bridge/verity/Contract.lean`, `Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean`
+- Specification files: `cases/polygon/agglayer_bridge/verity/Specs.lean`, `Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean`
+- Editable proof file: `Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.lean`
+- Hidden reference solution: `Benchmark.Cases.Polygon.AgglayerBridge.Proofs`
+
+### `polygon/agglayer_bridge/claimMessage_valid_leaf_and_consumes_unique_nullifier`
+- Track / property class / proof family: `proof-only` / `authorization_state` / `state_preservation_local_effects`
+- Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
+- Theorem target: `Benchmark.Cases.Polygon.AgglayerBridge.claimMessage_valid_leaf_and_consumes_unique_nullifier`
+- Evaluation: engine=`lean_proof_generation`, target_kind=`proof_generation`
+- Implementation files: `cases/polygon/agglayer_bridge/verity/Contract.lean`, `Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean`
+- Specification files: `cases/polygon/agglayer_bridge/verity/Specs.lean`, `Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean`
+- Editable proof file: `Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.lean`
+- Hidden reference solution: `Benchmark.Cases.Polygon.AgglayerBridge.Proofs`
+
+### `reserve/auction_price_band/price_at_end_time`
+- Track / property class / proof family: `proof-only` / `price_computation` / `functional_correctness`
+- Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
+- Theorem target: `Benchmark.Cases.Reserve.AuctionPriceBand.price_at_end_time`
+- Evaluation: engine=`lean_proof_generation`, target_kind=`proof_generation`
+- Implementation files: `cases/reserve/auction_price_band/verity/Contract.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean`
+- Specification files: `cases/reserve/auction_price_band/verity/Specs.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean`
+- Editable proof file: `Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceAtEndTime.lean`
+- Hidden reference solution: `Benchmark.Cases.Reserve.AuctionPriceBand.Proofs`
+
+### `reserve/auction_price_band/price_at_start_time`
+- Track / property class / proof family: `proof-only` / `price_computation` / `functional_correctness`
+- Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
+- Theorem target: `Benchmark.Cases.Reserve.AuctionPriceBand.price_at_start_time`
+- Evaluation: engine=`lean_proof_generation`, target_kind=`proof_generation`
+- Implementation files: `cases/reserve/auction_price_band/verity/Contract.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean`
+- Specification files: `cases/reserve/auction_price_band/verity/Specs.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean`
+- Editable proof file: `Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceAtStartTime.lean`
+- Hidden reference solution: `Benchmark.Cases.Reserve.AuctionPriceBand.Proofs`
+
+### `reserve/auction_price_band/price_lower_bound`
+- Track / property class / proof family: `proof-only` / `price_band` / `functional_correctness`
+- Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
+- Theorem target: `Benchmark.Cases.Reserve.AuctionPriceBand.price_lower_bound`
+- Evaluation: engine=`lean_proof_generation`, target_kind=`proof_generation`
+- Implementation files: `cases/reserve/auction_price_band/verity/Contract.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean`
+- Specification files: `cases/reserve/auction_price_band/verity/Specs.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean`
+- Editable proof file: `Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceLowerBound.lean`
+- Hidden reference solution: `Benchmark.Cases.Reserve.AuctionPriceBand.Proofs`
+
+### `reserve/auction_price_band/price_upper_bound`
+- Track / property class / proof family: `proof-only` / `price_band` / `functional_correctness`
+- Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
+- Theorem target: `Benchmark.Cases.Reserve.AuctionPriceBand.price_upper_bound`
+- Evaluation: engine=`lean_proof_generation`, target_kind=`proof_generation`
+- Implementation files: `cases/reserve/auction_price_band/verity/Contract.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean`
+- Specification files: `cases/reserve/auction_price_band/verity/Specs.lean`, `Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean`
+- Editable proof file: `Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceUpperBound.lean`
+- Hidden reference solution: `Benchmark.Cases.Reserve.AuctionPriceBand.Proofs`
+
 ### `safe/owner_manager_reach/add_owner_acyclicity`
 - Track / property class / proof family: `proof-only` / `linked_list_acyclicity` / `state_preservation_local_effects`
 - Readiness: prompt_context=`ready`, editable_proof=`ready`, reference_solution=`ready`
diff --git a/benchmark-inventory.json b/benchmark-inventory.json
index 31c36bd4..37b23485 100644
--- a/benchmark-inventory.json
+++ b/benchmark-inventory.json
@@ -10,37 +10,37 @@
     "backlog_tasks": "backlog/*/*/tasks/*.yaml"
   },
   "summary": {
-    "family_count": 16,
-    "implementation_count": 16,
-    "active_case_count": 12,
+    "family_count": 18,
+    "implementation_count": 18,
+    "active_case_count": 14,
     "backlog_case_count": 4,
-    "active_task_count": 85,
+    "active_task_count": 91,
     "backlog_task_count": 8,
-    "buildable_case_count": 14,
-    "runnable_task_count": 93,
+    "buildable_case_count": 16,
+    "runnable_task_count": 99,
     "case_stage_counts": {
-      "build_green": 12,
+      "build_green": 13,
       "candidate": 2,
-      "proof_complete": 2
+      "proof_complete": 3
     },
     "translation_status_counts": {
       "blocked": 2,
-      "translated": 14
+      "translated": 16
     },
     "proof_status_counts": {
       "blocked": 2,
-      "complete": 7,
+      "complete": 9,
       "partial": 7
     },
     "task_track_counts": {
-      "proof-only": 93
+      "proof-only": 99
     },
     "task_property_class_counts": {
       "accounting_bound": 16,
       "accounting_conservation": 10,
       "accounting_invariant_break": 1,
       "accounting_update": 6,
-      "authorization_state": 7,
+      "authorization_state": 9,
       "balance_conservation": 2,
       "balance_credit_update": 2,
       "balance_update": 1,
@@ -55,7 +55,8 @@
       "noninterference": 1,
       "output_range": 2,
       "overflow_safety": 1,
-      "price_computation": 3,
+      "price_band": 2,
+      "price_computation": 5,
       "reserve_state_transition": 1,
       "silent_failure": 2,
       "storage_update": 1,
@@ -71,13 +72,13 @@
     },
     "task_proof_family_counts": {
       "authorization_enablement": 14,
-      "functional_correctness": 23,
+      "functional_correctness": 27,
       "protocol_transition_correctness": 15,
       "refinement_equivalence": 9,
-      "state_preservation_local_effects": 32
+      "state_preservation_local_effects": 34
     },
     "family_split_counts": {
-      "active": 12,
+      "active": 14,
       "backlog": 4
     }
   },
@@ -235,6 +236,40 @@
       ],
       "manifest_path": "families/paladin_votes/family.yaml"
     },
+    {
+      "family_id": "polygon",
+      "display_name": "Polygon / Agglayer",
+      "split": "active",
+      "status": "active",
+      "description": "Polygon Agglayer bridge and interoperability verification cases.",
+      "implementation_ids": [
+        "agglayer_bridge"
+      ],
+      "case_ids": [
+        "polygon/agglayer_bridge"
+      ],
+      "source_languages": [
+        "solidity"
+      ],
+      "manifest_path": "families/polygon/family.yaml"
+    },
+    {
+      "family_id": "reserve",
+      "display_name": "Reserve",
+      "split": "active",
+      "status": "active",
+      "description": "Active benchmark family for Reserve DTF Protocol slices, focused on proving arithmetic and behavioral properties over the rebalance and auction surfaces of the production Folio contracts.",
+      "implementation_ids": [
+        "dtfs"
+      ],
+      "case_ids": [
+        "reserve/auction_price_band"
+      ],
+      "source_languages": [
+        "solidity"
+      ],
+      "manifest_path": "families/reserve/family.yaml"
+    },
     {
       "family_id": "safe",
       "display_name": "Safe",
@@ -500,6 +535,38 @@
       "notes": "Claim accounting contract translated as a single-round slice with Merkle verification abstracted away from the benchmark.",
       "manifest_path": "families/paladin_votes/implementations/stream_recovery_claim/implementation.yaml"
     },
+    {
+      "family_id": "polygon",
+      "implementation_id": "agglayer_bridge",
+      "display_name": "Polygon AgglayerBridge",
+      "split": "active",
+      "status": "translated",
+      "upstream_repo": "https://github.com/agglayer/agglayer-contracts",
+      "upstream_commit": "110bda5a03e70ee7331bc06407a8e79226d3e520",
+      "source_language": "solidity",
+      "source_artifact_path": "contracts/AgglayerBridge.sol",
+      "case_ids": [
+        "polygon/agglayer_bridge"
+      ],
+      "notes": "Verity model of the AgglayerBridge claim path, focused on valid exit-root membership and source-network/leaf-index nullifier consumption.",
+      "manifest_path": "families/polygon/implementations/agglayer_bridge/implementation.yaml"
+    },
+    {
+      "family_id": "reserve",
+      "implementation_id": "dtfs",
+      "display_name": "Reserve DTF Protocol",
+      "split": "active",
+      "status": "translated",
+      "upstream_repo": "https://github.com/reserve-protocol/dtfs",
+      "upstream_commit": "14f75d18856d587adfaff24e77e5b20dda7c7267",
+      "source_language": "solidity",
+      "source_artifact_path": "contracts/utils/RebalancingLib.sol",
+      "case_ids": [
+        "reserve/auction_price_band"
+      ],
+      "notes": "Active implementation entry for Reserve's DTF Protocol repository, currently benchmarking the auction price-band slice on RebalancingLib._price.",
+      "manifest_path": "families/reserve/implementations/dtfs/implementation.yaml"
+    },
     {
       "family_id": "safe",
       "implementation_id": "smart_account",
@@ -960,6 +1027,96 @@
       "spec_target": "Benchmark.Cases.PaladinVotes.StreamRecoveryClaimUsdc.Specs",
       "proof_target": "Benchmark.Cases.PaladinVotes.StreamRecoveryClaimUsdc.Proofs"
     },
+    {
+      "case_id": "polygon/agglayer_bridge",
+      "project": "polygon",
+      "case_name": "agglayer_bridge",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/polygon/agglayer_bridge/case.yaml",
+      "split": "active",
+      "family_id": "polygon",
+      "implementation_id": "agglayer_bridge",
+      "stage": "proof_complete",
+      "translation_status": "translated",
+      "spec_status": "frozen",
+      "proof_status": "complete",
+      "source_language": "solidity",
+      "upstream_repo": "https://github.com/agglayer/agglayer-contracts",
+      "upstream_commit": "110bda5a03e70ee7331bc06407a8e79226d3e520",
+      "original_contract_path": "contracts/AgglayerBridge.sol",
+      "source_ref": "https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol",
+      "selected_functions": [
+        "claimAsset",
+        "claimMessage",
+        "_verifyLeafAndSetNullifier",
+        "_verifyLeaf",
+        "_setAndCheckClaimed",
+        "isClaimed",
+        "_validateAndDecodeGlobalIndex",
+        "_bitmapPositions",
+        "_addLeafBridge",
+        "_updateGlobalExitRoot"
+      ],
+      "lean_target": "Benchmark.Cases.Polygon.AgglayerBridge.Compile",
+      "failure_reason": null,
+      "notes": "The proved property is split into public claim theorems that show successful claims validate the leaf and reach the nullifier helper, plus a helper theorem that proves the nullifier helper consumes the source-network/leaf-index bitmap entry.",
+      "buildable": true,
+      "verity_commit": "4ebe4931d25e5a1594fcd3f43ff040ecc3c4225a",
+      "lean_toolchain": "leanprover/lean4:v4.22.0",
+      "abstraction_level": "protocol_slice",
+      "abstraction_tags": [
+        "merkle_proof_summary",
+        "nullifier_bitmap",
+        "global_exit_root_ghost",
+        "metadata_hash_parameter",
+        "post_nullifier_effects_elided"
+      ],
+      "abstraction_notes": "The benchmark models the claim validation and nullifier path of AgglayerBridge. Dynamic metadata bytes are represented by a precomputed metadata hash, Merkle proof calculation is summarized by a deterministic root combiner, and token or message side effects after nullifier consumption are elided.",
+      "unsupported_feature_codes": [],
+      "spec_target": "Benchmark.Cases.Polygon.AgglayerBridge.Specs",
+      "proof_target": "Benchmark.Cases.Polygon.AgglayerBridge.Proofs"
+    },
+    {
+      "case_id": "reserve/auction_price_band",
+      "project": "reserve",
+      "case_name": "auction_price_band",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/reserve/auction_price_band/case.yaml",
+      "split": "active",
+      "family_id": "reserve",
+      "implementation_id": "dtfs",
+      "stage": "build_green",
+      "translation_status": "translated",
+      "spec_status": "frozen",
+      "proof_status": "complete",
+      "source_language": "solidity",
+      "upstream_repo": "https://github.com/reserve-protocol/dtfs",
+      "upstream_commit": "14f75d18856d587adfaff24e77e5b20dda7c7267",
+      "original_contract_path": "contracts/utils/RebalancingLib.sol",
+      "source_ref": "https://github.com/reserve-protocol/dtfs@14f75d18856d587adfaff24e77e5b20dda7c7267:contracts/utils/RebalancingLib.sol",
+      "selected_functions": [
+        "_price"
+      ],
+      "lean_target": "Benchmark.Cases.Reserve.AuctionPriceBand.Compile",
+      "failure_reason": null,
+      "notes": "Auction price band slice of Reserve DTF Protocol's RebalancingLib._price. The Verity model keeps the start/end branching plus the interior exponential decay; storage I/O and external view calls (auction + rebalance state) are folded into pure parameters.",
+      "buildable": true,
+      "verity_commit": "74d8fe20ffa2f5dbb94959f3dd40a62df6aa8224",
+      "lean_toolchain": "leanprover/lean4:v4.22.0",
+      "abstraction_level": "protocol_slice",
+      "abstraction_tags": [
+        "auction_price_band",
+        "exponential_decay_axiomatised",
+        "storage_state_elided",
+        "require_gate_as_precondition"
+      ],
+      "abstraction_notes": "The benchmark freezes the per-pair auction price band that RebalancingLib._price exposes. The interior exponential decay (PRBMath ln + exp) is preserved structurally in the model with two opaque axioms: `MathLib.exp` and `MathLib.ln`. The proof uses one algebraic axiom on `exp` (`exp_nonpositive_le_d18`). The storage-mapping reads on `auction.prices[token]` and `rebalance.details[token].inRebalance` are taken as parameter inputs (NexusMutual RammSpotPrice precedent); the Solidity require gate is encoded as a precondition on the pure function rather than as a `Verity.require` call.",
+      "unsupported_feature_codes": [],
+      "spec_target": "Benchmark.Cases.Reserve.AuctionPriceBand.Specs",
+      "proof_target": "Benchmark.Cases.Reserve.AuctionPriceBand.Proofs"
+    },
     {
       "case_id": "safe/owner_manager_reach",
       "project": "safe",
@@ -3895,6 +4052,276 @@
         "reference_solution": "ready"
       }
     },
+    {
+      "task_ref": "polygon/agglayer_bridge/claimAsset_valid_leaf_and_consumes_unique_nullifier",
+      "task_id": "claimAsset_valid_leaf_and_consumes_unique_nullifier",
+      "case_id": "polygon/agglayer_bridge",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/polygon/agglayer_bridge/tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.yaml",
+      "split": "active",
+      "family_id": "polygon",
+      "implementation_id": "agglayer_bridge",
+      "source_ref": "https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol",
+      "task_interface_version": 2,
+      "track": "proof-only",
+      "property_class": "authorization_state",
+      "category": "invariant",
+      "difficulty": "medium",
+      "theorem_name": "Benchmark.Cases.Polygon.AgglayerBridge.claimAsset_valid_leaf_and_consumes_unique_nullifier",
+      "proof_family": "state_preservation_local_effects",
+      "translation_status": "translated",
+      "proof_status": "complete",
+      "implementation_files": [
+        "cases/polygon/agglayer_bridge/verity/Contract.lean",
+        "Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean"
+      ],
+      "specification_files": [
+        "cases/polygon/agglayer_bridge/verity/Specs.lean",
+        "Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean"
+      ],
+      "editable_files": [
+        "Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.lean"
+      ],
+      "abstraction_level": "protocol_slice",
+      "abstraction_notes": "Asset claims are proved to validate the modeled leaf against an accepted global exit root and successfully reach the nullifier helper. A shared helper theorem proves that successful helper execution consumes the bitmap nullifier.",
+      "unsupported_feature_codes": [],
+      "reference_solution_module": "Benchmark.Cases.Polygon.AgglayerBridge.Proofs",
+      "evaluation": {
+        "engine": "lean_proof_generation",
+        "target_kind": "proof_generation"
+      },
+      "readiness": {
+        "prompt_context": "ready",
+        "editable_proof": "ready",
+        "reference_solution": "ready"
+      }
+    },
+    {
+      "task_ref": "polygon/agglayer_bridge/claimMessage_valid_leaf_and_consumes_unique_nullifier",
+      "task_id": "claimMessage_valid_leaf_and_consumes_unique_nullifier",
+      "case_id": "polygon/agglayer_bridge",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/polygon/agglayer_bridge/tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.yaml",
+      "split": "active",
+      "family_id": "polygon",
+      "implementation_id": "agglayer_bridge",
+      "source_ref": "https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol",
+      "task_interface_version": 2,
+      "track": "proof-only",
+      "property_class": "authorization_state",
+      "category": "invariant",
+      "difficulty": "medium",
+      "theorem_name": "Benchmark.Cases.Polygon.AgglayerBridge.claimMessage_valid_leaf_and_consumes_unique_nullifier",
+      "proof_family": "state_preservation_local_effects",
+      "translation_status": "translated",
+      "proof_status": "complete",
+      "implementation_files": [
+        "cases/polygon/agglayer_bridge/verity/Contract.lean",
+        "Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean"
+      ],
+      "specification_files": [
+        "cases/polygon/agglayer_bridge/verity/Specs.lean",
+        "Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean"
+      ],
+      "editable_files": [
+        "Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.lean"
+      ],
+      "abstraction_level": "protocol_slice",
+      "abstraction_notes": "Message claims are proved to validate the modeled leaf against an accepted global exit root and successfully reach the nullifier helper. A shared helper theorem proves that successful helper execution consumes the bitmap nullifier.",
+      "unsupported_feature_codes": [],
+      "reference_solution_module": "Benchmark.Cases.Polygon.AgglayerBridge.Proofs",
+      "evaluation": {
+        "engine": "lean_proof_generation",
+        "target_kind": "proof_generation"
+      },
+      "readiness": {
+        "prompt_context": "ready",
+        "editable_proof": "ready",
+        "reference_solution": "ready"
+      }
+    },
+    {
+      "task_ref": "reserve/auction_price_band/price_at_end_time",
+      "task_id": "price_at_end_time",
+      "case_id": "reserve/auction_price_band",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/reserve/auction_price_band/tasks/price_at_end_time.yaml",
+      "split": "active",
+      "family_id": "reserve",
+      "implementation_id": "dtfs",
+      "source_ref": "https://github.com/reserve-protocol/dtfs@14f75d18856d587adfaff24e77e5b20dda7c7267:contracts/utils/RebalancingLib.sol",
+      "task_interface_version": 2,
+      "track": "proof-only",
+      "property_class": "price_computation",
+      "category": "arithmetic-invariant",
+      "difficulty": "easy",
+      "theorem_name": "Benchmark.Cases.Reserve.AuctionPriceBand.price_at_end_time",
+      "proof_family": "functional_correctness",
+      "translation_status": "translated",
+      "proof_status": "complete",
+      "implementation_files": [
+        "cases/reserve/auction_price_band/verity/Contract.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean"
+      ],
+      "specification_files": [
+        "cases/reserve/auction_price_band/verity/Specs.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean"
+      ],
+      "editable_files": [
+        "Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceAtEndTime.lean"
+      ],
+      "abstraction_level": "protocol_slice",
+      "abstraction_notes": "Boundary exactness at endTime: when the auction has reached its end timestamp and the auction is not atomic-swap, `_price` returns the launcher-published endPrice.",
+      "unsupported_feature_codes": [],
+      "reference_solution_module": "Benchmark.Cases.Reserve.AuctionPriceBand.Proofs",
+      "evaluation": {
+        "engine": "lean_proof_generation",
+        "target_kind": "proof_generation"
+      },
+      "readiness": {
+        "prompt_context": "ready",
+        "editable_proof": "ready",
+        "reference_solution": "ready"
+      }
+    },
+    {
+      "task_ref": "reserve/auction_price_band/price_at_start_time",
+      "task_id": "price_at_start_time",
+      "case_id": "reserve/auction_price_band",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/reserve/auction_price_band/tasks/price_at_start_time.yaml",
+      "split": "active",
+      "family_id": "reserve",
+      "implementation_id": "dtfs",
+      "source_ref": "https://github.com/reserve-protocol/dtfs@14f75d18856d587adfaff24e77e5b20dda7c7267:contracts/utils/RebalancingLib.sol",
+      "task_interface_version": 2,
+      "track": "proof-only",
+      "property_class": "price_computation",
+      "category": "arithmetic-invariant",
+      "difficulty": "easy",
+      "theorem_name": "Benchmark.Cases.Reserve.AuctionPriceBand.price_at_start_time",
+      "proof_family": "functional_correctness",
+      "translation_status": "translated",
+      "proof_status": "complete",
+      "implementation_files": [
+        "cases/reserve/auction_price_band/verity/Contract.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean"
+      ],
+      "specification_files": [
+        "cases/reserve/auction_price_band/verity/Specs.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean"
+      ],
+      "editable_files": [
+        "Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceAtStartTime.lean"
+      ],
+      "abstraction_level": "protocol_slice",
+      "abstraction_notes": "Boundary exactness at startTime: `_price` returns the launcher-published startPrice when the auction has just opened.",
+      "unsupported_feature_codes": [],
+      "reference_solution_module": "Benchmark.Cases.Reserve.AuctionPriceBand.Proofs",
+      "evaluation": {
+        "engine": "lean_proof_generation",
+        "target_kind": "proof_generation"
+      },
+      "readiness": {
+        "prompt_context": "ready",
+        "editable_proof": "ready",
+        "reference_solution": "ready"
+      }
+    },
+    {
+      "task_ref": "reserve/auction_price_band/price_lower_bound",
+      "task_id": "price_lower_bound",
+      "case_id": "reserve/auction_price_band",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/reserve/auction_price_band/tasks/price_lower_bound.yaml",
+      "split": "active",
+      "family_id": "reserve",
+      "implementation_id": "dtfs",
+      "source_ref": "https://github.com/reserve-protocol/dtfs@14f75d18856d587adfaff24e77e5b20dda7c7267:contracts/utils/RebalancingLib.sol",
+      "task_interface_version": 2,
+      "track": "proof-only",
+      "property_class": "price_band",
+      "category": "arithmetic-invariant",
+      "difficulty": "medium",
+      "theorem_name": "Benchmark.Cases.Reserve.AuctionPriceBand.price_lower_bound",
+      "proof_family": "functional_correctness",
+      "translation_status": "translated",
+      "proof_status": "complete",
+      "implementation_files": [
+        "cases/reserve/auction_price_band/verity/Contract.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean"
+      ],
+      "specification_files": [
+        "cases/reserve/auction_price_band/verity/Specs.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean"
+      ],
+      "editable_files": [
+        "Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceLowerBound.lean"
+      ],
+      "abstraction_level": "protocol_slice",
+      "abstraction_notes": "Lower band: `endPrice \u2264 price` for any timestamp. The interior branch is closed by the explicit `if (p < endPrice) p = endPrice` clamp; the boundary branches are closed via the `hBand` precondition.",
+      "unsupported_feature_codes": [],
+      "reference_solution_module": "Benchmark.Cases.Reserve.AuctionPriceBand.Proofs",
+      "evaluation": {
+        "engine": "lean_proof_generation",
+        "target_kind": "proof_generation"
+      },
+      "readiness": {
+        "prompt_context": "ready",
+        "editable_proof": "ready",
+        "reference_solution": "ready"
+      }
+    },
+    {
+      "task_ref": "reserve/auction_price_band/price_upper_bound",
+      "task_id": "price_upper_bound",
+      "case_id": "reserve/auction_price_band",
+      "suite": "active",
+      "schema_version": 1,
+      "manifest_path": "cases/reserve/auction_price_band/tasks/price_upper_bound.yaml",
+      "split": "active",
+      "family_id": "reserve",
+      "implementation_id": "dtfs",
+      "source_ref": "https://github.com/reserve-protocol/dtfs@14f75d18856d587adfaff24e77e5b20dda7c7267:contracts/utils/RebalancingLib.sol",
+      "task_interface_version": 2,
+      "track": "proof-only",
+      "property_class": "price_band",
+      "category": "arithmetic-invariant",
+      "difficulty": "hard",
+      "theorem_name": "Benchmark.Cases.Reserve.AuctionPriceBand.price_upper_bound",
+      "proof_family": "functional_correctness",
+      "translation_status": "translated",
+      "proof_status": "complete",
+      "implementation_files": [
+        "cases/reserve/auction_price_band/verity/Contract.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Contract.lean"
+      ],
+      "specification_files": [
+        "cases/reserve/auction_price_band/verity/Specs.lean",
+        "Benchmark/Cases/Reserve/AuctionPriceBand/Specs.lean"
+      ],
+      "editable_files": [
+        "Benchmark/Generated/Reserve/AuctionPriceBand/Tasks/PriceUpperBound.lean"
+      ],
+      "abstraction_level": "protocol_slice",
+      "abstraction_notes": "Upper band: `price \u2264 startPrice` for any timestamp. Discharged via the axiom `MathLib_exp_nonpositive_le_D18` (declared in Contract.lean) plus the `mulDivUp_le_self_of_le` ceil-division lemma proven inline in Proofs.lean.",
+      "unsupported_feature_codes": [],
+      "reference_solution_module": "Benchmark.Cases.Reserve.AuctionPriceBand.Proofs",
+      "evaluation": {
+        "engine": "lean_proof_generation",
+        "target_kind": "proof_generation"
+      },
+      "readiness": {
+        "prompt_context": "ready",
+        "editable_proof": "ready",
+        "reference_solution": "ready"
+      }
+    },
     {
       "task_ref": "safe/owner_manager_reach/add_owner_acyclicity",
       "task_id": "add_owner_acyclicity",
@@ -5521,5 +5948,5 @@
       }
     }
   ],
-  "generated_at": "2026-04-28T17:34:17.541206+00:00"
+  "generated_at": "2026-05-06T15:45:48.600078+00:00"
 }
diff --git a/cases/polygon/agglayer_bridge/case.yaml b/cases/polygon/agglayer_bridge/case.yaml
new file mode 100644
index 00000000..70301eba
--- /dev/null
+++ b/cases/polygon/agglayer_bridge/case.yaml
@@ -0,0 +1,50 @@
+manifest_kind: case
+project: polygon
+case_id: agglayer_bridge
+schema_version: 1
+split: active
+family_id: polygon
+implementation_id: agglayer_bridge
+stage: proof_complete
+translation_status: translated
+spec_status: frozen
+proof_status: complete
+upstream_repo: https://github.com/agglayer/agglayer-contracts
+upstream_commit: 110bda5a03e70ee7331bc06407a8e79226d3e520
+original_contract_path: contracts/AgglayerBridge.sol
+source_ref: https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol
+lean_target: Benchmark.Cases.Polygon.AgglayerBridge.Compile
+spec_target: Benchmark.Cases.Polygon.AgglayerBridge.Specs
+proof_target: Benchmark.Cases.Polygon.AgglayerBridge.Proofs
+selected_functions:
+  - claimAsset
+  - claimMessage
+  - _verifyLeafAndSetNullifier
+  - _verifyLeaf
+  - _setAndCheckClaimed
+  - isClaimed
+  - _validateAndDecodeGlobalIndex
+  - _bitmapPositions
+  - _addLeafBridge
+  - _updateGlobalExitRoot
+source_language: solidity
+verity_version: 4ebe4931d25e5a1594fcd3f43ff040ecc3c4225a
+lean_toolchain: leanprover/lean4:v4.22.0
+abstraction_level: protocol_slice
+abstraction_tags:
+  - merkle_proof_summary
+  - nullifier_bitmap
+  - global_exit_root_ghost
+  - metadata_hash_parameter
+  - post_nullifier_effects_elided
+abstraction_notes: >
+  The benchmark models the claim validation and nullifier path of AgglayerBridge.
+  Dynamic metadata bytes are represented by a precomputed metadata hash, Merkle
+  proof calculation is summarized by a deterministic root combiner, and token or
+  message side effects after nullifier consumption are elided.
+unsupported_feature_codes: []
+notes: >
+  The proved property is split into public claim theorems that show successful
+  claims validate the leaf and reach the nullifier helper, plus a helper theorem
+  that proves the nullifier helper consumes the source-network/leaf-index bitmap
+  entry.
diff --git a/cases/polygon/agglayer_bridge/tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.yaml b/cases/polygon/agglayer_bridge/tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.yaml
new file mode 100644
index 00000000..7d666f0f
--- /dev/null
+++ b/cases/polygon/agglayer_bridge/tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.yaml
@@ -0,0 +1,34 @@
+manifest_kind: task
+schema_version: 1
+task_id: claimAsset_valid_leaf_and_consumes_unique_nullifier
+case_id: polygon/agglayer_bridge
+split: active
+family_id: polygon
+implementation_id: agglayer_bridge
+source_ref: https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol
+task_interface_version: 2
+theorem_name: Benchmark.Cases.Polygon.AgglayerBridge.claimAsset_valid_leaf_and_consumes_unique_nullifier
+proof_family: state_preservation_local_effects
+property_class: authorization_state
+difficulty: medium
+category: invariant
+track: proof-only
+translation_status: translated
+proof_status: complete
+evaluation_engine: lean_proof_generation
+implementation_files:
+  - cases/polygon/agglayer_bridge/verity/Contract.lean
+  - Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean
+specification_files:
+  - cases/polygon/agglayer_bridge/verity/Specs.lean
+  - Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean
+editable_files:
+  - Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimAsset_valid_leaf_and_consumes_unique_nullifier.lean
+reference_solution_module: Benchmark.Cases.Polygon.AgglayerBridge.Proofs
+reference_solution_declaration: Benchmark.Cases.Polygon.AgglayerBridge.claimAsset_valid_leaf_and_consumes_unique_nullifier
+abstraction_level: protocol_slice
+abstraction_notes: >
+  Asset claims are proved to validate the modeled leaf against an accepted global
+  exit root and successfully reach the nullifier helper. A shared helper theorem
+  proves that successful helper execution consumes the bitmap nullifier.
+unsupported_feature_codes: []
diff --git a/cases/polygon/agglayer_bridge/tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.yaml b/cases/polygon/agglayer_bridge/tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.yaml
new file mode 100644
index 00000000..40435979
--- /dev/null
+++ b/cases/polygon/agglayer_bridge/tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.yaml
@@ -0,0 +1,34 @@
+manifest_kind: task
+schema_version: 1
+task_id: claimMessage_valid_leaf_and_consumes_unique_nullifier
+case_id: polygon/agglayer_bridge
+split: active
+family_id: polygon
+implementation_id: agglayer_bridge
+source_ref: https://github.com/agglayer/agglayer-contracts@110bda5a03e70ee7331bc06407a8e79226d3e520:contracts/AgglayerBridge.sol
+task_interface_version: 2
+theorem_name: Benchmark.Cases.Polygon.AgglayerBridge.claimMessage_valid_leaf_and_consumes_unique_nullifier
+proof_family: state_preservation_local_effects
+property_class: authorization_state
+difficulty: medium
+category: invariant
+track: proof-only
+translation_status: translated
+proof_status: complete
+evaluation_engine: lean_proof_generation
+implementation_files:
+  - cases/polygon/agglayer_bridge/verity/Contract.lean
+  - Benchmark/Cases/Polygon/AgglayerBridge/Contract.lean
+specification_files:
+  - cases/polygon/agglayer_bridge/verity/Specs.lean
+  - Benchmark/Cases/Polygon/AgglayerBridge/Specs.lean
+editable_files:
+  - Benchmark/Generated/Polygon/AgglayerBridge/Tasks/claimMessage_valid_leaf_and_consumes_unique_nullifier.lean
+reference_solution_module: Benchmark.Cases.Polygon.AgglayerBridge.Proofs
+reference_solution_declaration: Benchmark.Cases.Polygon.AgglayerBridge.claimMessage_valid_leaf_and_consumes_unique_nullifier
+abstraction_level: protocol_slice
+abstraction_notes: >
+  Message claims are proved to validate the modeled leaf against an accepted
+  global exit root and successfully reach the nullifier helper. A shared helper
+  theorem proves that successful helper execution consumes the bitmap nullifier.
+unsupported_feature_codes: []
diff --git a/cases/polygon/agglayer_bridge/verity/Compile.lean b/cases/polygon/agglayer_bridge/verity/Compile.lean
new file mode 100644
index 00000000..1b900e93
--- /dev/null
+++ b/cases/polygon/agglayer_bridge/verity/Compile.lean
@@ -0,0 +1 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Compile
diff --git a/cases/polygon/agglayer_bridge/verity/Contract.lean b/cases/polygon/agglayer_bridge/verity/Contract.lean
new file mode 100644
index 00000000..ea2e84ba
--- /dev/null
+++ b/cases/polygon/agglayer_bridge/verity/Contract.lean
@@ -0,0 +1 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Contract
diff --git a/cases/polygon/agglayer_bridge/verity/Specs.lean b/cases/polygon/agglayer_bridge/verity/Specs.lean
new file mode 100644
index 00000000..92672ea2
--- /dev/null
+++ b/cases/polygon/agglayer_bridge/verity/Specs.lean
@@ -0,0 +1 @@
+import Benchmark.Cases.Polygon.AgglayerBridge.Specs
diff --git a/families/polygon/family.yaml b/families/polygon/family.yaml
new file mode 100644
index 00000000..f47b22c7
--- /dev/null
+++ b/families/polygon/family.yaml
@@ -0,0 +1,14 @@
+manifest_kind: family
+schema_version: 1
+family_id: polygon
+display_name: Polygon / Agglayer
+split: active
+status: active
+description: >
+  Polygon Agglayer bridge and interoperability verification cases.
+implementation_ids:
+  - agglayer_bridge
+case_ids:
+  - polygon/agglayer_bridge
+source_languages:
+  - solidity
diff --git a/families/polygon/implementations/agglayer_bridge/implementation.yaml b/families/polygon/implementations/agglayer_bridge/implementation.yaml
new file mode 100644
index 00000000..21c58565
--- /dev/null
+++ b/families/polygon/implementations/agglayer_bridge/implementation.yaml
@@ -0,0 +1,16 @@
+manifest_kind: implementation
+schema_version: 1
+family_id: polygon
+implementation_id: agglayer_bridge
+display_name: Polygon AgglayerBridge
+split: active
+status: translated
+upstream_repo: https://github.com/agglayer/agglayer-contracts
+upstream_commit: 110bda5a03e70ee7331bc06407a8e79226d3e520
+source_language: solidity
+source_artifact_path: contracts/AgglayerBridge.sol
+case_ids:
+  - polygon/agglayer_bridge
+notes: >
+  Verity model of the AgglayerBridge claim path, focused on valid exit-root
+  membership and source-network/leaf-index nullifier consumption.