Salto: Static Analyses for Trustworthy OCaml

camel robot
A futuristic camel robot
(image produced by Stable Diffusion)

The expressive type system of OCaml brings strong static safety guarantees by ensuring data is used in a consistent way by a program. The Salto project aims at providing OCaml programs with additional guarantees, by answering questions such as:

Those questions are beyond the scope of the OCaml type system, but are within reach of abstract interpretation-based static analyses.

The goal of the Salto project is to define sound static analyses that help answer the above questions as automatically as possible. The analysis will help a programmer have better confidence in her programs, by bringing increased safety and security guarantees.




The Salto project is a partnership between Nomadic Labs and Inria, and is funded by the Tezos Foundation.