Formally Modelling Optimism's Supernode: A Dafny Model, an AI Reviewer, and What They Achieved Together

Cross-chain interoperability is one of the hardest correctness problems in the OP Stack today. The Supernode is the component tasked with solving it: it watches every L2 in a chain cluster, checks that "executing messages" on one chain genuinely correspond to "initiating messages" on another, and advances the cross-safe frontier that the rest of the protocol relies on, but only once it's confirmed everything lines up. For that purpose, it's important to ensure that the Supernode correctly determines which messages are valid and which are invalid. Get it wrong in one direction, and a chain can build on cross-chain state that was never actually valid. Get it wrong in the other direction and the whole cluster's progress stalls for no reason.

During our second engagement with the Optimism team, a 10-week extension of an initial 9-week audit, we used formal methods to attack this problem: a hand-built Dafny model of the Supernode's core logic, and a systematic AI-driven comparison of that model against the actual Go implementation. This post walks through both, and how they were used to help build confidence on the Supernode design.

Why this matters

If you've done formal verification work, you know the usual arc: build a model, prove some properties, ship the proofs as an artifact, and watch the model quietly retire. We have been exploring how to keep getting value out of the model beyond the audit engagement.

Expert formal modeling makes every other stage of review sharper, and it stays cheap to keep paying off long after the proofs are done. A model built once gives an AI reviewer ground truth to check against instead of guessed intent. It tells you exactly where your own simplifying assumptions are shaky when the AI reviewer comes back with an uncertain result. And it can be turned into a fuzzing harness that keeps catching regressions long after the engagement ends. Formal modeling, AI-assisted review, and fuzzing compound when chained together, and fuzzing is what lets you confirm that the compounding is actually working: it runs the real implementation against properties the model proved and reports when the two come apart. In addition to identified bugs, the engagement produces a specification, trusted and continuously checked from three different directions, that the team can lean on as the system keeps evolving.

Why formal verification, and why Dafny

Manual code review catches bugs you can imagine. Formal verification is complementary: it forces you to state precisely what "correct" means and checks that statement against every reachable state, including the ones nobody would think to trace by hand. For a component like the Supernode, where correctness depends on a chain of database consistency conditions holding across rewinds, restarts, and partial failures, having that precise, machine-checked statement is valuable on its own, whether there are bugs to be found or not.

We chose the Dafny programming language because it lets us write an abstract model of the system, its state, its methods, and the properties those methods must preserve, and then use Dafny’s built-in formal verification capabilities to have an automated theorem prover check whether these properties hold. Specifically, this meant writing:

• Methods, annotated with requires (preconditions) and ensures (postconditions) clauses, that mirror the Supernode's state-mutating operations.
• Functions and predicates, pure and side-effect-free, that express the invariants we wanted to hold.
• Lemmas that help Dafny's prover along when a property doesn't follow trivially from the definitions.

We left some components deliberately abstract. Rather than modeling every implementation detail of the ChainContainer or LogsDB components, we specified only their expected behavior through preconditions and postconditions, marking those specifications with Dafny's {:axiom} attribute to indicate we are assuming rather than proving them. This is a standard technique for keeping a model tractable: it focuses the proof effort on the logic that matters most (here, the core cross-validation loop in Interop.dfy) while still giving a rigorous contract for everything that logic depends on.

Here's what that looks like for LogsDB.Rewind, one of the operations we treated as an axiom rather than modeled in full:

The method has no body: we assume the contract holds rather than proving it from a lower-level model of the database. This then becomes a rigorous specification for the behavior of the components, which can guide future review, development and testing.

What we proved

The model centers on three families of invariants, all carried as pre- and postconditions of the Supernode's main entry point, ProgressAndRecord:

Base invariants cover the basic internal consistency of the system. This includes that the VerifiedDB's timestamps run sequentially with no gaps, every PendingTransition is well-formed, and the data recorded in the VerifiedDB and LogsDBs matches what's on the L2 chain (or was, if the chain has suffered a reorg).

Database consistency invariants are trickier. These specify what "in sync" means between the VerifiedDB and the LogsDBs, both in steady state and in the middle of applying a PendingTransition.

The Supernode can be interrupted at any point by a transient error, and when it resumes it needs to pick the transition back up and complete it idempotently. We proved that with no pending transition, the two databases stay in sync, and that applying a pending transition successfully restores that sync. This is exactly the recovery guarantee the implementation is supposed to provide.

Cross-validity of verified entries is the central property that matters most directly to users of the system. For every L2 head recorded as verified, every executing message it contains needs a corresponding initiating message that exists, isn't expired, and was included before the executing message's timestamp. We proved this both for entries already committed to the VerifiedDB and for any pending Advance transition, so we can know the property continues to hold once the transition is applied and the entry is added to the database.

Turning the model into an AI reviewer

The Dafny model gives you ground truth for what the Go implementation is supposed to do. The natural next question, and the focus of the extension's second phase, was whether we could use that model to systematically check the implementation function by function, rather than relying entirely on manual comparison.

We built on infrastructure from our AI audit tooling and pointed it at the problem of validating the implementation against the specification provided by the model. The resulting workflow looks like the following:

