An Active Aera Request Cannot Be Consumed Twice

\;\coloneqq\;

\land\;

\land\;

\land\;

\land\;(

\;\Rightarrow

\land\;

)

An active Aera request cannot be consumed twice.

View Lean

Aera Finance V3 accepts asynchronous deposit and redemption requests through ProvisionerV2. Each request stays active until it is solved, refunded, or cancelled. We modeled that terminal lifecycle and proved that one activation can produce at most one terminal outcome.

Why It Matters

A terminal route releases or redirects the assets associated with a request. If the same active request could be consumed again, another route could attempt a second release from the same request.

In the scoped model, every successful terminal route clears the request's active marker. Immediate attempts to solve, refund, or cancel that activation again are rejected or ignored before a second terminal outcome can occur.

How This Was Modeled and Proven

We recreated the relevant terminal control flow from ProvisionerV2.sol at commit f0ebc159…. The model tracks the active request marker, its deposit or redemption kind, its committed amount, and the aggregate custody channel used by that request.

One specification combines every modeled terminal route. Six proof lemmas cover live vault solve, live fixed-price direct solve, explicit refund, cancellation, and the refund branches reached when vault or fixed-price direct solve is attempted after expiry. The public theorem combines them into one invariant.

Public artifacts: Contract.lean, Specs.lean, and Proofs.lean.

Function	Theorem	Status
At-most-once consumption	active_request_cannot_be_consumed_twice	proven

At-most-once consumption: active_request_cannot_be_consumed_twice; proven

Scope

The theorem applies to one active request lifecycle. A caller may create the same request again after termination if the source permits it. The proof does not claim lifetime uniqueness for a reusable request hash.
Request hashes are represented by collision-free keys. The proof does not establish Keccak collision resistance.
Aggregate deposit-token and vault-unit custody are modeled. External token storage, callbacks, and vault correctness are outside this state slice.
Authorization, deadlines, policy predicates, and external-call success are explicit control-flow inputs. Reverting attempts do not count as terminal outcomes.
This is a hand-authored model of pinned source control flow. It is not a source-to-model refinement or bytecode-equivalence proof.

Proof artifacts

Model, specification, and proof.

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout ae0f22d1786c4bb62e2ca9d80d064fe4d26011c3
lake build Benchmark.Cases.AeraFinance.ProvisionerV2AsyncSettlement.Compile

A successful build means Lean checked the model, specification, route lemmas, and public theorem. The reference files contain no sorry and introduce no project-defined axioms. Repository

Hypotheses

These conditions bound the scoped model and its application to the pinned source.

active requestactive(key) = 1 and aggregate custody covers its amount
theorem premise
The proof begins from a valid active deposit or redemption request whose modeled custody channel covers its committed amount.
fixed-price direct routefixedPrice(key) = 1
source-enforced runtime precondition
Direct settlement and its expired refund branch apply only to requests committed as fixed price. Other terminal routes do not need this condition.
external boundaryexplicit policy and interaction outcomes
model boundary
The proof checks ProvisionerV2 control flow around external outcomes. It does not prove token, vault, oracle, or policy computations performed outside the modeled slice.

Learn More

Read the pinned ProvisionerV2 source or inspect the Lean proof.

More case studies

Gearbox BytecodeRepository Version Index

Lean proofs for exact fresh-insertion updates to Gearbox bytecode and version indexes.

for

Doppler Multicurve Fee Conservation

Eighteen Lean theorems preserve manager-credit backing and the carry, beneficiary-credit, or liquidity-input partition under the modeled transition premises.

for

Velora BridgeStaking Allocation Safety

In the Lean accounting model, under stated token and external-call hypotheses, allocated Velora VLR and WETH never exceed their modeled BridgeStaking balances.

for

Invariant