Quickstart: Build a Verified React App Using Dafny

This guide walks you through building a simple increment/decrement counter app where the state machine is formally verified in Dafny, compiled to JavaScript, and wired into a React component. The counter’s invariant — that the value is always non-negative — is proved at compile time and preserved by every state transition, including undo and redo.

Prerequisites: Dafny installed and available in PATH, Node.js and npm, and the dafny2js tool from the repository.

Architecture overview

Before diving in, here is how the pieces fit together:

MyAppDomain.dfy          # Verified state machine (you write this)
        |
        v
dafny translate js       # Compile to JavaScript
        |
        v
MyApp.cjs                # Generated Dafny code (do not edit)
        |
        v
dafny2js                 # Generate integration layer
        |
        v
app.js                   # Generated API wrapper (do not edit)
        |
        v
App.jsx                  # React component (you write this)

React owns rendering. Dafny owns state transitions. The boundary is clean: your component calls App.Dispatch, App.Undo, and App.Redo; everything below that line is verified.

Steps

Understand the Replay framework

The Replay.dfy file (already in the repository at kernels/Replay.dfy) defines two abstract modules you will refine:

Domain — the interface your app must implement: Model, Action, Inv, Apply, Normalize, and two lemmas.
Kernel — the generic history manager proved once; provides Do, Undo, Redo, and all correctness theorems.

You never modify these files. You refine them.

Create the Dafny domain

Create MyAppDomain.dfy alongside kernels/Replay.dfy:

include "Replay.dfy"

module MyAppDomain refines Domain {
  type Model = int

  datatype Action = Inc | Dec

  predicate Inv(m: Model) {
    m >= 0
  }

  function Apply(m: Model, a: Action): Model {
    match a
    case Inc => m + 1
    case Dec => m - 1
  }

  function Normalize(m: Model): Model {
    if m < 0 then 0 else m
  }

  lemma StepPreservesInv(m: Model, a: Action)
    ensures Inv(Normalize(Apply(m, a)))
  {
  }
}

module MyAppKernel refines Kernel {
  import D = MyAppDomain
}

module AppCore {
  import K = MyAppKernel
  import D = MyAppDomain

  function Init(): K.History { K.History([], 0, []) }

  function Inc(): D.Action { D.Inc }
  function Dec(): D.Action { D.Dec }

  function Dispatch(h: K.History, a: D.Action): K.History { K.Do(h, a) }
  function Undo(h: K.History): K.History { K.Undo(h) }
  function Redo(h: K.History): K.History { K.Redo(h) }

  function Present(h: K.History): D.Model { h.present }
  function CanUndo(h: K.History): bool { |h.past| > 0 }
  function CanRedo(h: K.History): bool { |h.future| > 0 }
}

The file has three modules:

MyAppDomain — your domain: Model = int, invariant m >= 0, Apply for transitions, Normalize to clamp negatives back to zero, and the StepPreservesInv lemma (the body is empty because Dafny can verify it automatically for this simple case).
MyAppKernel — wires your domain into the generic kernel.
AppCore — the public React-facing API: Init, Dispatch, Undo, Redo, Present, CanUndo, CanRedo.

Normalize is the key to invariant preservation for Dec: it clamps the result to zero when it would go negative. The StepPreservesInv lemma proves this works for all inputs.

Verify the Dafny code

dafny verify MyAppDomain.dfy

Dafny checks that:

Inv(Init()) holds (the initial value 0 satisfies m >= 0)
For every m and a, Inv(Normalize(Apply(m, a))) holds

If verification passes, you have a mathematical proof that the invariant holds for every reachable state.

Verification must pass before compiling. Skipping verification with --no-verify produces working JavaScript but loses all correctness guarantees.

Create the React app with Vite

From the repository root:

npm create vite@latest my-app -- --template react
cd my-app
npm install
npm install bignumber.js
cd ..

Dafny compiles integers to BigNumber, so bignumber.js is a required runtime dependency.

Configure Vite

Edit my-app/vite.config.js:

import { defineConfig } from 'vite'
import react from '@vitejs/plugin-react'

export default defineConfig({
  plugins: [react()],
  optimizeDeps: {
    include: ['bignumber.js'],
  },
})

This ensures Vite pre-bundles bignumber.js correctly alongside the CommonJS Dafny output.

