+ {formal}
+
+ ))}
+ + The safe path rejects operator submissions that violate the + feed's configured bounds. +
++ In the formal view, each statement ranges over all submission values + and states satisfying the assumptions listed below. +
+ +
+ Midas'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 and does not prevent. In particular, it highlights that the
+ safe path really does enforce the configured rejection criteria,
+ including the zero-price case under a strict enough deviation
+ setting.
+
+ 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. +
+
+ This case study is about{' '}
+ setRoundDataSafe
+ , the guarded submission path. It also models the underlying
+ write behavior of{' '}
+ setRoundData,
+ because a successful safe call ends by writing a new round
+ through that path.
+
+ maxAnswerDeviation
+ {' '}
+ is set below 100% in the contract's fixed-point units.
+ The contract uses 8 decimals for percentages, so 100% is{' '}
+ 100 * 1e8. Any
+ smaller cap rules out a candidate live price of zero.
+ startedAt{' '}
+ strictly increases,{' '}
+ onlyUp{' '}
+ excludes negative deviation, and the stored answer and growth
+ APR remain inside the configured min/max bands.
+ + The comparison is growth-aware on both sides. The previous round + is first turned into a live price at the current block time, and + the incoming submission is also projected forward to the current + block time before deviation is measured. +
+
+ Out of scope: direct calls that bypass{' '}
+ setRoundDataSafe{' '}
+ and invoke{' '}
+ setRoundData{' '}
+ directly, access control plumbing, events, unrelated read-only
+ interface methods, and downstream protocol integrations outside
+ this contract.
+
+ 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 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.
+
+ If the build succeeds, the proofs are correct.{' '}
+
+ The six guarantee families for this case are machine-checked in
+ Lean 4. The corresponding proof file in the{' '}
+ sorry-free, so
+ the claims below are accepted by Lean's kernel rather than
+ by informal review.
+
| + Guarantee + | ++ Status + | +
|---|---|
| Rejects zero price below 100% cap | ++ proven + | +
| Deviation bound on accepted write | ++ proven + | +
| More than one hour since last update | ++ proven + | +
| startedAt strictly increases | ++ proven + | +
| onlyUp forbids negative deviation | ++ proven + | +
| Stored answer and APR stay in bands | ++ proven + | +
+
+ The proofs use zero axioms. Two hypotheses matter for the + zero-price rejection theorem. +
+setRoundDataSafe{' '}
+ skips the deviation check entirely.
+
+
+
+
+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +
+