Midas Growth-Aware Feed Safety Guarantees

Midas's CustomAggregatorV3CompatibleFeedGrowth is an onchain price feed that stores a raw answer, a start timestamp, and a growth APR for each round. In other words, the contract does not treat the stored answer as the final price forever. Starting from the round's startedAt, it updates that answer over time using the configured APR. This lets the feed track assets whose price is expected to increase between submissions, instead of staying flat until the next manual update.

That makes the safe submission path economically important. When a new round is submitted, the contract compares the new growth-adjusted price at the current block time against the previous growth-adjusted price at the current block time. It does not just compare the two stored round values as if no time had passed.

In the shape of this contract, most of the risk is operator risk: an authorized updater submits the next round by hand. Formal verification helps here by showing exactly what the safe wrapper setRoundDataSafe does on both sides of the guard. In particular, the benchmark now exposes human-readable theorems saying that guardrail-safe submissions are accepted and written exactly as submitted, while submissions outside those guardrails are rejected.

Why this matters

This is a manually updated price feed. That means the main operational risk is not an adversary exploiting arithmetic from nowhere, but an authorized operator submitting a round that should have been rejected by the feed's own configured rules.

If the safe path accepted a submission outside those rules, every downstream integration reading the feed would inherit a price the contract itself was supposed to screen out. The point of this case study is to make those guardrails explicit and machine-check that they hold on the guarded entrypoint.

How this was modeled

The benchmark isolates the contract slice that determines whether a safe submission is accepted and what gets written if it is. That includes the current configuration fields, the storage for the latest round, and the next-round write path that records the new answer, timestamps, APR, and round id.

The updated spec layer also introduces human-readable helpers such as safeAccepted, safeRejected, safeInputsOk, and writesSubmittedRound. Those names let the top-level theorem talk about the user-facing behavior of the safe setter instead of only exposing lower-level arithmetic lemmas.

The model also captures the growth arithmetic used to reconstruct the previous live price and the candidate live price of the new submission. This matters because the safety check is about the economically meaningful price at the current moment, not just the raw number stored in storage.

Deviation is modeled with the contract's special zero-price branch, where a candidate live price of zero is treated as a full 100% move. The negative-deviation branch used by onlyUp is included as well, along with the underlying band checks from setRoundData.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
git checkout 07564a24d6a85eefc0479af3a547381bb7a40a68
lake build Benchmark.Cases.Midas.CustomFeedGrowthSafe.Proofs

Proof status

This case is now organized around two human-readable headline specs in Lean 4: one theorem for accepted submissions and one theorem for rejected submissions. The corresponding proof file in the Verity benchmark repository is sorry-free, so the proved claims below are accepted by Lean's kernel rather than by informal review.

The rejection theorem is proved by contrapositive: any successful safe call is shown to satisfy safeInputsOk, so a call that does not satisfy safeInputsOk must reject. The helper packages the lower-level deviation, timing, monotonicity, onlyUp, and band checks into a single readable condition.

View specs in LeanView proofs in Lean

Assumptions

The proofs use zero axioms. The accept/reject theorems are phrased through the helper safeInputsOk. The two assumptions below matter specifically for the separate zero-price rejection corollary.

• hHistorythe feed already has a previous round

  setRoundDataSafe compares against lastAnswer() only when history exists

  The zero-price rejection corollary is about states where the safe path actually compares the new submission against an existing live price. If there is no prior round, setRoundDataSafe skips the deviation check entirely.

• hStrictDeviationmaxAnswerDeviation < 100 * 1e8

  Fixed-point threshold in the contract's percentage units

  The contract allows a maximum deviation up to and including 100%. The zero-price rejection corollary therefore needs the configured deviation cap to be strictly below 100%. At exactly 100%, that specific rejection claim no longer follows from the deviation check alone.

View specs in LeanView proofs in Lean

Learn more

Upstream Solidity contract, the production source modeled in this case.

Verity benchmark repository, which contains the formal specification, machine-checked proofs, and the broader benchmark suite this case belongs to.

What is a formal proof? A short explanation for non-specialists.