diff --git a/data/research.js b/data/research.js index 07d639e..dad4da2 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,14 @@ export const research = [ + { + slug: 'how-a-formal-audit-works-in-detail', + title: 'How a Formal Audit Works in Detail', + subtitle: + 'The technical path from repo access to machine-checked security guarantees.', + description: + 'The workflow behind an LFG Labs formal audit: specification, threat modeling, Verity modeling, Lean proofs, reports, and proof maintenance.', + date: '2026-04-23', + tag: 'Explainer' + }, { slug: 'midas-feed-growth-safety', title: 'Midas Growth-Aware Feed Safety Guarantees', diff --git a/pages/research/how-a-formal-audit-works-in-detail.jsx b/pages/research/how-a-formal-audit-works-in-detail.jsx new file mode 100644 index 0000000..c876b7d --- /dev/null +++ b/pages/research/how-a-formal-audit-works-in-detail.jsx @@ -0,0 +1,394 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import ExternalLink from '../../components/research/ExternalLink' +import { getSortedResearch } from '../../lib/getSortedResearch' + +const AUDIT_PIPELINE = [ + 'Freeze a baseline commit', + 'Map the architecture and attack surface', + 'Write human-reviewable security specs', + 'Model the contract logic in Verity', + 'Prove the model satisfies the specs', + 'Report bugs and ambiguous behavior as they appear', + 'Re-run proofs after fixes', + 'Publish the final audit report and proof artifacts' +] + +const SPEC_EXAMPLE = `-- Functional guarantee, written before proof work starts. +def no_unbacked_note_created + (before after : ProtocolState) : Prop := + after.totalNotes <= after.totalBackedAssets ∧ + stateTransitionIsAuthorized before after ∧ + nullifiersAreNotReused before after` + +const MODEL_EXAMPLE = `verity_contract ShieldedPool where + storage + roots : Uint256 → Uint256 := slot 0 + nullifiers : Uint256 → Bool := slot 1 + commitments : Uint256 → Bool := slot 2 + + function withdraw + (root nullifier commitment amount : Uint256) : Unit := do + require (rootIsKnown roots root) "unknown root" + requireNot (getMapping nullifiers nullifier) "spent note" + require (verifyWithdrawProof root nullifier commitment amount) + "invalid proof" + setMapping nullifiers nullifier true + transferOut amount` + +const PROOF_TASK = `theorem withdraw_preserves_accounting + (s : ContractState) + (root nullifier commitment amount : Uint256) : + let result := (withdraw root nullifier commitment amount).run s + result.isOk → + no_unbacked_note_created s result.state := by + -- Unfold the Verity model. + -- Use the signed-off spec. + -- Discharge every state-transition case. + -- Lean accepts only if all cases are covered.` + +const CIRCUIT_AXIOM = `-- The circuit verifier is outside the EVM proof. +-- We state exactly what it is assumed to guarantee. +axiom withdraw_circuit_sound + (root nullifier commitment amount : Uint256) : + verifyWithdrawProof root nullifier commitment amount = true → + validWithdrawWitness root nullifier commitment amount` + +const BENCHMARK_INPUTS = [ + 'Fixed contract model', + 'Fixed formal specification', + 'One editable proof file', + 'One theorem name' +] + +const BENCHMARK_EVALUATION = [ + 'Reject placeholders such as sorry, admit, or new axiom', + 'Run Lean against the submitted proof', + 'Accept only if the required theorem compiles' +] + +function Snippet({ children }) { + return ( + 
+      {children}
+
+ ) +} + +function NumberedList({ items }) { + return ( +
    + {items.map((item, index) => ( +
  1. + + {index + 1} + + {item} +
    2. + ))} +
+ ) +} + +function Checklist({ title, items }) { + return ( +
+

+ {title} +

+ +
+ ) +} + +export default function HowAFormalAuditWorksInDetailPage() { + const otherResearch = getSortedResearch().filter( + (r) => r.slug !== 'how-a-formal-audit-works-in-detail' + ) + + return ( + <> + + + How a Formal Audit Works in Detail | Research | LFG Labs + + + + +
+ + +
+

+ How a Formal Audit Works in Detail +

+

+ The technical path from repo access to machine-checked security + guarantees. +

+
+ +
+

+ A formal audit is not just a normal audit with proofs added at the + end. The proof work changes the audit process itself. +

+

+ We first decide what the protocol must guarantee, then model the + relevant contract logic in{' '} + + Verity + + , then prove in{' '} + Lean 4{' '} + that the model satisfies the agreed specification. Bugs and + ambiguities usually appear during modeling, before the final proof + is complete. +

+
+ +
+

+ The audit pipeline +

+

+ The engagement starts from a fixed commit hash, but the work is + iterative. Every important claim needs a spec, a model, and a + proof. +

+ +
+ +
+

+ 1. Specification is the core audit work +

+
+

+ Before writing proofs, we audit the protocol with the team and + decide what actually matters: funds cannot be created out of + thin air, withdrawals cannot be replayed, state transitions are + authorized, accounting stays solvent, and edge cases behave + intentionally. +

+

+ The output is not a vague checklist. It is a set of formal + properties that engineers can review and sign off on before the + proof phase starts. +

+
+
+ {SPEC_EXAMPLE} +
+

+ This is where most audit judgment lives. If the wrong invariant is + specified, a perfect proof still proves the wrong thing. +

+
+ +
+

+ 2. We model only the security-relevant behavior +

+
+

+ Verity lets us encode EVM-style contract logic in Lean: storage + slots, mappings, require checks, uint256 arithmetic, transfers, + and state updates. The model is the executable object that the + proof talks about. +

+

+ The point is not to rewrite the whole repository mechanically. + The point is to model the behavior needed to prove the agreed + guarantees, while documenting every boundary that is assumed + rather than proved. +

+
+
+ {MODEL_EXAMPLE} +
+
+ +
+

+ 3. Proof turns the audit claim into a checkable artifact +

+

+ A theorem ties the implementation model to the signed-off spec. + Lean checks every case. If one branch is missing, if arithmetic + wraps unexpectedly, or if a state update breaks the invariant, the + proof does not compile. +

+ {PROOF_TASK} +

+ This is the difference between “we reviewed this” and + “this exact property was checked by a proof kernel.” +

+
+ +
+

+ 4. Bugs show up during modeling +

+
+

+ Modeling forces every implicit assumption into the open: which + state can change, which caller is authorized, which arithmetic + can overflow, which roots are valid, which nullifiers are spent, + and which off-chain component is trusted. +

+

+ When the model cannot satisfy the spec, we do not hide that + until the final report. We sync with the engineering team, + explain the failing case, let them patch, and continue from the + new behavior. +

+

+ The pre-audit report records the bugs, ambiguities, required + fixes, and the on-chain/off-chain attack surface before the + final proof is presented. +

+
+
+ +
+

+ 5. Circuits become explicit assumptions +

+
+

+ If the protocol uses circuits, we audit and formalize the + circuit specification in Lean. The circuit compiler and + underlying cryptography are outside the EVM proof unless they + are separately verified. +

+

+ That means the EVM proof can use a circuit guarantee as an + axiom, but the axiom must say exactly what is being trusted. +

+
+
+ {CIRCUIT_AXIOM} +
+

+ This is stronger than leaving the circuit as a black box. The + trusted boundary is named, scoped, and reviewable. +

+
+ +
+

+ 6. The benchmark shapes how we run proof tasks +

+

+ The{' '} + + Verity Benchmark + {' '} + is built around the same unit of work we use internally: fixed + implementation, fixed spec, one theorem to prove, and Lean as the + evaluator. +

+
+ + +
+

+ This keeps proof work honest. A proof is not accepted because it + looks plausible. It is accepted only if Lean checks it without + placeholders. +

+
+ +
+

+ 7. What the final deliverables contain +

+
+
+ Signed-off specs.{' '} + Human-reviewable invariants and threat assumptions written in + Lean. +
+
+ Verity model. The + machine-checkable model of the contract behavior used by the + proofs. +
+
+ Pre-fix report. Bugs, + ambiguities, exploit paths, and required changes found during + specification and modeling. +
+
+ Post-fix report. The + cleaned-up audit report after the engineering team addresses the + findings. +
+
+ Proof artifacts. Lean + files that anyone can re-run to independently check the claims. +
+
+
+ +
+

+ 8. Maintenance means re-proving equivalence +

+
+

+ After the audit, small implementation changes should not require + starting over. If the core invariants stay the same, we update + the Verity model and re-prove that the new implementation still + satisfies the same specs. +

+

+ If a change breaks or changes the core invariant, that is not + maintenance. It is new scope, because the security claim itself + changed. +

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

+ More research +

+
+ {otherResearch.map((r) => ( + + ))} +
+
+ )} +
+ + + ) +}