Lemmascript

LemmaScript formal verification for TypeScript

LemmaScript is a verification toolchain for TypeScript. Ordinary TypeScript carries //@ specification comments; the lsc CLI generates formal artefacts that a backend prover (Dafny, or Lean via Velvet/Loom) checks. The annotations are comments — invisible to tsc, bundlers, and the runtime — and the annotated TypeScript source remains the shipped production code. LemmaScript verifies a formal model of that source; proofs apply only within the supported TypeScript fragment and documented modelling assumptions. See references/annotations.md for semantic limits: number uses mathematical-integer rather than IEEE-754 semantics, Map/Record values can differ at runtime, lifted method calls lose JavaScript short-circuit behaviour, and cross-file calls are axiomatized rather than body-verified. UI/I/O/auth/clock/adapter code is trusted unless separately covered. Think "Verus is to Rust as LemmaScript is to TypeScript".

Where fast-check samples inputs and can only find bugs, LemmaScript proves properties for every input. It costs far more effort per property, so reserve it for load-bearing logic; use the fast-check skill for the broad regression net beneath the proofs.

When to apply

Apply when a property must hold unconditionally and a violation is severe: invariant preservation across a state machine's actions, conservation ("money never leaks"), soundness and completeness of a decision procedure, security predicates (path-traversal containment, open-redirect exclusion, permission-gate correctness), parser conservation, or bounded-resource guarantees (no overbooking, rate-limit bounds).

Do not apply to code outside the supported fragment (heavy async, this-dispatch, closures over mutable state, regex, real I/O), to float-sensitive numerics (the model treats number as a mathematical integer), or when a sampled property-based test gives sufficient confidence — proofs are expensive to write and to maintain.

Installation and prerequisites

Node.js ≥ 18. Dafny ≥ 4.x for the primary backend; elan plus the Loom/Velvet forks for the Lean backend.

npm install lemmascript@0.5.22

For brownfield work, clone LemmaScript as a sibling of the target project and invoke it from source (npx tsx ../LemmaScript/tools/src/lsc.ts ...) — it is a tech preview, and the cleanest fix for a gap is sometimes in the toolchain itself. The midspiral/hono-lemmascript repository is a complete worked example with annotations, generated Dafny, proofs, and CI.

Core concepts

Annotate the function, then generate and verify:

export function firstIndexOf(arr: number[], target: number): number {
  //@ verify
  //@ requires arr.length > 0
  //@ ensures \result >= -1 && \result < arr.length
  //@ ensures \result === -1 ==> forall(k: nat, k < arr.length ==> arr[k] !== target)
  //@ ensures \result >= 0 ==> arr[\result] === target
  //@ ensures \result >= 0 ==> forall(k: nat, k < \result ==> arr[k] !== target)
  let i = 0;
  while (i < arr.length) {
    //@ invariant 0 <= i && i <= arr.length
    //@ invariant forall(k: nat, k < i ==> arr[k] !== target)
    //@ decreases arr.length - i
    if (arr[i] === target) return i;
    i = i + 1;
  }
  return -1;
}

npx --yes --package=lemmascript@0.5.22 -- lsc gen   --backend=dafny src/find.ts   # generate artefacts
npx --yes --package=lemmascript@0.5.22 -- lsc check --backend=dafny src/find.ts   # generate + verify
npx --yes --package=lemmascript@0.5.22 -- lsc regen --backend=dafny src/find.ts   # regenerate, 3-way merge

Key pieces:

• //@ verify opts a function in; once any function in a file has it, only marked functions are extracted.
• //@ requires / //@ ensures are the contract; \result names the return value; ==> is implication; forall(k, P) / exists(k, P) quantify.
• //@ invariant and //@ decreases go at the top of the loop body.
• Pure functions (no loops, no mutation) are callable from other functions' specs; //@ pure forces the classification.
• Unmodellable calls are handled by //@ extern (deterministic axiom), //@ havoc (nondeterministic value), or file-level //@ autohavoc (abstract everything unmodellable, soundly).

