TScert: A Sound Core for TypeScript

TScert is a research project that aims to provide stronger type-safety guarantees for a supported subset of TypeScript than the standard compiler offers. TypeScript permits constructs such as `any`, type assertions, unchecked array reads, and covariant arrays that can let values violate their declared types at runtime. TScert rejects unsafe functions unless it can validate a proof that their formal translations respect their annotations. For example, it catches a function that removes an array’s last element and then returns that element as a definite string; declaring the possible `undefined` result makes the function acceptable. The guarantee is that, for inputs and heap states matching declared types, a checked function’s translation neither gets stuck nor returns a value outside its result type. It may still throw or run forever.

The system parses TypeScript and its declarations, translates functions into a small calculus defined in Lean, and checks certificates against that translation. An OCaml producer and a certificate-search tool propose information, but their claims are untrusted; the Lean checker validates the proof, and its soundness is formally established. Trust still depends on the fidelity of the TypeScript-to-calculus translation, reviewed library contracts, callers and imports honoring declarations, and Lean itself. The supported fragment includes common control flow, arrays, objects, classes, functions, generics, and native promises; unsupported forms are refused with explanations, while `any` and type assertions provide no evidence. At version 0.94, the project reports checking 643 of 686 functions in its own front end, underscoring both its progress and its unfinished, bounded scope.