How would you describe them?
TScert: a sound core for TypeScript. An independent checker, whose soundness is proved in Lean, accepts a TypeScript function only with a proof.
