TScert proves TypeScript functions type-safe with a Lean-verified checker

A research project called TScert, published on GitHub under the account cristianoc and surfaced on Hacker News's front page, takes aim at the soundness gaps in TypeScript's type checker. Its approach is unusual: a TypeScript function is accepted only when it carries a machine-checked proof that it is type-safe, and the small checker that validates those proofs has itself been proved sound in the Lean proof assistant.

What TScert does

TypeScript's type system is deliberately unsound in places. As the project's README explains, features such as any, type assertions, unchecked indexed reads and covariant arrays let programs sail through tsc yet still read undefined where a type promises string. TScert offers a stricter deal for the code it accepts: for every input meeting a function's annotations, the function's translation into a formal model will never apply an operation to a value of the wrong shape and never return a value outside its declared result type. A theorem in Lean captures that guarantee, and the theorem covers the very checker that decides acceptance.

The README's worked example captures an array's length, pops the last element, then indexes at the old length minus one. Under strict mode — which leaves noUncheckedIndexedAccess off — tsc accepts the function with result type string even though it returns undefined at run time. TScert rejects it, reporting that the index expression's available claim is undefined | string while the return contract demands string. Rewritten with a result type of string | undefined, the same function is accepted.

Untrusted proposals, one verified checker

The pipeline is designed so that almost nothing is trusted. A front end built on TypeScript's compiler API reads the source and its declarations, with Lean planning the execution. An OCaml component, the producer, proposes a type for every expression and variable, but those answers are treated as claims, not facts. Lean then translates the function, using the proposed types, into a small formal language — the calculus — whose execution and safety semantics are defined in Lean itself. An untrusted search finally proposes a certificate, a derivation showing the translated program conforms to its types, and the verified checker validates that certificate against the same translation.

What acceptance guarantees — and what it doesn't

According to the README, acceptance proves that the function's translation, run on inputs and a heap matching the declared types, does not get stuck and does not return a value outside its result type. It may still throw or run forever. The trust base is explicit: the translation from TypeScript to the calculus is reviewed and tested but not proved; library and host functions are assumed to follow reviewed contracts; callers and imports are assumed to meet their declared types; and Lean itself is trusted.

Status and coverage

TScert is an open-ended research effort, not a product. Its benchmark is its own front end: at version 0.94, 643 of the 686 functions in the repository's tools/ directory verify, each checked in its own unit, according to a census tied to commit ae20a6c6 and dated 2026-11-04.

The supported subset is nonetheless broad, spanning variables, patterns, conditionals, switch, loops (including for...of and for...in), labeled blocks 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, tuples, optional chaining, enums, and classes with fields, methods and inheritance; closures with optional, default and rest parameters, generic functions checked for every permitted type argument, and async/await over native promises; and aliases, interfaces, unions, intersections and library types via reviewed contracts. any is refused outright, assertions like e as T establish nothing, and unsupported forms are rejected with a reason and location. Building the project requires Node, a pinned Lean toolchain, OCaml and Dune.

Foundations and an unusual license

The repository credits a long research lineage — Appel and McAllester's foundational proof-carrying code model, 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.

Its license is as distinctive as its architecture. The project uses what it calls the NON-AI MIT License: the MIT terms, plus an exclusion of the code from training or improving machine-learning systems and from datasets built for that purpose, extending to derivatives. Rights are also reserved against text and data mining under Article 4(3) of Directive (EU) 2019/790, restated in a machine-readable ai.txt file.

Why it matters

TypeScript is among the most widely used typed languages, and its soundness gaps are familiar to anyone who has chased an unexpected undefined. TScert's significance lies less in current coverage than in architecture: nothing the surrounding toolchain infers is trusted, every type claim and certificate passes through a small verifier whose soundness is a theorem, and the fragment boundary is honest — whatever cannot be proved is refused with an explanation. That is the proof-carrying-code idea applied to a mainstream industrial language. If the approach scales beyond its self-benchmark, it points to a practical route to per-function, machine-checked guarantees on critical code paths — a complement to tsc, not a replacement.