Dafny for TypeScript developers

Dafny is a programming language with a checker built in. Next to the code you write what the function needs (requires) and what it promises (ensures). Dafny proves the promise holds for every input, and only then compiles the code. It can compile to JavaScript, so the code you proved is the code you ship.

This page shows how to use it inside a normal TypeScript project, with one small example. No Dafny experience needed: a coding agent can write the Dafny, and the verifier checks every line of it.

Write a function in Dafny with its promises, prove them for every input, and compile it to JavaScript for your TS code.

Why you would want this

Both tests pass, but indexOfId([10, 20, 30], 10) returns -1.

Here is a normal binary search over sorted ids, and two normal tests:

Note: indexOfId is pure from the outside (same inputs, same output, no side effects), but it loops over mutable local variables inside. Dafny proves that as written.

src/ids.ts

export function indexOfId(ids: readonly number[], target: number): number {
  let lo = 0;
  let hi = ids.length - 1;
  while (lo < hi) {
    const mid = Math.floor((lo + hi) / 2);
    if (ids[mid] < target) lo = mid + 1;
    else if (ids[mid] > target) hi = mid - 1;
    else return mid;
  }
  return -1;
}

src/ids.test.ts

test('finds an id', () => {
  expect(indexOfId([10, 20, 30], 20)).toBe(1);
});

test('returns -1 for a missing id', () => {
  expect(indexOfId([10, 20, 30], 25)).toBe(-1);
});

Both tests pass. The function still has a bug: indexOfId([10, 20, 30], 10) returns -1, and so does indexOfId([10, 20, 30], 30). When the search narrows down to one last element, the loop stops before looking at it. Binary search is famous for bugs like this. They hide at the edges, where tests rarely look.

When Dafny fits

• Code with loops and indexes, where off-by-one mistakes are easy: search, merge, pagination, ring buffers, parsers, diffing.
• Code where “it returns the right thing” can be said precisely: “if it returns an index, the id is there; if it returns -1, the id is nowhere in the list”.
• You want the checked code to be the shipped code, not a copy of it.

Dafny is not the tool for “what happens when two requests arrive at the same time”. That is about the order of events, not one function. See the Quint page for that.

Install

Dafny 4 comes with .NET 8 and Z3.

brew install dafny    # Dafny 4, with .NET 8 and Z3
npm i bignumber.js    # the generated JavaScript needs it at runtime

On Linux and Windows, see the install page.

Step 1: write the function in Dafny, with its rules (use AI)

requires is what callers guarantee; ensures is what the function promises.

The Dafny version looks a lot like TS. The new parts are the lines between the signature and the body:

dafny/Search.dfy

newtype int53 = x: int | -0x20_0000_0000_0000 < x < 0x20_0000_0000_0000  // compiles to a plain JS number

method IndexOf(ids: seq<int53>, target: int53) returns (index: int53)
  requires |ids| < 0x20_0000_0000_0000
  requires forall i, j :: 0 <= i < j < |ids| ==> ids[i] < ids[j]      // the caller promises: sorted, no duplicates
  ensures 0 <= index ==> index as int < |ids| && ids[index] == target  // a found index points at the target
  ensures index < 0 ==> target !in ids                                // -1 means the id is not in the list
{
  var lo: int53 := 0;
  var hi: int53 := |ids| as int53 - 1;
  while lo < hi {
    var mid := (lo + hi) / 2;
    if ids[mid] < target {
      lo := mid + 1;
    } else if ids[mid] > target {
      hi := mid - 1;
    } else {
      return mid;
    }
  }
  return -1;
}

Run the verifier:

Three errors. Each one points at a line:

1. lo + hi might go past the int53 range. In JS this means going past Number.MAX_SAFE_INTEGER, where numbers silently lose precision. The standard fix is lo + (hi - lo) / 2, which can never be bigger than hi.
2. ids[mid] might be out of range. Dafny does not know yet that mid stays inside the list.
3. return -1 might break the promise “the id is not in the list”.

Step 2: tell Dafny what stays true in the loop

With loop invariants, only the real bug is left.

Dafny checks a loop one pass at a time. To do that it needs to know what is true at the start of every pass. That is a loop invariant. For binary search it is the same thing you would say to explain the code to a colleague:

• lo and hi stay within the list.
• Everything before lo is smaller than the target.
• Everything after hi is bigger than the target.

Before the fix Diff With the fix