The complete annotation surface, the spec expression language, and the semantic gotcha list live in references/annotations.md.

The edit loop (Dafny backend)

lsc gen produces two files beside the source: foo.dfy.gen (always regeneratable — never edit) and foo.dfy (source of truth — add helper lemmas, ghost predicates, assert nudges here). The diff between them must be additions only; lsc check enforces this. After editing the TypeScript, run regen (never delete and gen fresh — that discards every proof). When Dafny complains, the fix belongs either in the .ts (tighten requires, weaken ensures, add invariant/decreases) or in the .dfy (helper lemma, ghost predicate, assert).

The full workflow — backend choice, Lean's four-file scheme, proof debugging flags, CI wiring, and brownfield strategy — lives in references/workflow.md.

Anti-patterns

• Reaching for //@ assume to silence a failure. It tells the prover to trust the obligation unconditionally; the proof stops meaning anything. Restructure, or prove a helper lemma. Its one sanctioned use is constraining a deliberately havoced value.
• Refactoring production code "for clarity" during brownfield verification. In-place verification is the point; an unchanged diff is the evidence the verified code is the shipped code.
• Editing .dfy.gen. It is regenerated; changes vanish. Edit the .dfy.
• Deleting .dfy files to "start clean". Proof work lives there; regen's three-way merge preserves it.
• Verifying a parallel model instead of the real function. Prefer in-place annotation; where a type can't be imported, shadow it with //@ declare-type so the actual function stays the proof target.
• Proving what the spec doesn't say. Write the //@ contract intent line and check the ensures actually expresses it — a theorem about the wrong predicate verifies happily.

Project integration

• State the trust boundary in the README: which functions are proved, and which surrounding layers (UI, I/O, auth, clock) are trusted. Case studies do this plainly; follow suit.
• Track verified files in LemmaScript-files.txt (one file per line, optional per-file timeout and flags) so tools/check.sh and CI verify them; copy hono-lemmascript's GitHub Actions workflow as the template.
• Start small in brownfield code: pure helpers, predicates, parsers without I/O. Grow towards the invariant-bearing core.
• Keep fast-check properties alongside proofs. They run in the inner loop in milliseconds, catch spec regressions before a prover run, and cover the unverified boundary code.
• Land toolchain fixes separately. When the tech preview needs a patch (unsupported method, missed narrowing), fix LemmaScript/tools/src/ in its own PR.

Hard-won lessons

• The spec is the product. Provers check the written specification, not the intended one. Review ensures clauses as adversarially as code.
• number is a mathematical integer in the model (floats become real; overflow at 2^53 is out of scope). Do not verify float-sensitive numerics; do flag integer-encoding overflow risks — a case study's injectivity proof surfaced a real ≥1000-votes overflow in an existing encoding.
• Missing invariants live in the TypeScript. The LLM/prover loop can supply tactics and lemmas in the .dfy, but a missing //@ invariant must be added in the source and regenerated.
• Refinement scales. For loop-heavy code, prove the method equals a pure recursive spec (result == range_spec(...)), then prove properties of the spec — every property transfers automatically.
• Verification conditions are cheap to split. dafny verify --filter-symbol=... and --isolate-assertions turn one opaque timeout into named, tractable obligations.

References

• LemmaScript repository — SPEC.md, DESIGN.md, GETTING_STARTED.md, AGENTS.md, examples.
• Announcement post and lemmascript.com.
• Worked case studies: hono-lemmascript (brownfield, CVE-driven), clear-split-lemmascript (greenfield, dual-backend), collab-todo-lemmascript (verified domain model behind a React app).
• references/annotations.md for the annotation surface, spec language, and gotchas.
• references/workflow.md for the edit loop, backends, CI, and brownfield strategy.
• Sampled-input testing as the complementary adversary lives in ../fast-check/SKILL.md.