From 59cd35d57142d1d7075751067341349caa19dcfd Mon Sep 17 00:00:00 2001 From: Fricoben Date: Wed, 22 Apr 2026 09:05:31 +0100 Subject: [PATCH 1/5] feat: add midas research case study --- components/research/MidasGuarantee.jsx | 103 ++++++ data/research.js | 10 + pages/research/midas-feed-growth-safety.jsx | 383 ++++++++++++++++++++ 3 files changed, 496 insertions(+) create mode 100644 components/research/MidasGuarantee.jsx create mode 100644 pages/research/midas-feed-growth-safety.jsx diff --git a/components/research/MidasGuarantee.jsx b/components/research/MidasGuarantee.jsx new file mode 100644 index 0000000..77a984f --- /dev/null +++ b/components/research/MidasGuarantee.jsx @@ -0,0 +1,103 @@ +import { useEffect, useRef, useState } from 'react' +import { ExternalLinkIcon } from './ExternalLink' + +const FORMAL_GUARANTEES = [ + "history && maxDev < 100% -> safe(0, t, apr) reverts", + 'success && history -> abs(deviation(lastLive, newLive)) <= maxDev', + 'success -> now - lastUpdated > 1 hour', + "success -> startedAt' > startedAt", + 'success && onlyUp -> signedDeviation >= 0', + "success -> answer' and apr' stay within bands" +] + +export default function MidasGuarantee({ specsHref }) { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ {FORMAL_GUARANTEES.map((formal, i) => ( + + {formal} + + ))} +
+
+

+ Once the feed has history, the safe submission path rejects zero + live prices below a 100% deviation cap, and every accepted round + satisfies the contract's deviation, timing, monotonicity, and + band guards. +

+
+
+ +
+ + View Lean + + +
+
+ ) +} diff --git a/data/research.js b/data/research.js index 60012f2..07d639e 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'midas-feed-growth-safety', + title: 'Midas Growth-Aware Feed Safety Guarantees', + subtitle: + 'Formally verified safety properties of the safe submission path in Midas\'s growth-aware price feed.', + description: + 'How we proved zero-price rejection and accepted-write safety guarantees for Midas\'s CustomAggregatorV3CompatibleFeedGrowth safe path using Verity and Lean 4.', + date: '2026-04-21', + tag: 'Case study' + }, { slug: 'zama-erc7984-confidential-token', title: 'ERC-7984 Confidential Token Invariants', diff --git a/pages/research/midas-feed-growth-safety.jsx b/pages/research/midas-feed-growth-safety.jsx new file mode 100644 index 0000000..44b402d --- /dev/null +++ b/pages/research/midas-feed-growth-safety.jsx @@ -0,0 +1,383 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import Disclosure from '../../components/research/Disclosure' +import ExternalLink from '../../components/research/ExternalLink' +import Hypothesis from '../../components/research/Hypothesis' +import MidasGuarantee from '../../components/research/MidasGuarantee' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const UPSTREAM_CONTRACT = + 'https://github.com/midas-apps/contracts/blob/main/contracts/feeds/CustomAggregatorV3CompatibleFeedGrowth.sol' + +const BENCHMARK_PULL_REQUEST = + 'https://github.com/lfglabs-dev/verity-benchmark/pull/25' + +const BENCHMARK_REPO = + 'https://github.com/lfglabs-dev/verity-benchmark' + +const BENCHMARK_COMMIT = + 'https://github.com/lfglabs-dev/verity-benchmark/blob/5ee8e4dd4e29ea9c3181ac6358d516f954b62d89' + +const SPECS_LINK = `${BENCHMARK_COMMIT}/Benchmark/Cases/Midas/CustomFeedGrowthSafe/Specs.lean` +const PROOFS_LINK = `${BENCHMARK_COMMIT}/Benchmark/Cases/Midas/CustomFeedGrowthSafe/Proofs.lean` + +export default function MidasFeedGrowthSafetyPage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'midas-feed-growth-safety' + ) + + return ( + <> + + + Midas Growth-Aware Feed Safety Guarantees | Research | LFG Labs + + + + +
+ + +
+

+ 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 and does not prevent. In particular, it highlights that the + guardrails on deviation, timing, monotonic timestamps, and + non-decreasing updates in{' '} + onlyUp mode really + do hold on the safe path, including the rejection of zero-price + submissions below a 100% deviation cap. +

+
+ +
+

+ What this covers +

+

+ 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. +

+ +

+ The guarantees are split into two categories and should be read + differently. +

+
    +
  • + Rejection guarantee: once the feed has prior + history, a zero-price submission through the safe path is + rejected whenever{' '} + + 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. +
    • +
  • + Successful-write guarantees: for executions + that satisfy the contract's own guards and complete the + safe path, the verified model shows that the candidate live + price is within the configured deviation bound, more than one + hour has passed since the previous update, the new round's{' '} + 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. +

+ +
+ +
+

+ 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 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. +

+

+ Intentionally out of scope: access control plumbing, events, + unrelated read-only interface methods, and downstream protocol + integrations outside this contract. +

+
+ +
+

+ Proof status +

+

+ The six guarantee families for this case are machine-checked in + Lean 4. The proof file in{' '} + PR #25{' '} + is 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 +
+
+

+ View specs in Lean + View proofs in Lean +

+
+ +
+

+ Assumptions +

+

+ The proofs use zero axioms. The operative assumptions are the + contract's own guards and a clear scope restriction about + which entrypoint is being analyzed. +

+
    + + The zero-price rejection and deviation-direction claims are + about calls that actually compare against a previous live price. + If there is no prior round history,{' '} + setRoundDataSafe{' '} + skips the deviation comparison entirely. + + + The zero-price rejection claim depends on the configured cap + being strictly below 100% in the contract's 8-decimal + percentage units. At exactly 100%, a zero-price candidate is no + longer excluded by that guard alone. + + + The positive guarantees apply to executions that satisfy the + contract's own conditions: timestamps are ordered + correctly, more than one hour has elapsed since the previous + update, the new{' '} + startedAt{' '} + advances, the raw answer and APR fall inside configured bands, + and when history exists the candidate live price passes the + deviation check. + + + When{' '} + onlyUp{' '} + is enabled, the safe path assumes the contract's own + additional conditions hold: the submitted APR is non-negative, + and the signed deviation against the previous live price is not + negative. + +
+
+ +
+

+ Scope limitation +

+

+ This case study is deliberately about the safe submission path. It + does not claim that the same guarantees hold for callers who + bypass{' '} + setRoundDataSafe{' '} + and invoke{' '} + setRoundData{' '} + directly, because that path omits the safe wrapper's + deviation and timing checks. +

+

+ It also does not verify admin authorization, emitted events, or + the behavior of protocols that consume this feed downstream. +

+
+ +
+

+ Learn more +

+

+ + Upstream Solidity contract + + {', the production source modeled in this case.'} +

+

+ + Benchmark pull request + + {', which adds the formal specification and machine-checked proofs.'} +

+

+ + Verity benchmark repository + + {', the broader benchmark suite this case belongs to.'} +

+

+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +

+
+ + {otherResearch.length > 0 && ( +
+

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +} From 872bac322a37f982ddd209f39c1907920a151983 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Wed, 22 Apr 2026 09:30:59 +0100 Subject: [PATCH 2/5] fix: simplify midas guarantee copy --- components/research/MidasGuarantee.jsx | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/components/research/MidasGuarantee.jsx b/components/research/MidasGuarantee.jsx index 77a984f..63a9bde 100644 --- a/components/research/MidasGuarantee.jsx +++ b/components/research/MidasGuarantee.jsx @@ -2,12 +2,8 @@ import { useEffect, useRef, useState } from 'react' import { ExternalLinkIcon } from './ExternalLink' const FORMAL_GUARANTEES = [ - "history && maxDev < 100% -> safe(0, t, apr) reverts", - 'success && history -> abs(deviation(lastLive, newLive)) <= maxDev', - 'success -> now - lastUpdated > 1 hour', - "success -> startedAt' > startedAt", - 'success && onlyUp -> signedDeviation >= 0', - "success -> answer' and apr' stay within bands" + 'violatesBounds -> revert', + 'success -> boundsHold' ] export default function MidasGuarantee({ specsHref }) { @@ -79,10 +75,8 @@ export default function MidasGuarantee({ specsHref }) { aria-hidden={!showEnglish} >

- Once the feed has history, the safe submission path rejects zero - live prices below a 100% deviation cap, and every accepted round - satisfies the contract's deviation, timing, monotonicity, and - band guards. + The safe path rejects operator submissions that violate the + feed's configured bounds.

From 9de708a69b9ffce7919446418c1913fd18fbce4f Mon Sep 17 00:00:00 2001 From: Fricoben Date: Wed, 22 Apr 2026 09:53:54 +0100 Subject: [PATCH 3/5] fix: remove pr references --- pages/research/midas-feed-growth-safety.jsx | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/pages/research/midas-feed-growth-safety.jsx b/pages/research/midas-feed-growth-safety.jsx index 44b402d..819c0b8 100644 --- a/pages/research/midas-feed-growth-safety.jsx +++ b/pages/research/midas-feed-growth-safety.jsx @@ -11,9 +11,6 @@ import { getSortedResearch } from '../../lib/getSortedResearch' const UPSTREAM_CONTRACT = 'https://github.com/midas-apps/contracts/blob/main/contracts/feeds/CustomAggregatorV3CompatibleFeedGrowth.sol' -const BENCHMARK_PULL_REQUEST = - 'https://github.com/lfglabs-dev/verity-benchmark/pull/25' - const BENCHMARK_REPO = 'https://github.com/lfglabs-dev/verity-benchmark' @@ -186,11 +183,13 @@ export default function MidasFeedGrowthSafetyPage() {

The six guarantee families for this case are machine-checked in - Lean 4. The proof file in{' '} - PR #25{' '} + Lean 4. The corresponding proof file in the{' '} + + Verity benchmark repository + {' '} is sorry-free, so - the claims below are accepted by Lean's kernel rather than by - informal review. + the claims below are accepted by Lean's kernel rather than + by informal review.

@@ -341,17 +340,11 @@ export default function MidasFeedGrowthSafetyPage() { {', the production source modeled in this case.'}

-

- - Benchmark pull request - - {', which adds the formal specification and machine-checked proofs.'} -

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

Date: Wed, 22 Apr 2026 10:03:22 +0100 Subject: [PATCH 4/5] fix: simplify midas assumptions --- pages/research/midas-feed-growth-safety.jsx | 63 +++------------------ 1 file changed, 9 insertions(+), 54 deletions(-) diff --git a/pages/research/midas-feed-growth-safety.jsx b/pages/research/midas-feed-growth-safety.jsx index 819c0b8..ca9b715 100644 --- a/pages/research/midas-feed-growth-safety.jsx +++ b/pages/research/midas-feed-growth-safety.jsx @@ -4,7 +4,6 @@ import PageLayout from '../../components/PageLayout' import ResearchCard from '../../components/ResearchCard' import Disclosure from '../../components/research/Disclosure' import ExternalLink from '../../components/research/ExternalLink' -import Hypothesis from '../../components/research/Hypothesis' import MidasGuarantee from '../../components/research/MidasGuarantee' import { getSortedResearch } from '../../lib/getSortedResearch' @@ -254,60 +253,16 @@ export default function MidasFeedGrowthSafetyPage() { Assumptions

- The proofs use zero axioms. The operative assumptions are the - contract's own guards and a clear scope restriction about - which entrypoint is being analyzed. + The proofs use zero axioms. The main conditional claim here is + the zero-price rejection result: it applies when the feed already + has a previous round to compare against and{' '} + + maxAnswerDeviation + {' '} + is set below 100% in the contract's fixed-point units. At + exactly 100%, that specific rejection claim no longer follows from + the deviation check alone.

-
    - - The zero-price rejection and deviation-direction claims are - about calls that actually compare against a previous live price. - If there is no prior round history,{' '} - setRoundDataSafe{' '} - skips the deviation comparison entirely. - - - The zero-price rejection claim depends on the configured cap - being strictly below 100% in the contract's 8-decimal - percentage units. At exactly 100%, a zero-price candidate is no - longer excluded by that guard alone. - - - The positive guarantees apply to executions that satisfy the - contract's own conditions: timestamps are ordered - correctly, more than one hour has elapsed since the previous - update, the new{' '} - startedAt{' '} - advances, the raw answer and APR fall inside configured bands, - and when history exists the candidate live price passes the - deviation check. - - - When{' '} - onlyUp{' '} - is enabled, the safe path assumes the contract's own - additional conditions hold: the submitted APR is non-negative, - and the signed deviation against the previous live price is not - negative. - -
From 67dd1d0e35d52a4e91874abd41cb0bfdd05261c2 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Wed, 22 Apr 2026 10:20:19 +0100 Subject: [PATCH 5/5] fix: align midas article structure --- components/research/MidasGuarantee.jsx | 11 +- pages/research/midas-feed-growth-safety.jsx | 128 ++++++++++++-------- 2 files changed, 87 insertions(+), 52 deletions(-) diff --git a/components/research/MidasGuarantee.jsx b/components/research/MidasGuarantee.jsx index 63a9bde..96979dc 100644 --- a/components/research/MidasGuarantee.jsx +++ b/components/research/MidasGuarantee.jsx @@ -2,8 +2,10 @@ import { useEffect, useRef, useState } from 'react' import { ExternalLinkIcon } from './ExternalLink' const FORMAL_GUARANTEES = [ - 'violatesBounds -> revert', - 'success -> boundsHold' + '∀ s ts apr now, history(s) ∧ maxDev(s) < 100% → ¬success(safe(0, ts, apr, now, s))', + '∀ s x ts apr now, success(safe(x, ts, apr, now, s)) → dev(lastLive(s, now), newLive(x, ts, apr, now)) ≤ maxDev(s)', + "∀ s x ts apr now s′, success(safe(x, ts, apr, now, s)) → startedAt′ > startedAt(s) ∧ inBands(answer′, apr′)", + '∀ s x ts apr now, success(safe(x, ts, apr, now, s)) ∧ onlyUp(s) → signedDev ≥ 0' ] export default function MidasGuarantee({ specsHref }) { @@ -81,6 +83,11 @@ export default function MidasGuarantee({ specsHref }) { +

+ In the formal view, each statement ranges over all submission values + and states satisfying the assumptions listed below. +

+

- What this covers + Why this matters

- 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. + 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.

- +

- The guarantees are split into two categories and should be read - differently. + 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.

  • @@ -134,12 +147,21 @@ export default function MidasFeedGrowthSafetyPage() { 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. +

@@ -169,11 +191,15 @@ export default function MidasFeedGrowthSafetyPage() { is included as well, along with the underlying band checks from{' '} setRoundData.

-

- Intentionally out of scope: access control plumbing, events, - unrelated read-only interface methods, and downstream protocol - integrations outside this contract. -

+ + {VERIFY_COMMAND} +

+ If the build succeeds, the proofs are correct.{' '} + + Source repository + +

+
@@ -253,35 +279,37 @@ export default function MidasFeedGrowthSafetyPage() { Assumptions

- The proofs use zero axioms. The main conditional claim here is - the zero-price rejection result: it applies when the feed already - has a previous round to compare against and{' '} - - maxAnswerDeviation - {' '} - is set below 100% in the contract's fixed-point units. At - exactly 100%, that specific rejection claim no longer follows from - the deviation check alone. + The proofs use zero axioms. Two hypotheses matter for the + zero-price rejection theorem.

-
- -
-

- Scope limitation -

-

- This case study is deliberately about the safe submission path. It - does not claim that the same guarantees hold for callers who - bypass{' '} - setRoundDataSafe{' '} - and invoke{' '} - setRoundData{' '} - directly, because that path omits the safe wrapper's - deviation and timing checks. -

-

- It also does not verify admin authorization, emitted events, or - the behavior of protocols that consume this feed downstream. +

    + + The zero-price rejection claim 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. + + + The contract allows a maximum deviation up to and including + 100%. The zero-price rejection theorem 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 Lean + View proofs in Lean