GitHub - cristianoc/TScert: TScert: a sound core for TypeScript. An independent checker, whose soundness is proved in Lean, accepts a TypeScript function only with a proof.

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. tscert-launch.mp4 Why 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. An example 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. How it works 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.

What acceptance means 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. Status 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. On the shoulders of 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. Try it 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. Develop 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 Read next 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. License 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.