From Intent to Proof: Dafny Verification for Web Apps

Formal verification has never been part of web development culture. We think it should be.

Generative AI has changed who builds software and how. Less technical creators can now ship working products because LLMs can write functional code. Experienced engineers move faster because LLMs handle the tedious parts, freeing them to focus on architecture and design.

Using AI for code generation as it exists today means choosing between two imperfect options: Trust the output and iterate as bugs are discovered in production, or review the code to some lesser or greater extent manually, at which point the heavy supervision diminishes the productivity gains.

We recognize and want a third option: specify intent upfront, translate that into a mathematical property, and verify that all generated code satisfies it automatically. For the less technical creator this means far fewer bugs shipped, and for the experienced engineer this means far less supervision beyond the expression of intent and definition of specs.

The human states what should be true. The machine proves that it’s true. Code that cannot be proven to be true does not compile and is not surfaced to the user at all.

To enter this space, we are starting with UI state: foundational to modern web apps, deceptively difficult to get right, and an area where LLMs consistently struggle.

The Core Idea: How Verified State Evolution Works

If every state transition preserves a global invariant, then every state reachable through the system is correct — by construction.

We demonstrate the core idea with one of the most basic examples of UI state: undo/redo. We’re not here to re-invent replay — it’s a solved problem. We’re using replay as an anchor to demonstrate how verification might apply to a familiar methodology, and then imagine how it might extend to harder problems.

Applying verification to replay

Consider a counter that can’t go negative. The state invariant is simple: n ≥ 0. A user increments twice, undoes once, then decrements. What should redo do?

In linear undo (implemented by most applications) redo should do nothing. The decrement created a new timeline; the old future is gone. But a subtle bug (forgetting to clear the future on new actions) would let redo jump back to 2 — a state from a timeline where the user incremented, not decremented. No crash. No invalid state. Just silently wrong.

Now consider the same counter, but with the behavior defined upfront. The flow would be as such:

The human expresses intent in natural language:

“I need a counter for a shopping cart quantity. It can’t go below zero. Undo/redo should work like most apps — if I undo and then do something new, I can’t redo the old action anymore.”

The LLM translates this to a structured spec:

Model:      integer (quantity)  
Invariant:  quantity ≥ 0  
Actions:    increment, decrement  
Semantics:  linear undo — new actions clear the future

The human reviews and confirms or modifies. Then the LLM generates the implementation in Dafny, a verification-aware language. The proof requires:

1. Every state in history satisfies n ≥ 0
2. Do(action) sets future = []

The second requirement isn’t a lint rule or a code review comment. It’s part of the specification. If the LLM then incorrectly generates future: h.future instead of future: [], the proof fails. The code doesn’t compile and doesn’t surface for review.

The bug from the previous example — silently jumping to the wrong timeline — is not caught at runtime or by tests. Instead, because that implementation cannot be proven, the code cannot be generated.

The LLM then acts less like a generator of the most plausible implementation and more like a search for the correct implementation.

From toy example to real applications

A counter is trivial: one invariant, two functions. But the structure — specify, prove, compile — scales to domains where the invariants are global and the bugs are subtle:

• Kanban boards where cards must exist in exactly one column
• Capability delegation with transitive permissions
• Collaborative documents with referential integrity

Beyond Undo: Offline Collaboration

Replay handles a single user’s timeline. But what happens when multiple users edit the same board and one goes offline?

Alice drags card X to “Done.” Bob, working offline, drags the same card to position 2 in “In Progress”, right after card Y. When Bob reconnects, his action references a board state that no longer exists. Card Y might have moved. The column might be full.

Most systems pick one of two bad options:

• Reject. Bob’s action fails. His work disappears. Safe, but infuriating, especially if his intent (“put X in In Progress”) was perfectly valid against the current state.

• Rebase naively. Reinterpret Bob’s action against the new board. “Position 2” now means something different. Card X lands in the wrong place, or worse, if the naive logic has bugs, it duplicates, vanishes, or violates the column’s WIP limit.

The verified approach is different: try to preserve intent, prove what you accept.

When Bob’s action arrives, the server asks: can we interpret this in a way that satisfies the invariant? It tries Bob’s original placement first. If that fails (card Y is gone), it tries fallbacks — “at end of column,” “before the first card.” Only if every interpretation would violate the invariant does it reject.

The kernel proves: every accepted action produces a valid state. The server never accepts a corrupted board, no matter how stale the client or how concurrent the edits.

