TScert：TypeScript 的数学级安全核心
TScert: A Sound Core for TypeScript
TypeScript 的类型检查器为了实用性，在 `any`、类型断言等场景下故意放弃了类型安全性，导致程序运行时仍可能读取到 `undefined`。TScert 项目提供了一个独立的、经过 Lean 形式化证明的验证器，它不信任任何推断出的类型，只接受附带数学证明的函数。这意味着，只有当代码被证明在形式模型中永远不会对不匹配的值进行操作，且返回值严格符合声明类型时，TScert 才会放行。作为一个研究项目，它目前拒绝 `any` 和类型断言，旨在为 TypeScript 代码提供比传统编译器更强的安全保证。
它从不信任 TypeScript 或提议工具推断出的类型；它所信任的内容列在‘接受意味着什么’部分。