TScert Verifies 643 of 686 TypeScript Functions in Lean, Under a Licence That Bars AI Training

TScert, a research project by Cristiano Calcagno, accepts a TypeScript function only if it comes with a proof, and its census dated November 4, 2026 shows 643 of 686 functions in its own tools/ folder verifying. The repository was created on October 16, 2026 and had 123 stars on November 5.

The README calls it "a sound core for TypeScript" and "unfinished by design". The checker and its soundness proof are written in Lean 4. A front end uses TypeScript's compiler API, and an OCaml program, called the producer, proposes the types the checker then tests.

What a passing function is guaranteed

The main theorem is named checkUnitJson_safe. For inputs and a heap that meet their declared types, an accepted function never applies an operation to a value it does not fit and never returns a value outside its result type. The README is explicit that it "may throw or run forever", so this is type safety and not termination or correctness.

1. Verify643 functions
2. Do not verify43 functions

Source: TScert README, accessed 2026-11-05

The 43 that do not verify are the honest part of the number. The sections of the README The Terminal read say nothing about whether they fail on a real defect or on a form the checker refuses to handle. It does say unsupported forms are refused with a reason.

What the proof does not cover

The README lists what is trusted and not proved: that the translation from TypeScript into the Lean calculus is faithful, which is reviewed and tested; the contracts of libraries and the host; callers meeting the declared types; and Lean itself. any is refused outright. Type assertions such as e as T and e! decide nothing.

That last rule is the point. TypeScript's own project lists, under the heading Non-goals in its design goals, "Apply a sound or "provably correct" type system. Instead, strike a balance between correctness and productivity." TScert's answer is not to change TypeScript but to accept only the subset where a proof can be built.

Construct	How TScert treats it
any	Refused
e as T, e!	Decide nothing
Unsupported syntax	Refused with a reason
Translation faithfulness	Trusted, reviewed and tested

A licence with an AI clause

The repository uses what its README calls the NON-AI MIT License, with a copyright line reading "Copyright (c) 2026 Cristiano Calcagno". It is the MIT text plus a restriction: the software "may not be used for the purpose of training or improving machine learning algorithms, including but not limited to artificial intelligence", and the condition carries over to derivatives and updates.

The README adds a reservation of rights against text and data mining under EU Directive 2019/790, Article 4(3), and an ai.txt file repeats it. Both are the author’s own legal position.

The README names its related work, from Reynolds in 1983 to the JSCert mechanisation of JavaScript in 2014, and keeps the full list in docs/REFERENCES.md. Open work is tracked in WORK.md, and the architecture and trust surface in docs/DESIGN.md.

Other small, sharp-edged tools the site has covered include a browser SQLite editor that uploads nothing and a Databricks API emulator.

The next census to watch is the one that follows v0.94: if the 643 rises, the README's own numbers will show it.