Velora BridgeStaking Allocation Safety
Allocated VLR and WETH never exceed their modeled BridgeStaking balances.
Velora uses the BridgeStaking contract to receive VLR and WETH through Across and combine the two legs into an seVLR staking deposit. While one leg is still pending, the contract records how much of each token is reserved.
We modeled the relevant accounting at Velora's pinned commit bfb5f8093bc6f6db0f0840b83d22e803c2811fcb. The invariant requires the contract's tracked balance for each token to cover every amount allocated to incomplete bridge records.
Why It Matters
Across may deliver VLR and WETH in either order. After the first token arrives, BridgeStaking records it as allocated until the pair can be staked or rescued.
If balances and allocations drift apart, an owner withdrawal could spend tokens reserved for a user. The same mismatch can hide an underfunded pending record during staking or rescue.
The proof checks every modeled bridge callback, rescue, and withdrawal. Successful paths update balances and allocations together. Failed guards, checked-arithmetic errors, and selected transfer failures roll back.
How This Was Modeled and Proven
We modeled three BridgeStaking transitions in Lean: bridge-message handling, pending-fund rescue, and owner withdrawal. The model preserves Solidity's checked arithmetic, zero-address beneficiary sentinel, and validation against the stored record.
The callback proof prepares the record, credits the received token, then settles once both tokens are present. Successful seVLR staking debits equal amounts from balances and allocations. The catch path rescues the stored amounts, while selected transfer failures roll back. External-call internals and reentrant accounting are outside the model.
Three Lean theorems prove the invariant for VLR and WETH across every modeled success and revert branch. The proof contains no case-specific axioms, sorry, or admit.
Scope
Included: VLR and WETH bridge receipt accounting, allocation credits, completion detection, successful seVLR accounting, catch/rescue, public rescue, owner withdrawal, checked arithmetic, and explicit safeTransfer success or failure.
Storage model: Lean uses flattened semantic storage, not exact EVM slot packing. Token-balance slots stand for faithful balanceOf observations at entry and exact modeled debits on successful calls.
External calls: The seVLR deposit outcome uses an explicit success/catch selector. The VLR and WETH safeTransfer calls in catch/rescue and public rescue use per-token outcome selectors, while withdrawal uses its own transfer selector. The two safeApprove calls, including failure, allowance changes, and side effects, are excluded. Because those approvals occur before the caught seVLR call, a caught deposit revert leaves the exact allowances in place while rescue returns the tokens. The model does not link external bytecode, raw return data, token implementations, or the Balancer minimum-BPT condition.
Public boundary: Across caller authentication, pause state, ABI decoding, source-chain metadata, owner or beneficiary authorization, events, and reentrancy are out of scope. The callback accepts only VLR or WETH in the source. The withdrawal theorem covers those two invariant-tracked tokens even though the Solidity owner function accepts an arbitrary token address.
Proof artifacts
- Contract.lean contains the source-shaped transition model.
- Specs.lean defines the conservation invariant and run-bound specifications.
- Proofs.lean contains all three reference proofs.
- Case directory contains the compile target and benchmark wiring. The reviewed change is in pull request 157.
| Function | Theorem | Status |
|---|---|---|
| handleV3AcrossMessage | handleV3AcrossMessage_preserves_allocated | Proven |
| rescuePendingFunds | rescuePendingFunds_preserves_allocated | Proven |
| withdrawUnallocatedTokens | withdrawUnallocatedTokens_preserves_allocated | Proven |
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout cb087481e27d71f261b173c8de26c828f51a90a5 lake build Benchmark.Cases.Velora.BridgeStaking.Proofs
Hypotheses
These hypotheses define the exact boundary between the proved Lean accounting result and deployed-contract behavior.
entry deliveryAcross delivery is already reflected in the selected token balanceBridgeStaking.sol balanceOf check
The modeled entry balance includes the callback's token delivery and faithfully represents the contract's balanceOf observation.
exact successful debita successful token call debits exactly the requested amountModeled safeTransfer and seVLR accounting boundary
Fee-on-transfer, rebasing, donation, seizure, and unrelated atomic balance changes are excluded from the successful-call model.
explicit external outcomeinputs select deposit and modeled safeTransfer outcomesLean transition parameters
A false modeled safeTransfer result causes the entire modeled transaction to revert under the atomic-execution boundary. The selectors abstract external execution rather than proving callee bytecode. The two safeApprove calls, their failures, allowance effects, and side effects are not represented.
fixed dependency call graphthe configured external dependencies do not call back into tracked accountingBridgeStaking immutables and the configured seVLR call graph
SafeTransferLib is not a reentrancy guard. In the observed deployments, immutable VLR and WETH resolve to the reviewed OpenZeppelin VLR and canonical WETH implementations, while immutable seVLR routes through verified Balancer V2 or V3 contracts. We found no callback route into BridgeStaking with an authorized caller identity. The Lean model does not formalize this nested call graph.
tracked token domainthe theorem ranges over VLR and WETHBridge callback source guard and selected invariant slice
The callback source accepts these two tokens. The generic owner withdrawal remains outside the theorem for unrelated token addresses.