TScert принимает функцию на TypeScript только с доказательством, проверенным в Lean
TScert: A Sound Core for TypeScript
Проверяльщик типов TypeScript намеренно нестрог: any, утверждения типов, непроверенные чтения по индексу и ковариантные массивы пропускают код, который падает на undefined. TScert не доверяет выведенным типам, а требует сертификат — вывод о соответствии программы её типам, — который валидирует ядро, чья корректность доказана в Lean. Проект исследовательский: на версии v0.94 из 686 функций собственного фронтенда прошли проверку 643.
Для каждого входа, удовлетворяющего аннотациям, перевод функции в формальную модель никогда не применяет операцию к значению, которому она не подходит, и никогда не возвращает значение вне своего результирующего типа.