Graphiti: Formally Verified Out-of-Order Execution in Dataflow Circuits

Yann Herklotz, Ayatallah Elakhras, Martina Camaioni, Paolo Ienne, Lana Josipovic and Thomas Bourgeat

High-level synthesis turns C programs into hardware, and for irregular code the best results come from dataflow circuits that borrow out-of-order execution from CPUs — letting a fast loop iteration overtake a slow one — but reordering makes these circuits so subtle that the transformations risk silent bugs that scare a conservative industry off adopting them; this paper (EPFL and ETH Zurich — Yann Herklotz, Lana Josipovic, Thomas Bourgeat, and colleagues) builds Graphiti, a Lean 4 framework that treats dataflow-circuit optimizations as formally verified graph rewrites, proves an out-of-order loop rewrite correct (catching a real bug in the prior unverified version), and delivers 2.1 times the speed of in-order HLS with no loss versus the unverified out-of-order approach.

The argument in one glance

Problem

The fastest hardware compilers reorder work, and reordering is where bugs hide

High-level synthesis lets you write a program in C and have a tool build the hardware circuit for you, instead of hand-writing low-level register-transfer descriptions. For regular, predictable code a fixed compile-time schedule works well, but for irregular programs the best results come from dynamic high-level synthesis, which generates a dataflow circuit whose parts fire as their data arrives. To push performance further, these tools have started borrowing tricks from out-of-order processors: letting a later, independent loop iteration overtake an earlier one that is stuck on a slow computation, so a shared operator stays busy instead of stalling. This is a real speedup, but it comes at a price in trust. Once operations can run out of order, the circuit has a swarm of subtle emerging behaviors, and the transformations that introduce the reordering are so intricate that it is easy to get them subtly wrong, producing a circuit that computes the wrong answer in some cases.
What people did

Implement the aggressive out-of-order optimization and test it

The state of the art is to implement these dataflow-circuit optimizations directly in the compiler and validate them by testing on a suite of benchmarks — build the transformation that inserts out-of-order execution, run it on example programs, check the outputs, and ship it if the benchmarks pass.
Why it fell short

Testing misses subtle reordering bugs, and industry will not trust that

Testing cannot cover the enormous space of emerging behaviors that out-of-order execution creates, so unsound optimizations slip through: the paper finds that the original, unverified implementation of exactly this out-of-order optimization silently produced a wrong circuit for one of its own reported benchmarks. Hardware bugs are extraordinarily expensive to fix once fabricated, and the industry that would benefit from these aggressive transformations is conservative and slow to adopt anything it cannot trust. Without a way to prove the transformations correct rather than merely test them, the performance is left on the table.
This paper's idea

Treat the optimizations as graph rewrites and prove them correct in a proof assistant

Graphiti is a framework embedded in the Lean 4 proof assistant for formally reasoning about and manipulating dataflow circuits. Its core idea is to view a dataflow-circuit optimization as a graph rewrite — the hardware analogue of the term rewrites that optimizing software compilers perform — and to give it a formal semantics and a notion of equivalence so the rewrite can be proved correct. Because out-of-order execution introduces local nondeterminism that the classic dataflow semantics cannot even express, Graphiti develops a metatheory of graph refinement rich enough to capture it, and uses it to verify a general-purpose dataflow-circuit rewriting algorithm. With this, the authors formally prove correct the loop rewrite that introduces out-of-order execution — catching, in the process, the bug in the prior unverified version. The verified pipeline runs 2.1 times faster than in-order HLS and 5.8 times faster than a verified static-schedule tool, matching the unverified out-of-order approach with none of its risk.

Why this problem is worth solving

The performance is real and the domain is exactly where correctness matters most.

