Skip to main content

🌐 TypeScript verification

📽️ Demo 

Our goal is to bring formal verification 🛡️ to TypeScript in the same way TypeScript brings typing to JavaScript.

Formal verification is a strong method to ensure that code does not contain bugs or security issues 🧨 and improve the QA process. This is thanks to the use of mathematical methods 📐. With formal verification, we can probably hope to divide by one hundred the number of bugs on a code that is already well-typed and tested. If the verification is cost-effective enough, we can apply it on a large class of programs to improve the quality of existing software 🌟.

Our strategy is to consider a convenient subset of TypeScript (essentially a purely functional subset) and make an automatic translation to similar-looking Coq code. The Coq 🐓 system is an interactive proof assistant that allows to verify arbitrary specifications on programs, either automatically or with manual guidance. Our translation to Coq might or might not be 100% faithful. The goal is to be efficient even if we need some approximations.

We have two projects:

  1. coq-of-js to translate JavaScript code to Coq using the Babel parser. You can try it with our 📽️ demo  where you type JavaScript code on the left and see the Coq translation on the right. This works on untyped JavaScript. However it seems some type information would be helpful for the translation, so we are now directly targeting the translation of TypeScript (instead of untyped JavaScript).
  2. coq-of-ts to translate TypeScript code to Coq, using the TypeScript compiler API. This follows the coq-of-js project and is under development.

For any additional information or service request, if you have code to verify or to develop, contact us:

Helping you build 🚀