1. Build a callgraph of the Go codebase (using Trail of Bits' Trailmark so we know, for any function, exactly who calls it and who it calls.
2. Map each modeled Dafny method to the Go function it's meant to correspond to.
3. For every function in that map, spin up an independent agent to check it in isolation, split into a precondition analysis (can every caller of the function actually guarantee the preconditions hold at the callsite?) and a postcondition analysis (does the function body, assuming its preconditions, actually establish the specified postconditions?).
4. Compile all of this into a report, with each condition classified as Satisfied, Violated, or Uncertain, and a description of the failure scenario where relevant.

The key design choice was keeping each function's analysis modular. Rather than giving the agent a callee's full implementation, we gave it that callee's Dafny contract: its requires, ensures, and modifies clauses. Since every callee is also independently checked against that same contract elsewhere in the pipeline, the overall analysis stays sound without ballooning the context each individual check has to reason about. It's the same divide-and-conquer principle that makes modular formal verification tractable in the first place, applied here with an LLM doing the checking instead of a proof search.

Across the sixteen functions analyzed this way, most conditions came back Satisfied. A handful came back Violated, but on inspection, rather than defects in the implementation, these were consistently cases where the Go code had to handle an implementation detail abstracted away by the model (like a database bootstrapping requirement) or where the model and the code had diverged due to more recent changes in the implementation. However, these results helped surface a bug in the form of a rewind edge case around cold-start backfill. On cold start, the Supernode backfills its LogsDBs with blocks older than its first verified timestamp so later executing messages can still reference them. The rewind-planning logic computes its target heads from the VerifiedDB entry at the rewind target, and if the rewind target lands at a timestamp before backfill began, that entry doesn't exist, so the target heads come back nil. The implementation responds to a nil target by clearing the LogsDBs entirely, silently deleting the backfilled blocks with no way to reconstruct them. Any future executing message depending on those blocks would then be rejected incorrectly. It's a narrow, easy-to-miss boundary condition, exactly the kind of issue that formally specifying a property and asking whether it holds in every reachable state is well suited to surface. The Optimism team has since addressed the issue: a rewind that would delete the backfilled blocks now halts the Supernode before anything is written, with instructions for the operator to wipe the affected databases and restart so that backfill runs again.

Also interesting were the conditions that came back "Uncertain." Rather than cases where the AI reviewer simply failed to reach a conclusion, in many instances these were cases where the model makes simplifying assumptions, or where the analysis depended on a function not specified in the model. For example, some methods in Dafny's LogsDB are modeled as always succeeding when its inputs are valid, which keeps the core logic proof tractable, but Go has to handle I/O errors, partial writes, and network failures. Every "Uncertain" postcondition tracing back to processBlockLogs or ApplyRewindPlan boils down to the same question: if a database write fails halfway through, does the invariant still hold on the error path? This kind of result highlights the simplifying assumptions in the model and points towards remaining gaps between the model and the code, and might suggest areas that deserve attention in future revisions.

Closing the loop with fuzzing

Beyond the proofs and AI analysis, the formal model had an additional role in extending our fuzzing harness. Rather than hand-writing fuzzing assertions, we had an LLM derive Go predicate checkers that follow the Dafny invariants, conjunct for conjunct, and ran them after every simulated round of cross-validation, on both the valid path and the adversarial path. A violation reported by the fuzzer is, by construction, a violation of a property we'd already formally proven should hold. A fuzzing failure means the implementation diverges from a specification we trust, not just that something looks off. We also used the harness to exercise areas the static analysis reasons about less well, like fault injection into the VerifiedDB and engine rewind paths, and multi-round adversarial sequences that are hard to reconstruct by hand.

The engine behind the harness is a chain randomizer, iterated forward from the one we built during the first engagement. From a single seed it synthesizes an entire cross-chain cluster: multiple L2s with their own safe-head histories, a shared L1 with reorgs, and executing messages deliberately wired back to real initiating messages on sibling chains, so that the valid path is valid by construction rather than by luck. Each synthetic chain implements the same interfaces the Supernode's real engine and virtual-node code consume, which means the actual implementation runs unmodified against generated data instead of a bespoke test double. The adversarial path is then produced by a set of targeted mutators layered on top of that valid baseline, breaking a single executing message, opening an L1 divergence, punching a gap in a LogsDB's front, or reorging L1 out from under an in-flight transition, so every failure the fuzzer reports is a specific, reproducible perturbation of an otherwise consistent world, and the seed that produced it replays the exact sequence on demand.

Why this combination works

Formal modeling, AI-assisted spec comparison, and fuzzing each cover a gap the others leave open. The Dafny model gives a precise, provable statement of what "correct" means, but can't confirm the Go code actually implements it. Manual and AI-assisted code review can check that correspondence, but doing it exhaustively by hand doesn't scale at the size of a real production codebase, and doing it with an LLM alone risks confident-sounding wrong answers. Fuzzing explores state spaces the reviewer might miss, but needs to know the properties to check for.

Put together, they compound. The model gives the AI reviewer ground truth to check against instead of having to infer intent from code. The AI reviewer's results point to potential gaps between the model and the implementation, and what parts of the code might deserve more attention. And the fuzzer turns the whole specification into an executable, continuously-run regression suite that keeps catching drift long after the audit engagement ends. The end result is a shared, precisely stated, independently verified contract that the team, and future reviewers, can trust.

That last part matters most for a codebase like the Supernode, which is still evolving and may be reimplemented in Optimism’s Rust consensus client. A benchmark suite grounded in a formal specification, and not in the quirks of a single implementation, makes a rewrite safer: it tests that both the old and new code satisfy the same contract, rather than just that the new code resembles the old.

If you are also building a system where correctness really matters, reach out.