High-level synthesis compiles an imperative program, usually C, into a hardware circuit. The mature, industrial style is static scheduling, which fixes at compile time exactly what happens on each clock cycle — excellent for regular loop nests but poor for irregular code whose behavior depends on the data. Dynamic HLS instead produces a dataflow circuit: a latency-insensitive network of components (branches, multiplexers, merges, forks, operators, joins) that pass data tokens and fire whenever their inputs are ready, coordinating by local handshakes rather than a global schedule. This runtime flexibility is what lets it handle irregular programs well, and it invites processor-style optimizations. The most powerful recent one is out-of-order execution: in a loop whose iterations take different amounts of time — a greatest-common-divisor computation, say, where some inputs converge fast and others slowly — an in-order circuit stalls behind its slowest iteration, while an out-of-order circuit lets a quick later iteration flow through a shared operator ahead of a stuck earlier one, keeping the hardware busy. A tagging scheme (a Tagger marks each iteration and lets them reorder inside a region, an Untagger restores the original output order) makes this correct in principle. The technique delivers genuine speedups, so it is worth getting right — and because it targets fabricated hardware, where a bug can cost a fortune, getting it right is not optional.

The trouble is that the very feature that makes it fast makes it nearly impossible to reason about informally.

Correctness of a compiler optimization means the transformed program behaves like the original. For an in-order, deterministic circuit that is hard enough; for an out-of-order one it becomes qualitatively worse, because reordering introduces local nondeterminism — at a shared resource, which of several ready iterations goes first is not fixed, so the circuit can evolve along many different internal paths, all of which must produce the same final answer. The number of these emerging behaviors is vast, which is exactly why out-of-order bugs in both software and hardware are notoriously subtle and time-consuming to debug, and why testing, which samples only a handful of paths, is a weak guarantee. It gets worse at the level of formal theory: the classical semantics for dataflow networks, Kahn’s, assumes deterministic components and therefore literally cannot express the local nondeterminism that out-of-order execution relies on. So a would-be verifier cannot just reach for the standard framework; the right notion of equivalence is not equality of outputs under a deterministic model but a simulation, or refinement, relation that permits the reordered circuit to take different internal routes while still refining the original’s behavior. Building that semantic foundation is the prerequisite for any rigorous claim about these optimizations, and its absence is why the field had aggressive transformations but no proofs.

What people did before, and where it broke

Static-schedule HLS, including verified versions. Fix the schedule at compile time; tools like Vericert even formally verify this flow, generating a static state machine. Where it broke. Static scheduling handles irregular, data-dependent code poorly, so it leaves large speedups unrealized — the paper measures the verified static tool as 5.8 times slower than its out-of-order dataflow result.
Dynamic HLS with in-order dataflow circuits. Generate a dataflow circuit that fires on data availability but keeps iterations in order. Where it broke. An in-order circuit stalls behind its slowest iteration, so on irregular loops it wastes the shared operators that a reordered schedule could keep busy — about 2.1 times slower than the out-of-order version.
Aggressive out-of-order dataflow optimizations, unverified. Implement tagged out-of-order execution in the compiler and validate by testing on benchmarks. Where it broke. Testing cannot cover the huge space of reordering behaviors; the original unverified implementation of this optimization silently produced an incorrect circuit for one of its own reported benchmarks.
Classical dataflow semantics for reasoning. Try to reason about the circuits with Kahn-network semantics. Where it broke. Kahn semantics assume deterministic components and cannot express the local nondeterminism at shared resources that out-of-order execution requires, so they are simply inadequate as a basis for proving these optimizations correct.
The gap. No framework gave dataflow-circuit optimizations a formal semantics that captures out-of-order nondeterminism, a notion of graph equivalence to prove rewrites against, and a mechanized proof — so the fastest transformations remained untrusted and their adoption stalled.

How Graphiti works

Turning an untrusted out-of-order optimization into a proved-correct graph rewrite

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Make hardware-circuit optimizations first-class rewrites with a correctness story, like compiler optimizations already have. The organizing insight is an analogy: an optimizing software compiler improves a program by term rewrites, and it can prove those correct because it has a formal language semantics and a notion of program equivalence. Graphiti argues a dataflow-circuit optimization is the same kind of thing — a rewrite, but on a circuit graph rather than a syntax tree — and so it deserves the same rigorous treatment. It builds the missing pieces: a formal semantics for dataflow-circuit graphs and a notion of when one graph is equivalent to (refines) another, so that any optimization phrased as a graph rewrite can be stated and proved correct instead of merely tested. This turns a grab-bag of clever but untrusted transformations into a principled, extensible engine where each new optimization is a verified rewrite. Treating a dataflow-circuit transformation as a rewrite to be formally verified against a semantics, rather than an ad-hoc pass validated by testing, is the same foundational move the formally-verified dataflow-circuit-rewrites work covered elsewhere on this site makes, putting circuit optimizations on the same proof footing that program optimizations enjoy. Graphiti extends this to the hardest case — the out-of-order rewrite whose nondeterminism defeats simpler approaches.