This is where replay becomes infrastructure. The same architecture — kernel, domain, proof obligation — handles problems that can’t be tested exhaustively.

The next section walks through how the methodology is built to scale to complex domains.

Implementation: Kernels, Domains & AppCore

The Architecture

Our system separates what’s generic from what’s application-specific. The fundamental capability here is that Dafny code can be verified and compiled to JavaScript. The specific architecture we’ve implemented here (separating kernels, domains, and AppCore) is one pattern for organizing that capability. Its benefit is reuse: prove a kernel once, plug in many domains. But it’s not the only way. A simpler project might verify a single module without the kernel abstraction. This separation of concerns is a design choice, not a requirement of the approach.

Kernels

Kernels are generic, reusable modules that encapsulate a pattern of state evolution and prove it correct once:

• A kernel is parameterized over a domain — it doesn’t know what the state looks like or what the actions mean, only that the domain satisfies certain proof obligations
• The kernel’s guarantees follow from those obligations — if the domain proves its transitions preserve the invariant, the kernel guarantees that all states it produces (including through undo, redo, sync, or conflict resolution) also satisfy that invariant
• Once a kernel is proved, it never needs to be touched again — new domains just plug in

We’ve built three kernels so far: replay (undo/redo), authority (client-server synchronization), and multi-collaboration (offline clients with conflict resolution). Each encapsulates a different pattern but all follow the same structure.

Domains

Domains are application logic — the part that’s unique to each app:

• At minimum, a domain defines Model (the data shape), Action (things users can do), and an invariant Inv (rules that must always be true of the model)
• More sophisticated kernels require more from domains. For example, the multi-collaboration kernel also needs Rebase (how to transform stale actions), Candidates (fallback interpretations when the original action fails), and Explains (what counts as preserving user intent)
• The domain interface is a contract with the kernel: define what it asks for, prove the obligations it requires, and the kernel guarantees its properties

AppCore

AppCore is the API layer that wires a domain to a kernel and exposes it to the application:

• It instantiates the generic kernel with a specific domain
• It exposes the methods the UI will actually call: Init, Dispatch, Undo, Redo, Present
• It handles the translation between the domain’s action types and the kernel’s generic interface

Think of it this way: the kernel is a template, the domain is business logic, and AppCore is the glue that produces a ready-to-use JavaScript module.

Responsibility by Layer

Each layer trusts the one below it.

File Structure

A typical verified domain example:

Replay.dfy          # Generic kernel (proved once, never touched)
KanbanDomain.dfy    # Domain: model, actions, invariant, proofs
                    # AppCore: Wires Kanban domain to Replay kernel, exposes API

compile.sh          # Dafny → JavaScript compilation

Kanban.cjs          # Compilation output: what the app imports
kanban/             # React app imports the compiled module

The .dfy files are where verification happens. The .cjs file is what ships. The React app imports the compiled module and calls its methods.

The Proof Obligation

If we take the replay kernel as an example, for each domain, one thing must be proved:

lemma ApplyPreservesInv(m: Model, a: Action)
  requires Inv(m)
  requires Valid(m, a)
  ensures Inv(Apply(m, a))

In plain terms: if the rules hold before an action, they hold after. That’s the only obligation for this specific kernel. Other kernels may include more obligations. In addition, each domain may have domain-specific guarantees beyond the kernel.

Proof Effort Scales with Complexity

The effort scales with domain complexity, not with the kernel’s logic. A counter domain (~50 lines of proofs) and the Kanban domain (~1,400 lines of proofs) share the same kernel.

Same Methodology, Different Shapes

To show this generalizes, we implemented three domains with the same replay kernel:

The domains look nothing alike. The methodology is identical:

1. Define Model, Action, Inv
2. Prove transitions preserve invariant Inv
3. Plug into the kernel
4. Compile to JavaScript

Undo/redo works automatically for all different data shapes, but with the same guarantees.

Try It & Contribute

The code is open. The demos work. The methodology is documented.

Most importantly, the paradigm shift is real.

• GitHub repository — kernels, domains, React integration, and Dafny source
• Dafny documentation — learn more about the verification language
• Get in touch — if you’re interested in collaborating or have a hard problem for us

About

This work is a collaboration between:

• Nada Amin — Assistant Professor at Harvard, specializing in programming languages and AI
• Fernanda Graciolli — Developer specializing in React apps and product design