Formal Proof Obligations in TypeScript: What LemmaScript and Dafny Actually Give You

TypeScript’s type system is genuinely impressive. Conditional types, template literal types, mapped types, discriminated unions, the infer keyword deep inside conditional branches: a determined developer can encode remarkable invariants purely in the type layer. But none of that is formal verification. It is type checking. The distinction matters more than the TypeScript community usually acknowledges, and that is the gap LemmaScript is trying to cross.

What Type Checking Cannot Prove

Consider a simple binary search implementation. TypeScript can tell you that the function accepts a sorted number[] and returns a number. It cannot tell you that the returned index is actually the correct position of the target value, or that the algorithm terminates on all inputs, or that it never reads out of bounds. These are properties about the values your program computes, not the shapes of data flowing through it.

Formal verification tools work at a different level. They generate proof obligations, logical formulas that must be true for your program to be correct, and then discharge those obligations using an automated theorem prover. When a verifier says your binary search is correct, it means an SMT solver has checked every possible execution path against your specification.

This is the domain Dafny has occupied since Rustan Leino introduced it at Microsoft Research around 2009. Dafny is a verification-aware language: you write code alongside preconditions, postconditions, loop invariants, and termination metrics, and the toolchain feeds proof obligations to Z3, Microsoft’s SMT solver. If Z3 cannot find a counterexample, your code is verified with respect to your specification.

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= index < a.Length ==> a[index] == key
  ensures index < 0 ==> key !in a[..]
{
  var lo, hi := 0, a.Length;
  index := -1;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant key !in a[..lo] && key !in a[hi..]
    decreases hi - lo
  {
    var mid := lo + (hi - lo) / 2;
    if a[mid] == key { index := mid; return; }
    else if a[mid] < key { lo := mid + 1; }
    else { hi := mid; }
  }
}

The requires clause is the precondition. The ensures clauses are postconditions. The invariant annotations tell Dafny what must hold at every loop iteration, and decreases hi - lo proves termination by giving a measure that strictly decreases. Z3 checks all of this statically, before any code ever runs.

How LemmaScript Bridges the Gap

LemmaScript builds a toolchain that lets TypeScript developers write Dafny specifications alongside their TypeScript code and have those specifications verified. The core insight is that Dafny already has a JavaScript and TypeScript compilation backend. Dafny programs can be compiled to TypeScript output, which means the verified Dafny code can coexist in a TypeScript project without a runtime penalty.

The workflow looks roughly like this: you write your algorithmic logic in Dafny, prove it correct there, and then either use the compiled TypeScript output directly or write TypeScript implementations that satisfy contracts enforced by the Dafny verification layer. The “lemma” in LemmaScript refers to Dafny’s lemma construct, which lets you state and prove mathematical facts about your program without those facts appearing in the runtime output at all.

lemma SortedArrayContainsOnce(a: seq<int>, x: int)
  requires x in a
  requires forall i, j :: 0 <= i < j < |a| ==> a[i] < a[j]
  ensures exists! i :: 0 <= i < |a| && a[i] == x
{
  // Dafny proves this automatically from the strict sorting invariant
}

Lemmas like this have no runtime representation. They are pure proof artifacts, checked by Z3 at compile time, that establish facts the rest of your verified code can rely on.

Comparison with Other Approaches

Formal verification for mainstream languages is not new, but it has mostly lived at the periphery. LiquidHaskell brought refinement types to Haskell, letting you annotate function signatures with logical predicates that the verifier checks. F*, developed at Microsoft Research and INRIA, takes this further with a full dependent type theory and is used to verify cryptographic implementations in Project Everest. Why3 provides a verification platform for OCaml and several other languages, also backed by SMT solvers.

The JavaScript ecosystem has had far less of this. There is TS-Proof and academic work on formalizing JavaScript’s semantics, but nothing that has reached everyday developer workflows. The gap is partly cultural: the JavaScript ecosystem optimizes for speed of iteration, and formal verification traditionally requires a significant investment in writing specifications before you get any benefit.

LemmaScript’s bet is that by reusing Dafny’s mature verification infrastructure and its existing TypeScript compilation path, the cost of entry is lower than building a verification system from scratch. You get Z3, Dafny’s proof search heuristics, its standard library of verified data structures, and years of refinement by researchers who have used it on real systems.

The Trade-offs Are Real

Formal verification always involves a specification problem. The SMT solver can only check that your code satisfies the spec you wrote. If the spec is wrong or incomplete, verification gives you a false sense of security. This is a genuine pitfall: a developer who writes a postcondition that is weaker than intended gets a green checkmark and still ships buggy code.

Dafny also has a learning curve. The loop invariant annotation discipline is non-trivial for developers unfamiliar with it. Z3 timeouts are a real operational concern for complex proofs: you write something that should be true, and the solver simply times out rather than returning either verified or counterexample. Tuning these situations requires understanding how Z3 reasons about quantifiers, which is specialized knowledge.

The integration story between verified Dafny code and unverified TypeScript is the other frontier. Real applications are mostly unverified. Calling verified Dafny-compiled TypeScript from ordinary TypeScript does not automatically extend the proofs across that boundary. You get verified behavior inside the Dafny module and unchecked behavior everywhere else. This is not a failure of LemmaScript specifically; it is the fundamental challenge of bringing formal methods into existing codebases, and it is the same problem seL4 faced in its C verification work and that the Rust Prusti project manages with its annotation-based approach.

Why This Is Worth Watching

The appeal of LemmaScript is not that it will suddenly make TypeScript codebases fully verified. It will not. The appeal is that it lowers the cost of verified-by-construction code in a language ecosystem that has had essentially none of this tooling. When you are implementing a critical algorithm, a parser, or a data structure that needs to maintain complex invariants, having a path to Dafny-backed verification without leaving the TypeScript ecosystem is a genuine option that did not exist before.

The broader trend is encouraging. Lean 4 has built a serious community around machine-checked proofs, partly by making the language pleasant to write in. Dafny has improved its usability substantially over the last few years, and its multi-language compilation backends mean that investment in Dafny verification is not siloed to a single platform. The Z3 solver itself continues to improve at handling the kinds of quantifier-heavy formulas that algorithmic verification generates.

For TypeScript developers, the message from LemmaScript is that formal verification is no longer something that happens in a separate research language that your production code never touches. The boundary is getting thinner. Whether it becomes thin enough for mainstream adoption depends on tooling, documentation, and how much the community is willing to invest in specification writing, which has always been the hardest part.