LemmaScript

LemmaScript is a verification toolchain for TypeScript, currently a tech preview. Its lsc command translates your TypeScript into Dafny source code by fixed rules, one TypeScript construct to one Dafny construct, with no LLM. Where Dafny cannot finish a proof on its own, an LLM adds loop invariants, lemmas and hints until it checks. The output stays close to human-written Dafny on purpose, because that is the Dafny LLMs learned from and are good at proving. It can also output Lean 4, through the Velvet and Loom libraries; that backend needs more setup and appears in fewer of their examples. This page uses Dafny.

LemmaScript turns //@ contract comments into Dafny proofs. Here: a bill split with a rounding bug.

Using LemmaScript

The code below is in formal-methods-samples/lemmascript-split-bill. We ran it with lsc 0.6.4 and Dafny 4.11.0. The output is from our run.

The problem

Rounding every share up can leave the last person with a negative share.

A bill in cents is split between people. Everyone pays the same share, rounded up so nobody underpays, and the last person pays what is left:

// splitBill.ts (shortened)
export function splitBill(total: number, people: number): Split {
  const each = Math.ceil(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

For 1,000 cents between 3 people it gives 334, 334 and 332, and the shares add up. But when the shares are small and there are many people, rounding up takes more than the whole bill before the last person is reached.

Install and set up

npm install -D lemmascript

Needs Node 18+ and Dafny 4+.

Writing the contract

//@ requires and //@ ensures state the contract inside the TS file.

A contract is a set of //@ comments inside the ordinary TypeScript. tsc and the bundler ignore them.

//@ verify
export function splitBill(total: number, people: number): Split {
  // What callers must pass.
  //@ requires total >= 0
  //@ requires people >= 1
  // What the function promises; \result is the return value.
  //@ ensures \result.each * (people - 1) + \result.last === total
  //@ ensures \result.last >= 0
  //@ ensures \result.each >= 0
  const each = Math.ceil(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

Running it

Dafny cannot prove last >= 0. One failing input: 20 people splitting 3.41.

lsc gen translates the file, and lsc check regenerates it and runs Dafny:

lsc gen --backend=dafny src/splitBill.ts
lsc check --backend=dafny src/splitBill.ts

The generated Dafny follows the TypeScript: the interface becomes a datatype, Math.ceil a helper over real numbers, and each //@ line a Dafny clause:

// splitBill.dfy (shortened)
function splitBill(total: int, people: int): Split
  requires (total >= 0)
  requires (people >= 1)
{
  var each := CeilReal(((total as real) / (people as real)));
  var last := (total - (each * (people - 1)));
  Split(each, last)
}

lemma splitBill_ensures(total: int, people: int)
  requires (total >= 0)
  requires (people >= 1)
  ensures (((splitBill(total, people).each * (people - 1)) + splitBill(total, people).last) == total)
  ensures (splitBill(total, people).last >= 0)
  ensures (splitBill(total, people).each >= 0)
{
}

Real output (paths shortened):

Generated: .../src/splitBill.dfy.gen
Running dafny verify...
splitBill.dfy(26,0): Error: a postcondition could not be proved on this return path
   |
26 | {
   | ^

splitBill.dfy(24,41): Related location: this is the postcondition that could not be proved
   |
24 |   ensures (splitBill(total, people).last >= 0)
   |                                          ^^

Dafny program verifier finished with 2 verified, 1 error

The exit code is 1, so the same command fails a CI job. The shares always add up (that holds by construction), but the last share can be negative. Dafny does not say for which input. One is 20 people splitting 3.41: each share is 0.18, and the last person is owed 0.01.

Fixing the bug

Round down with Math.floor. Proved for every input.

The fix: rounding down leaves the remainder for the last person, which is never negative:

Diff style

// Splits a bill in cents between people: everyone pays the same share, and the last person pays what is left.
export interface Split {
  each: number;
  last: number;
}

//@ verify
export function splitBill(total: number, people: number): Split {
  //@ requires total >= 0
  //@ requires people >= 1
  //@ ensures \result.each * (people - 1) + \result.last === total
  //@ ensures \result.last >= 0
  //@ ensures \result.each >= 0
  const each = Math.ceil(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

// Splits a bill in cents between people: everyone pays the same share, and the last person pays what is left.
export interface Split {
  each: number;
  last: number;
}

//@ verify
export function splitBill(total: number, people: number): Split {
  //@ requires total >= 0
  //@ requires people >= 1
  //@ ensures \result.each * (people - 1) + \result.last === total
  //@ ensures \result.last >= 0
  //@ ensures \result.each >= 0
  const each = Math.ceil(total / people);
  const each = Math.floor(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

// Splits a bill in cents between people: everyone pays the same share, and the last person pays what is left.
export interface Split {
  each: number;
  last: number;
}
//@ verify
export function splitBill(total: number, people: number): Split {
  //@ requires total >= 0
  //@ requires people >= 1
  //@ ensures \result.each * (people - 1) + \result.last === total
  //@ ensures \result.last >= 0
  //@ ensures \result.each >= 0
  const each = Math.ceilfloor(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

// Splits a bill in cents between people: everyone pays the same share, and the last person pays what is left.
export interface Split {
  each: number;
  last: number;
}

//@ verify
export function splitBill(total: number, people: number): Split {
  //@ requires total >= 0
  //@ requires people >= 1
  //@ ensures \result.each * (people - 1) + \result.last === total
  //@ ensures \result.last >= 0
  //@ ensures \result.each >= 0
  const each = Math.floor(total / people);
  const last = total - each * (people - 1);
  return { each, last };
}

Running dafny verify...

Dafny program verifier finished with 4 verified, 0 errors

Dafny proved the fixed function on its own, with no extra hints from us. For every bill total and every number of people, the shares add up to the total and nobody pays a negative amount. A test can only check the inputs it tries.

Project layout and CI

Commit the .ts, .dfy and .dfy.gen files. CI installs Dafny and runs lsc check.

./
├── .github/workflows/ci.yml
├── LemmaScript-files.txt          the files to prove, one per line
└── src/
    ├── splitBill.ts               the code, with //@ contracts
    ├── splitBill.dfy.gen          made by lsc from splitBill.ts
    └── splitBill.dfy              the .dfy.gen file plus any proof hints

All three files in src/ are committed. lsc regen needs the old .dfy.gen to merge a change into .dfy. CI needs Dafny; this example does not use Lean:

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

# .github/workflows/ci.yml (steps)
- run: npm ci
- uses: dafny-lang/setup-dafny-action@v1
  with:
    dafny-version: "4.11.0"
# With no file, lsc check proves every file in LemmaScript-files.txt. It exits 1 if a proof fails.
- run: npx lsc check --backend=dafny
- run: git diff --exit-code -- '*.dfy.gen'

What fails when:

A change breaks a promise: lsc check, with the ensures line Dafny could not prove.
The code changes and .dfy is not updated: lsc check. The .dfy file may only add lines to .dfy.gen.
The new .dfy.gen is not committed: git diff.

Making changes

Change the contract and the code, run lsc regen, fix what Dafny cannot prove, commit all three files.

If the promise changes, change the //@ lines first. Then change the code.
Run npx lsc regen --backend=dafny src/splitBill.ts. It writes a new .dfy.gen, merges it into .dfy, keeps your proof hints, and runs Dafny.
If Dafny cannot prove it, fix the code, or add hints to .dfy (you or an LLM). Only add lines; do not change the generated ones.
Commit the .ts, .dfy and .dfy.gen files together.

A new file goes into LemmaScript-files.txt, so CI proves it too.

Strengths

It proves the rule for every input. Rules over real-sized values, such as money that never goes missing or correct sums, are what a proof handles and a search over small values cannot.
It checks your real function. You add //@ comments to your TypeScript that say what the function needs and what it promises.
It shows what failed. When a proof fails, it names the promise that could not be proved, and where.

Limitations

Pure functions only. It does not cover the order of events, async jobs or I/O. For event order, TLA+, Quint or pnueli check every order in a model.
Your code is translated first. You install Dafny or Lean and trust the translation, and numbers behave like exact math, not JavaScript floating point.
Hard proofs need help. You may need an AI agent to write them.
Only part of TypeScript is supported. No real await: an async function works only if it never awaits. Classes work only with Dafny, and some of their proofs need hand edits in the generated Dafny. Callback parameters cannot use array, nested, default or rest destructuring. The Lean backend knows fewer array and string methods, and no return inside a loop. Everything else it supports is listed in its supported subset.
It is an early preview. Some gaps you may have to fix in LemmaScript itself. For production code today, writing the function in Dafny and compiling it to JavaScript is the more stable path; see Dafny.