newtype int53 = x: int | -0x20_0000_0000_0000 < x < 0x20_0000_0000_0000
method IndexOf(ids: seq<int53>, target: int53) returns (index: int53)
  requires |ids| < 0x20_0000_0000_0000
  requires forall i, j :: 0 <= i < j < |ids| ==> ids[i] < ids[j]
  ensures 0 <= index ==> index as int < |ids| && ids[index] == target
  ensures index < 0 ==> target !in ids
{
  var lo: int53 := 0;
  var hi: int53 := |ids| as int53 - 1;
  while lo < hi {
    var mid := (lo + hi) / 2;
    invariant 0 <= lo as int <= |ids| && -1 <= hi as int < |ids|
    invariant forall i :: 0 <= i < lo as int ==> ids[i] < target
    invariant forall i :: hi as int < i < |ids| ==> ids[i] > target
  {
    var mid := lo + (hi - lo) / 2;
    if ids[mid] < target {
      lo := mid + 1;
    } else if ids[mid] > target {
      hi := mid - 1;
    } else {
      return mid;
    }
  }
  return -1;
}

Dafny checks that each invariant is true before the loop and stays true after every pass. You do not have to prove that by hand; the verifier does it. Run it again:

The range errors are gone. One error is left, and it is the real bug. When the loop ends, the invariants say “everything before lo is too small, everything after hi is too big”. With while lo < hi, the loop can end with lo == hi, and that one element was never checked. So Dafny cannot prove “the id is not in the list” at return -1. It is right: the id might be exactly there.

Step 3: fix it

while lo <= hi fixes it: 0 errors, for every sorted list and every target.

Keep looping while there is still something to check:

Before the fix Diff With the fix

newtype int53 = x: int | -0x20_0000_0000_0000 < x < 0x20_0000_0000_0000
method IndexOf(ids: seq<int53>, target: int53) returns (index: int53)
  requires |ids| < 0x20_0000_0000_0000
  requires forall i, j :: 0 <= i < j < |ids| ==> ids[i] < ids[j]
  ensures 0 <= index ==> index as int < |ids| && ids[index] == target
  ensures index < 0 ==> target !in ids
{
  var lo: int53 := 0;
  var hi: int53 := |ids| as int53 - 1;
  while lo <= hi
    invariant 0 <= lo as int <= |ids| && -1 <= hi as int < |ids|
    invariant forall i :: 0 <= i < lo as int ==> ids[i] < target
    invariant forall i :: hi as int < i < |ids| ==> ids[i] > target
  {
    var mid := lo + (hi - lo) / 2;
    if ids[mid] < target {
      lo := mid + 1;
    } else if ids[mid] > target {
      hi := mid - 1;
    } else {
      return mid;
    }
  }
  return -1;
}

0 errors means both promises hold for every sorted list and every target, of any length.

Dafny also proves that the loop always ends. Change lo := mid + 1 to lo := mid, a common mistake, and it says so:

In TS that version hangs forever for some inputs. Here it does not compile.

Step 4: compile to JavaScript and use it from TS

dafny translate js verifies, then writes plain JavaScript; a typed wrapper imports it into TS.

Add a script to package.json:

"scripts": {
  "dafny": "dafny translate js --include-runtime dafny/Search.dfy -o generated/search && echo 'module.exports = _module;' >> generated/search.js && mv generated/search.js generated/search.cjs"
}

dafny translate js verifies first. If there is any error, it stops and writes nothing.

The generated JavaScript has no types, so give it a two-line declaration file next to it. You write it once; the Dafny build leaves it alone:

generated/search.d.cts

declare const search: { __default: { IndexOf(ids: readonly number[], target: number): number } };
export = search;

Then src/ids.ts becomes one import and one line:

src/ids.ts

import search from '../generated/search.cjs';

export const indexOfId = (ids: readonly number[], target: number): number => search.__default.IndexOf(ids, target);

The rest of the app imports indexOfId exactly as before.

Add the edge cases to the tests:

test('finds the first and the last id', () => {
  expect(indexOfId([10, 20, 30], 10)).toBe(0);
  expect(indexOfId([10, 20, 30], 30)).toBe(2);
});

test('empty list', () => {
  expect(indexOfId([], 10)).toBe(-1);
});

Against the old TS function, the new test fails:

Against the Dafny build, all pass:

You still keep a few tests. They check the wiring (the wrapper, the export line, the import path), not the logic.

Project layout and CI

Commit generated/. CI verifies, regenerates it and fails on any difference.

One repo. The Dafny source sits in its own folder, and the JavaScript it produces is committed next to it:

./
├── .github/workflows/ci.yml
├── dafny/
│   └── Search.dfy               the code, with requires / ensures / invariants
├── generated/
│   ├── search.cjs               built from Search.dfy, committed, never edited by hand
│   └── search.d.cts             its types, written once by hand
├── src/
│   ├── ids.ts                   typed wrapper, the only file that imports generated/
│   └── ids.test.ts              tests for the wiring and a few edge cases
├── .gitignore                   node_modules, generated/*.dtr
├── package.json
└── tsconfig.json

Why commit generated/:

• The app builds, runs and deploys with plain Node. Only the people who change dafny/ need Dafny installed.
• The generated file shows up in code review, so a change in behavior is visible as a diff.
• CI can check that the committed file really comes from the committed, verified source. The build is repeatable: the same .dfy file gives the same .cjs file, byte for byte.

Scripts and dependencies in package.json:

"scripts": {
  "dafny": "dafny translate js --include-runtime dafny/Search.dfy -o generated/search && echo 'module.exports = _module;' >> generated/search.js && mv generated/search.js generated/search.cjs",
  "typecheck": "tsc",
  "test": "vitest run"
},
"dependencies": {
  "bignumber.js": "^11.1.5"
}

bignumber.js is a normal dependency, not a dev one: the generated code loads it at runtime.

The CI workflow has two jobs:

The CI workflow: .github/workflows/ci.yml (32 lines)

.github/workflows/ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  dafny:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: dafny-lang/setup-dafny-action@v1
        with:
          dafny-version: "4.11.0"
      - name: Verify and regenerate the JavaScript
        run: npm run dafny
      - name: generated/ matches the verified Dafny code
        run: git diff --exit-code generated/

  ts:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: actions/setup-node@v7
        with:
          node-version: 24
          cache: npm
      - run: npm ci
      - run: npm run typecheck
      - run: npm test

What fails when:

Change	Where CI fails
A change to Search.dfy that Dafny cannot prove	dafny job, npm run dafny: the verifier error, no JavaScript written
Search.dfy changes, generated/ is not rebuilt	dafny job, git diff: the committed JavaScript is stale
Someone edits generated/search.cjs by hand	dafny job, git diff: the rebuild overwrites the edit
The wrapper or the import path breaks	ts job, tsc or ids.test.ts

Making changes

Change the ensures first, then the body; regenerate and commit both.

Changing the search (for example, returning the insert position instead of -1):

1. Change the ensures lines first. They are the new promise, and the reviewer reads them before the code.
2. Change the body. Run npm run dafny until it verifies. If a loop fails, update the invariant: it should still be a sentence you can say out loud.
3. Update the types in generated/search.d.cts if the signature changed, and the tests that check the wiring.
4. Commit Search.dfy, generated/ and src/ together.

Adding a function: add it to the same .dfy file (or include a new one), export it through the wrapper, regenerate. One wrapper file per generated file keeps the untyped code in one place.

Reviewing a pull request: read the .dfy diff, starting with requires and ensures. Skim generated/. Its diff only confirms the rebuild happened, and CI has already checked that it matches.

Strengths

• Shipped code is the proven code. The JavaScript is compiled from the .dfy file, so no hand-made copy can drift.
• Proven for every input. Index access in range, loops that end, and every ensures hold for all inputs.
• Assumptions are written down. Hidden assumptions become requires lines that the next developer can read.

Limitations

• requires is not checked at runtime. A TS caller can still pass an unsorted list. Check it once where the list is built.
• Generated JavaScript. The output is readable but not hand-written. You edit the .dfy file, not the output.
• Loop invariants take effort. Writing them is the main skill to learn. A failed invariant points at a line, which helps.
• One function at a time. Dafny does not cover timing, concurrency, I/O or the order of events between services.

How to start in your own project

1. Pick one small function with loops or index math, where a mistake is expensive.
2. Write its promise as one sentence, then as ensures.
3. Write what callers must guarantee as requires.
4. Use limited number types like int53 so the output uses plain JS numbers.
5. When a loop fails to verify, write down what stays true on every pass. That is your invariant.
6. Add the dafny script, commit the generated folder, and wrap it with a typed TS function.

Related

• LemmaScript: writes the contracts as comments in the TS file and translates the function to Dafny or Lean for you, so you keep writing TypeScript.
• Dafny getting started
• Dafny reference manual
• Program Proofs, by Dafny’s creator, K. Rustan M. Leino: the book for programmers.