TScert solo acepta funciones de TypeScript si traen una prueba verificada en Lean
TScert: A Sound Core for TypeScript
El comprobador de tipos de TypeScript es deliberadamente poco sólido: `any`, las aserciones de tipo y los accesos a índices sin comprobar dejan pasar programas que en tiempo de ejecución leen `undefined` donde el tipo promete `string`. TScert ataca ese hueco: propone tipos, traduce la función a un pequeño cálculo formal y exige un certificado de derivación que un checker, con su solidez demostrada en Lean, valida. Es un proyecto de investigación y en su propia base de código verifica 643 de 686 funciones.
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`.