Invent the semantics the problem actually needs, because the classic one cannot hold nondeterminism. The reason no one had verified these optimizations is not laziness but a genuine theoretical gap: the standard semantics for dataflow networks, Kahn’s, is built on deterministic components, and out-of-order execution is fundamentally about local nondeterminism — at a shared operator, ready iterations may proceed in different orders, and the circuit must be correct along all of them. So Graphiti cannot reuse the textbook model; it develops a metatheory of graph refinement in which correctness is a simulation relation, letting the reordered circuit wander through different internal states as long as it still refines the behavior of the original. This choice of refinement over strict equality is precisely what makes a proof about out-of-order execution possible at all. Confronting a nondeterministic system with a verification framework designed to reason about nondeterminism head-on, rather than forcing it into a deterministic mold, is the same necessity the work on verifying nondeterministic quantum programs covered elsewhere on this site faces, where the logic itself has to be built to accommodate behavior that is not fixed in advance. Graphiti’s refinement metatheory is the dataflow-circuit counterpart of that move.

Verify only the trusted core, and let a proof assistant carry the guarantee. A framework is only useful if the proofs are actually checkable and the effort is bounded, so Graphiti is embedded in the Lean 4 proof assistant, which mechanically checks every step of every proof — no hand-waving, no gaps. Practically, it separates the flexible part from the trusted part: an unverified matcher works on a convenient graph form (ExprHigh) to locate where an optimization applies, while the transformation that must be correct runs on an inductively defined form (ExprLow) whose rewriting function is proved sound once and reused. The payoff of this structure shows in the numbers: the whole development is about sixteen thousand lines of Lean and roughly a person-year, but verifying the specific out-of-order loop rewrite took only about sixteen hundred of those lines, because it builds on the reusable, already-proved framework. Encoding a system’s semantics and correctness proofs in a mechanized proof assistant so the guarantee is machine-checked and the framework is reusable across cases is the same discipline the mechanised-semantics work for CHERI-C capabilities covered elsewhere on this site is built on, formalizing the model once in a proof assistant so later results stand on a checked foundation rather than informal argument.

Following the out-of-order rewrite through Graphiti

Verifiably introducing out-of-order execution into a GCD loop circuit

A trace, drawn from the paper's design, of how Graphiti transforms and proves correct a dataflow-circuit loop that gains out-of-order execution.

Step 1 of 5

An in-order dataflow circuit for a variable-latency loop

The starting point is a dataflow circuit for a loop whose iterations take different, data-dependent amounts of time — for example a greatest-common-divisor inner loop over arrays. In order, a slow iteration blocks the shared operators, so a later fast iteration cannot make progress until the slow one finishes.

This head-of-line stalling is exactly the inefficiency out-of-order execution removes, by letting independent iterations overtake one another.

Why it works

Framing optimizations as rewrites imports the compiler-correctness toolkit. Circuit optimizations lacked a correctness discipline → but casting them as graph rewrites with a formal semantics and equivalence notion mirrors verified term rewriting → so each transformation can be proved sound the way compiler passes are.
A refinement semantics captures nondeterminism that Kahn cannot. Out-of-order execution needs local nondeterminism, which deterministic Kahn semantics cannot express → but a simulation-based refinement relation lets the reordered circuit take different internal paths → so correctness of out-of-order rewrites becomes provable rather than merely testable.
Splitting matching from rewriting shrinks the trusted base. Verifying a flexible pattern-matcher would be onerous and brittle → but running matching unverified on ExprHigh and the transformation verified on ExprLow → so only the small trusted rewriting core carries proof obligations.
A reusable framework makes each new proof cheap. Verifying every optimization from scratch would be prohibitive → but a once-proved general rewriting algorithm and refinement metatheory are reused → so the specific out-of-order loop rewrite needed only about 1,600 of the roughly 16,000 lines.
Proof beats testing on the behaviors that hide bugs. Testing samples a few of the vast out-of-order execution paths → but a machine-checked refinement proof covers them all → so Graphiti catches an error the unverified, tested implementation shipped, while matching its speed.

