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 typ...