Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/metareflection/dafny-replay/llms.txt

Use this file to discover all available pages before exploring further.

The dafny2js tool bridges the gap between verified Dafny code and idiomatic JavaScript. You point it at your .dfy file, tell it which module is your public AppCore, and it generates an app.js (or app.ts) file that wraps every function in the AppCore module with proper type conversions. The result is a module you can import directly into React components — no manual BigNumber coercion, no __default prefixes, no hand-written Dafny-to-JS glue code.

​
The compilation pipeline

Generating a JavaScript API from Dafny takes two distinct steps: Dafny’s own compiler, and then dafny2js. 
MyAppDomain.dfy
      │
      ▼
dafny translate js          # Step 1: Dafny → raw CJS bundle
      │
      ▼
MyApp.cjs                   # Dafny runtime + generated JS (do not edit)
      │
      ▼
dafny2js                    # Step 2: read .dfy + .cjs → typed wrapper
      │
      ▼
app.js (or app.ts)          # Clean ESM module ready for Vite/React
1

Compile Dafny to JavaScript

Run the Dafny compiler to produce a CommonJS bundle that includes the Dafny runtime and your compiled modules:
dafny translate js \
  --no-verify \
  -o generated/MyApp \
  --include-runtime \
  MyAppDomain.dfy
Copy the output to your app’s source tree:
cp generated/MyApp.js my-app/src/dafny/MyApp.cjs
The .cjs extension tells Vite to treat it as CommonJS (which the Dafny compiler emits).
2

Run dafny2js

Point dafny2js at the .dfy source (for type information) and tell it the name of the CJS bundle and the AppCore module:
dotnet run --project dafny2js -- \
  --file MyAppDomain.dfy \
  --app-core AppCore \
  --cjs-name MyApp.cjs \
  --output my-app/src/dafny/app.js
dafny2js reads the .dfy file to understand your Model, Action, and History types, then emits a fully typed wrapper that loads the .cjs bundle at runtime.

​
CLI flags

FlagRequiredDescription
--file <path>YesPath to the .dfy source file. Used for type analysis.
--app-core <name>YesName of the module to wrap (e.g., AppCore).
--cjs-name <name>YesFilename of the compiled .cjs bundle (e.g., MyApp.cjs).
--output <path>YesOutput path for the generated wrapper file.
--clientNoEmit Vite-compatible client code (default). Uses ?raw import and new Function loader.
--denoNoEmit Deno-compatible server code. Uses readFileSync-style loading.
--null-optionsNoEmit TypeScript with T | null option types instead of strict non-null types.
--client and --deno are mutually exclusive. The default behavior (--client) generates code that works in Vite via the ?raw import and a new Function evaluator. Use --deno for server-side edge functions.

​
What app.js contains

The generated app.js has five sections.

​
1. BigNumber setup and module loading

import BigNumber from 'bignumber.js';
BigNumber.config({ MODULO_MODE: BigNumber.EUCLID });

import dafnyCode from './MyApp.cjs?raw';

const require = (mod) => {
  if (mod === 'bignumber.js') return BigNumber;
  throw new Error(`Unknown module: ${mod}`);
};

const initDafny = new Function('require', `
  ${dafnyCode}
  return { _dafny, MyAppDomain, MyAppKernel, AppCore };
`);

const { _dafny, MyAppDomain, MyAppKernel, AppCore } = initDafny(require);
The ?raw import tells Vite to load the file as a string. The new Function trick evaluates the CommonJS bundle in a scope where require('bignumber.js') resolves correctly. This is the only supported pattern for loading Dafny-compiled code in a Vite/ESM environment.

​
2. Type converters (toJson / fromJson)

For each datatype in your domain, dafny2js emits bidirectional converters between JavaScript values and Dafny runtime objects: 
// Action: Dafny datatype ↔ plain string
const actionFromJson = (json) => {
  switch (json) {
    case 'Inc': return MyAppDomain.Action.create_Inc();
    case 'Dec': return MyAppDomain.Action.create_Dec();
    default: throw new Error(`Unknown Action: ${json}`);
  }
};

const actionToJson = (value) => {
  if (value.is_Inc) return 'Inc';
  if (value.is_Dec) return 'Dec';
  throw new Error('Unknown Action variant');
};

// History: Dafny History record ↔ { past, present, future }
const historyFromJson = (json) => {
  return MyAppKernel.History.create_History(
    _dafny.Seq.of(...(json.past || []).map(x => new BigNumber(x))),
    new BigNumber(json.present),
    _dafny.Seq.of(...(json.future || []).map(x => new BigNumber(x)))
  );
};

const historyToJson = (value) => ({
  past:    [...value.dtor_past].map(x => x.toNumber()),
  present: value.dtor_present.toNumber(),
  future:  [...value.dtor_future].map(x => x.toNumber()),
});

​
3. Action constructors

Each datatype constructor gets a zero-argument factory function (for constructors with no fields) or an argument-accepting wrapper that converts JS types to Dafny types before calling the underlying constructor. 
const App = {
  Inc: () => MyAppDomain.Action.create_Inc(),
  Dec: () => MyAppDomain.Action.create_Dec(),
  ...
};

​
4. AppCore function wrappers

Every function in your AppCore module gets a wrapper that accepts and returns JavaScript-friendly values: 
Init:     ()          => AppCore.__default.Init(),
Dispatch: (h, a)      => AppCore.__default.Dispatch(h, a),
Undo:     (h)         => AppCore.__default.Undo(h),
Redo:     (h)         => AppCore.__default.Redo(h),
Present:  (h)         => toNumber(AppCore.__default.Present(h)),
CanUndo:  (h)         => AppCore.__default.CanUndo(h),
CanRedo:  (h)         => AppCore.__default.CanRedo(h),
Note that Present converts the returned BigNumber to a plain JavaScript number automatically.

​
5. Converter exports and internal access

const App = {
  // ... all the above

  // Converters for network serialization
  actionToJson,
  actionFromJson,
  historyToJson,
  historyFromJson,

  // Raw internal modules for app-extras.js
  _internal: { _dafny, MyAppDomain, MyAppKernel, AppCore },
};

export default App;
The _internal object gives app-extras.js access to the raw Dafny modules when you need to call functions outside the AppCore surface or build custom converters.

​
Using app.js in a component

After running the pipeline, import App from the generated file and call its functions directly: 
import App from './dafny/app.js';

// Create the initial history
const h = App.Init();

// Dispatch an action — returns a new history
const h2 = App.Dispatch(h, App.Inc());

// Read the current state as a plain JS number
const value = App.Present(h2);  // → 1

// Check undo/redo availability
App.CanUndo(h2);  // → false (no past states yet)
App.CanRedo(h2);  // → false

// Serialize for storage or network
const json = App.historyToJson(h2);
// → { past: [], present: 1, future: [] }
Never edit app.js by hand. It is regenerated every time you run dafny2js. Add customizations in a separate app-extras.js file that imports from app.js.

​
TypeScript output

Pass --output app.ts to generate a TypeScript file instead. The generated TypeScript includes explicit type definitions for the JSON representation of each datatype: 
export type Action = 'Inc' | 'Dec';

export interface History {
  past: number[];
  present: number;
  future: number[];
}
These types describe the plain-JS shapes used in toJson/fromJson, not the internal Dafny runtime objects. React components can import them for prop types and state annotations.

React integration

Load the generated app.js in Vite and wire it into React state.

app-extras.js pattern

Layer customizations on top of the generated API without modifying generated files.

Build docs developers (and LLMs) love

Get started for freeTalk to us