TScert checks that TypeScript functions are type-safe, and accepts a function only with a proof. A checker whose soundness is proved in Lean validates that proof. It never trusts the types that TypeScript or the proposing tools infer; what it does trust is listed under What acceptance means.

TypeScript's type checker is deliberately unsound in places: any, type assertions, unchecked index reads and covariant arrays let programs that pass tsc still read undefined where a type says string. TScert gives a stronger answer for the code it accepts: for every input that meets its annotations, the function's translation into a formal model never applies an operation to a value it does not fit, and never returns a value outside its result type. A theorem in Lean states that guarantee, and the checker that decides acceptance is the code the theorem is about.

TypeScript accepts this function (under strict, which leaves noUncheckedIndexedAccess off). TScert refuses it:

export function stale(xs: string[]): string {
  const n = xs.length;
  xs.pop();
  return xs[n - 1]; // past the end after the pop: undefined at run time
}

Abridged output (offsets refer to the example file):

"status": "unverified"
reject: source expression obligation at [219,228): evidence search failed: no derivation of its return-contract claim
obligation: The available claim for xs[n - 1] is undefined | string. This return requires string.

With the result type stated honestly, string | undefined, TScert accepts it. Both versions are pipeline cases: invalid-array-last-after-pop.ts and afterPop in array-last-element.ts.

A front end on TypeScript's compiler API reads the source and the declarations it uses, and Lean plans its execution. An OCaml program, the producer, proposes the type of every expression and variable; its answers are claims, and none is trusted. Lean translates the function, with those types, into a small formal language (the calculus) whose execution and safety are defined in Lean. An untrusted search proposes a certificate, a derivation that the program meets its types, and the checker validates it against the same translation. The stages describe each step.

Acceptance proves, of the function's translation into the calculus, that for inputs and a heap meeting their declared types it does not get stuck and does not return a value outside its result type. It may throw or run forever. The theorem is checkUnitJson_safe. Some things are trusted rather than proved:

• that the translation from TypeScript to the calculus is faithful (reviewed and tested, not proved);
• that library and host functions behave as their reviewed contracts state;
• that callers and imports meet their declared types;
• Lean itself.

The trust surface lists every assumption, and what "verified" means states the guarantee exactly.

TScert is a research project, unfinished by design. Its benchmark is its own front end: at v0.94, 643 of the 686 functions of tools/ verify, each checked in its own unit with what it calls read at its stated signature (census of ae20a6c6, 2026-11-04). The coverage metrics and the status table give the definitions and the dated measurements.

In outline, the supported subset covers:

• const/let, patterns, if, switch, loops including for...of and for...in, labeled blocks, throw and try/catch/finally;
• primitives with literal types, arithmetic, comparisons, template literals, typeof, in, instanceof and strict equality;
• object literals with spreads, records, index signatures, arrays and tuples, optional chaining, enums, and classes with fields, methods and a base class;
• functions, closures, optional, default and rest parameters, generic functions certified for every admissible type argument, async and await of native promises;
• declared types: aliases, interfaces, unions, intersections and library types through reviewed contracts.

any is refused, and a type assertion (e as T, e!) decides nothing. Every unsupported form is refused with a reason and a location. The fragment boundary lists what is refused and why.

TScert builds on decades of work on types and semantics, among them Appel and McAllester's indexed model for foundational proof-carrying code, Ahmed's semantics of types for mutable state, Wright and Felleisen's syntactic type soundness, Reynolds's parametricity, Abadi and Cardelli's theory of objects, semantic subtyping, JSCert, the ECMAScript specification and Lean 4. REFERENCES lists every work, with what TScert takes from it and where.

Prerequisites: Node, the pinned Lean toolchain, OCaml and Dune (the producer guide). Then:

make setup                                   # node dependencies
make build                                   # the Lean verifier and the OCaml producer
make check FILE=pipeline/examples/array-last-element.ts

make check prints the outcome and the directory holding the run's documents: the source, the parser's output, the producer's claims and the certificate.

make test     # fast checks and the controls (forged documents and claims)
make suite    # every pipeline case: source files with their expected outcome
make help     # every target

• DESIGN: principles, architecture, the trust surface, and the documentation map of every document.
• SEMANTICS, POSITIVE-TYPES, PROGRAM-TYPING: the calculus, its types and its typing rules.
• SOURCE-MODEL, SOURCE-ELABORATION, SOURCE-CONTRACTS, SOURCE-FRAGMENT: how TypeScript values and operations map to the calculus, how each source form lowers, how types and library contracts are read, and what the fragment refuses.
• AGENTS: the rules for changing the project: what a change must carry, which tests to keep, and how commits are recorded.
• WORK: open work and its status.
• Pipeline cases: worked examples of every supported construct, positive and negative.
• REFERENCES: the work TScert draws on.

Licensed under the NON-AI MIT License: the MIT terms, with the code excluded from use in training or improving machine-learning systems and from datasets for that training, also for its derivatives.

The copyright holder reserves the rights in this repository against text and data mining, under Article 4(3) of Directive (EU) 2019/790, including for training or improving machine-learning systems; ai.txt states the same reservation in machine-readable form.