What it costs (trade-offs and scope)

It verifies one optimization, not a whole HLS flow. Graphiti proves the out-of-order loop rewrite correct and provides the framework, but it is explicitly a step toward a fully verified HLS flow, not a complete one; the front-end matcher and the surrounding compiler (for example Dynamatic’s generation and buffer placement) are not themselves verified here.
Formal verification is substantial effort. The development is about 16,000 lines of Lean 4 and roughly a person-year; although the reusable framework makes each additional rewrite far cheaper (about 1,600 lines for the loop rewrite), building and extending it demands proof-assistant expertise that ordinary compiler engineering does not.
A new semantics had to be built and must be trusted. Because Kahn semantics were inadequate, Graphiti defines its own syntax, component semantics, and refinement metatheory; the guarantee is only as meaningful as those definitions faithfully model the real circuits, which is a modeling assumption at the base of any formal result.
The performance numbers depend on the workloads and baselines. The 2.1-times and 5.8-times figures are geometric-mean-style results over benchmarks that exhibit variable-latency, irregular behavior favorable to out-of-order execution, against specific tools (Dynamatic in-order and Vericert); code without such irregularity would gain less, and the comparison to Vericert required extending it to the benchmarks.
It matches, rather than exceeds, the unverified approach. Graphiti’s contribution is trust at no performance cost, not faster hardware than the best unverified method; its value is that the same speedup now comes with a proof, so the argument is about eliminating risk, not raising the performance ceiling.

The evaluation

Compiling irregular C loops to fast, trustworthy hardware

Property	Verified static schedule (Vericert)	Unverified out-of-order	Graphiti
Handles irregular, variable-latency code
Introduces out-of-order execution
Correctness guarantee
Handles out-of-order nondeterminism
Reported performance

A comparison drawn from the paper. Graphiti's verified out-of-order pipeline is evaluated on dataflow circuits from Dynamatic against the in-order flow, the unverified out-of-order approach, and the verified static-schedule tool Vericert; the 2.1-times and 5.8-times figures are the paper's reported speedups.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The full paper text was available (the authors’ own copy from an author’s site), so this account of the mechanism — dynamic HLS and dataflow circuits, tagged out-of-order execution via Taggers and Untaggers, the correctness difficulty from local nondeterminism and the inadequacy of Kahn semantics, Graphiti’s framing of optimizations as verified graph rewrites, the graph-refinement metatheory, the ExprHigh matcher and verified ExprLow rewriting, and the multi-step proof of the out-of-order loop rewrite in Lean 4 — follows the paper’s own description. The headline numbers are the paper’s reported results: a 2.1 times speedup over the in-order HLS flow and a 5.8 times speedup over the verified static-schedule tool Vericert, matching the unverified out-of-order approach in performance, with the development totaling about 16,000 lines of Lean 4 (around 1,600 for the loop rewrite) over roughly a person-year, and the discovery that the prior unverified implementation incorrectly optimized one of its own benchmarks. Those figures come from specific benchmarks and tools; results vary with the workload’s irregularity. Exact per-benchmark numbers, the formal definitions, and the proof structure should be read from the paper itself.

Background

Why hardware wants proofs, not just tests

It is worth remembering why formal verification is worth its considerable cost here in particular. Software bugs, however painful, can usually be patched after release; a hardware bug baked into a fabricated chip cannot, and recalling or working around silicon is famously ruinous, which is why the classic processor bugs of the past became cautionary tales. That asymmetry makes the hardware industry conservative: it adopts a new, aggressive compiler optimization only when it can trust that the optimization will not corrupt a design, and testing, which can only sample behaviors, is a weak basis for that trust — especially for out-of-order execution, whose whole point is to explore many orderings, most of which a test suite will never hit. A machine-checked proof is different in kind: it covers every behavior at once, turning “we tried hard to break it and could not” into “it cannot behave wrongly.” That is precisely what a conservative industry needs to green-light the fast-but-subtle transformations it has so far kept at arm’s length. This drive to give hardware and its compilation a rigorous, mechanized correctness foundation rather than an empirical one is the same commitment the formal-mechanised-semantics work covered elsewhere on this site embodies, replacing informal confidence with a checked model. Graphiti brings that commitment to the specific, high-value case of out-of-order dataflow-circuit optimization.