Compile Dafny to JavaScript and generate app.js

The dafny2js tool generates the integration layer — it reads your AppCore module and emits a clean ESM wrapper that handles all type conversions between JavaScript and Dafny.

# Create output directories
mkdir -p generated my-app/src/dafny

# Compile Dafny to JavaScript (skip verification since we already verified above)
dafny translate js --no-verify -o generated/MyApp --include-runtime MyAppDomain.dfy

# Copy the generated JavaScript
cp generated/MyApp.js my-app/src/dafny/MyApp.cjs

# Generate the app.js integration layer
dotnet run --project dafny2js -- \
  --file MyAppDomain.dfy \
  --app-core AppCore \
  --cjs-name MyApp.cjs \
  --output my-app/src/dafny/app.js

The generated app.js provides:

Proper ESM imports for the Dafny runtime
Type converters (toJson/fromJson) for all datatypes
Action constructors that accept JS values and convert to Dafny types
All functions from AppCore wrapped for direct calling

Do not edit MyApp.cjs or app.js directly. Regenerate them with the commands above after any change to your .dfy file.

Write the React component

Replace my-app/src/App.jsx:

import { useState } from 'react'
import App from './dafny/app.js'
import './App.css'

function MyApp() {
  // Store the Dafny History in React state
  const [h, setH] = useState(() => App.Init())

  const inc = () => setH(App.Dispatch(h, App.Inc()))
  const dec = () => setH(App.Dispatch(h, App.Dec()))
  const undo = () => setH(App.Undo(h))
  const redo = () => setH(App.Redo(h))

  return (
    <>
      <h1>My Dafny App</h1>
      <p className="subtitle">Verified, replayable reducer kernel</p>

      <div className="card">
        <div className="value">{App.Present(h)}</div>

        <div className="button-row">
          <button onClick={dec}>Dec</button>
          <button onClick={inc}>Inc</button>
        </div>

        <div className="button-row">
          <button onClick={undo} disabled={!App.CanUndo(h)}>
            Undo
          </button>
          <button onClick={redo} disabled={!App.CanRedo(h)}>
            Redo
          </button>
        </div>
      </div>

      <p className="info">
        React owns rendering, Dafny owns state transitions.
        <br />
        The invariant (value &gt;= 0) is verified at compile time.
      </p>
    </>
  )
}

export default MyApp

The pattern is straightforward:

useState holds the Dafny History object (past, present, future).
Every user action calls an App.* function and replaces the history with the result.
App.Present(h) extracts the current Model value for rendering.
App.CanUndo(h) and App.CanRedo(h) drive the disabled state of the history buttons.

Run the app

cd my-app
npm run dev

Open http://localhost:5173 in your browser. You have a running React app with a Dafny-verified state machine:

Click Inc to increment — the value increases.
Click Dec to decrement — the value decreases, but never below zero (the invariant is enforced by Normalize).
Click Undo and Redo to move through history — the invariant holds at every step.

What you proved

By completing this guide you discharged two proof obligations:

Obligation	What it means
`Inv(Init())`	The initial state `0` satisfies `m >= 0`
`Inv(m) ⇒ Inv(Normalize(Apply(m, a)))`	Every transition, after normalization, preserves non-negativity

The Replay kernel then guarantees:

Do preserves the invariant — every new action lands in a valid state.
Undo and Redo preserve the invariant — history navigation cannot produce an invalid state.
Every state in past and future satisfies the invariant — the full history is clean.

Next steps

Domain obligations

Learn the full contract for plugging a domain into any of the five kernels.

dafny2js tool

Explore all CLI options and the generated bundle structure.

React integration guide

Patterns for wiring the verified kernel into more complex React apps.

Kanban app

A non-trivial domain: ordered columns, drag-and-drop, WIP limits, and undo/redo.

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Quickstart: Build a Verified React App Using Dafny

Architecture overview

Steps

What you proved

Next steps

Domain obligations

dafny2js tool

React integration guide

Kanban app

Build docs developers (and LLMs) love

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Documentation Index

​Architecture overview

​Steps

​What you proved

​Next steps

Domain obligations

dafny2js tool

React integration guide

Kanban app

Build docs developers (and LLMs) love

Architecture overview

Steps

What you proved

Next steps