TScert only accepts TypeScript functions it can prove safe in Lean
TScert: A Sound Core for TypeScript
TypeScript's checker is deliberately unsound: any, type assertions, unchecked index reads, and covariant arrays let code that passes tsc still read undefined where a type promises string. TScert is an independent checker whose soundness is proved in Lean. It never trusts inferred types; an untrusted producer proposes claims, an untrusted search proposes a certificate, and the proved checker validates it. At v0.94 it verifies 643 of 686 functions in its own tools/ front end, refusing any and type assertions outright.
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.