If you remember only three things

1. High-level synthesis builds hardware from C, and for irregular code dynamic HLS produces dataflow circuits that borrow out-of-order execution from processors — letting a fast loop iteration overtake a slow one through a shared operator — for real speedups; but reordering creates a vast space of subtle emerging behaviors, so these transformations are hard to reason about, easy to make unsound, and prone to costly hardware bugs that testing misses and that make a conservative industry wary of adopting them.
2. Graphiti, embedded in the Lean 4 proof assistant, treats a dataflow-circuit optimization as a formally verified graph rewrite (the hardware analogue of a compiler term rewrite). Because out-of-order execution needs local nondeterminism that classical Kahn dataflow semantics cannot express, it develops a metatheory of graph refinement (a simulation relation) to verify a general rewriting algorithm, splits the flow into an unverified matcher on an ExprHigh graph and a verified rewrite on an inductively defined ExprLow graph, and uses this to prove the out-of-order loop rewrite correct — catching a real bug that the prior unverified implementation had shipped on one of its own benchmarks.
3. The verified pipeline runs 2.1 times faster than the in-order HLS flow and 5.8 times faster than the verified static-schedule tool Vericert, and matches the unverified out-of-order approach with none of its risk. The Lean development is about 16,000 lines over roughly a person-year, but the reusable framework meant the specific loop rewrite took only about 1,600 lines. Graphiti verifies one optimization rather than a whole HLS flow, but stands as a step toward fully verified dataflow HLS and an extensible verified optimizing engine for existing tools.

Check yourself

Check your understanding

1. Why does out-of-order execution make dataflow-circuit optimizations so hard to get right?
2. What is Graphiti's central idea for making these optimizations trustworthy?
3. Why couldn't Graphiti just reuse the classical (Kahn) semantics for dataflow networks?
4. What are Graphiti's main results, and what is the nature of its contribution?

Sources

The paper is “Graphiti: Formally Verified Out-of-Order Execution in Dataflow Circuits” by Yann Herklotz, Ayatallah Elakhras, Martina Camaioni, Paolo Ienne, and Thomas Bourgeat (EPFL) and Lana Josipovic (ETH Zurich), published at ASPLOS 2026, DOI 10.1145/3779212.3790166. It is licensed CC BY.

This explainer is based on the paper’s full text, obtained from an author’s copy (yannherklotz.com). The account of the mechanism — high-level synthesis and the distinction between static scheduling and dynamic HLS producing dataflow circuits; the components of dataflow circuits and tagged out-of-order execution via Taggers and Untaggers that reorder loop iterations and restore output order; the correctness challenge posed by local nondeterminism and the inadequacy of classical Kahn semantics; Graphiti’s reframing of optimizations as graph rewrites embedded in the Lean 4 proof assistant; the metatheory of graph refinement (a simulation relation) used to verify a general-purpose rewriting algorithm; the tool flow with an unverified ExprHigh matcher and a verified ExprLow rewriting function; and the multi-step proof of the out-of-order loop rewrite (normalization, pure generation, the main loop rewrite, and conversion back) — follows the paper’s own description. The reported results cited here are the paper’s own: a 2.1 times speedup over the in-order HLS flow and a 5.8 times speedup over the verified static-schedule tool Vericert, matching the performance of the existing unverified out-of-order approach; a development of about 15,806 lines of Lean 4 over roughly one person-year, of which about 1,600 lines were needed for the loop rewrite; and the discovery that the original unverified implementation incorrectly optimized one of its reported benchmarks. Evaluation used dataflow circuits from Dynamatic and compared against Dynamatic’s in-order flow, the unverified out-of-order approach, and Vericert. Exact per-benchmark numbers, the formal definitions, and the proof structure should be read from the paper itself.