LemmaScript — The Supported TypeScript Subset

A friendly tour of which TypeScript you can write and have verified. For the precise translation rules, see Specification; for a hands-on walkthrough, Getting started in an existing codebase.

The idea in one minute

You write ordinary TypeScript and add //@ comments that state what your code should do. The lsc tool reads the TypeScript, translates the parts it understands into a prover’s language (Dafny or Lean 4), and the prover checks that your code actually meets the spec.

// Clamp a number into [lo, hi].
export function clamp(x: number, lo: number, hi: number): number {
  //@ verify
  //@ requires lo <= hi
  //@ ensures lo <= \result && \result <= hi
  if (x < lo) return lo;
  if (x > hi) return hi;
  return x;
}

The function body is plain TypeScript that runs unchanged. The //@ lines are the contract — invisible at runtime, checked by the prover. Nothing here is a custom dialect: it’s a subset of TypeScript, plus comment annotations.

Two things shape what you can verify:

1. What TypeScript constructs lsc understands — the subject of this document.
2. What you can say in //@ annotations — the spec language, covered in SPEC.md §2.

Backends differ. Both Dafny and Lean are supported, but Dafny currently understands a wider set of library methods (most string/array helpers below are Dafny-only). Where it matters, SPEC.md has a per-backend column. When in doubt, target Dafny.

Types you can use

You write	Modeled as	Notes
number	integer	Maps to int by default. Add //@ type nat for a non-negative integer.
number (non-integer literal)	real	0.8, 3.14 become reals; mixed int/real arithmetic coerces automatically.
bigint	integer	Same as number; 32n, 0xffffn literals supported, exact past 2^53.
boolean	bool
string	string
T[] / Array<T> / readonly T[]	sequence
[A, B, ...] (heterogeneous tuple)	tuple	Native tuple ((A, B) / A × B). Access needs a literal index (t[0], t[1]); const [a, b] = t works.
[T, T, ...] (homogeneous tuple)	sequence	Same-typed elements model as a seq (more capable than a fixed tuple).
Map<K, V> / Record<K, V>	map
Set<T>	set
T | undefined, T | null	optional	undefined and null model identically.
user type / interface	generated datatype	Records and unions — see Modeling data.
<T extends Base>	generic	Type parameter erased to its bound; .map/.filter etc. work over it.
(a: T) => R	function value	Used for higher-order params and lambdas.

User-defined types referenced from a verified function are pulled in automatically, recursively, even across files. You don’t redeclare them.

Values, operators, literals

All the usual operators carry over with their normal meaning: === !== < <= > >= + - * / % && || ! and the ternary c ? a : b. number / number is real division (matching JS: 3 / 2 === 1.5); for an integer quotient use Math.floor(a / b). bigint / bigint is integer division.

Supported literal forms include number/bigint/hex literals, string and template literals (`${n} items` concatenates), array literals with spread ([...xs, e]), object literals with spread ({ ...obj, f: v }), and Record/Map object literals.

A handful of Math.* helpers are understood: abs, min, max, floor, ceil (and Math.max(...arr) over an array).

Control flow

Construct	Supported?
if / else if / else	✅
while	✅ — annotate with //@ invariant and //@ decreases
for (let i = ...; ...; i++)	✅ — desugared to a while
for (const x of xs)	✅ — over arrays, sets, Object.entries/values
switch on a discriminant	✅ — becomes a match
if-chain on a .tag field	✅ — also becomes a match
break	✅ — add //@ done_with to say what holds on exit
continue	✅
return inside a loop	✅ on Dafny; on Lean, restructure to break + a result variable
throw new Error(...)	✅ — modeled as an unreachable point; characterize valid input with //@ requires instead of relying on it

Loops are where most of the proof effort lives: a while or for usually needs a loop invariant. That’s expected — it’s the heart of what’s being verified.

Functions, generics, lambdas

Plain functions are the core unit. Parameters and the return type are read from your annotations. A function whose body is a single expression (or is recursive) becomes prover-level and spec-usable — you can mention it inside other //@ specs — so write predicate helpers as expression-bodied functions.

Generics work: <T extends Base> parameters, plus the higher-order array methods .map, .filter, .some, .every, .find, .findIndex with inline arrow functions. Lambdas passed to these get their parameter types inferred. Flat object-destructured lambda parameters are supported; array, nested, defaulted, and rest binding patterns are not.

async functions are supported only when they contain no await — the Promise<T> wrapper is just unwrapped to T. A real await / genuine async is not modelable.

Collections and their methods

Arrays, strings, maps, and sets all carry a useful slice of their standard library. A representative set (Dafny has the fullest coverage — see SPEC.md §3.2 for the exact list and any per-backend gaps):

• Array — .length, indexing a[i], .map, .filter, .some, .every, .includes, .indexOf, .find, .findIndex, .slice, .concat, .flat, .join, .shift, .pop, immutable update a.with(i, v) (and a[i] = v), spread [...a, x].
• String — .length, indexing, .slice, .substring, .indexOf, .includes, .startsWith, .endsWith, .split, .trim/.trimStart/.trimEnd, .toLowerCase/.toUpperCase, .charCodeAt.
• Map / Record — .get (returns optional in code, direct in specs), .set, .has, .delete, .size, in, object-literal construction, Object.entries/values/fromEntries.
• Set — .add, .delete, .has, .size, in, iteration.

Indexing into an array under noUncheckedIndexedAccess yields an optional element, matching TypeScript’s own typing.

Modeling data

Two shapes cover most domain modeling, and both translate directly:

Records — an object type becomes a single-constructor datatype with the same fields:

type Point = { x: number; y: number };

datatype Point = Point(x: int, y: int)

Discriminated unions — a union of objects sharing a literal tag becomes a sum type, and you branch on it with switch or an if-chain on the tag:

type Result =
  | { tag: "ok"; value: number }
  | { tag: "error"; message: string };

datatype Result = ok(value: int) | error(message: string)

A switch/if-chain on result.tag becomes a match, and a spec that conditions on a variant uses the constructor test — result.tag === "ok" reads as result.ok? in Dafny.

A bare string-literal union (type State = "idle" | "running") becomes an enum: comparisons like s === "idle" and using "running" as a value both work.

datatype State = idle | running

The annotation layer (the other half)

The //@ comments are where you say what to prove. The common ones:

• //@ requires P — a precondition the caller must meet.
• //@ ensures P — a postcondition the function guarantees (use \result for the return value).
• //@ invariant P / //@ decreases D — on loops.
• //@ verify — opt this function in (once any function in a file is marked, only marked functions are verified).

The spec expressions support quantifiers (forall(k, P), exists(k, P)), implication (==>), and the same operators and method calls as code. The full language — including ghost state, //@ havoc, //@ extern, and selective verification — is SPEC.md §2.

Where to go next

• Getting started in an existing codebase — clone a working example and run the edit loop.
• Specification — the precise annotation language and translation rules.
• examples/ — small, complete, verified LemmaScript files.
• Case studies & examples — the case studies, from string helpers to full verified apps.