OCamlPro is developing and maintaining a few major software, such as the Alt-Ergo SMT solver, for program verification, and the OPAM source package manager and the TypeRex programming tools for OCaml developers.

Web Data-Intensive Applications


OCamlPro develops Web Applications that can perform complex data-intensive computations at full-speed. As an example of such applications, OCamlPro has developed an online version of the OCaml interpreter, performing lexing, parsing, typing, bytecode generation, and translation to Javascript, so that the full OCaml language is available without maintaining a connexion to a server.

Program Verification and Certification


Alt-Ergo is an SMT solver specifically designed for program verification. It is used as an automatic theorem prover for logical goals generated by frameworks such as Frama-C, for C-program verification, Why3, Ada-Spark and soon Atelier-B, within the ANR Bware project.

Tools for OCaml Developers


OPAM is the OCaml Package Manager. It allows you to easily install any OCaml package together with all its dependencies, in just one command, while maintaining different versions of OCaml. All the most popular OCaml packages are already available in the primary directory.


TypeRex is a set of programming tools to help OCaml developers. Basic tools, such as ocp-indent, ocp-index or ocp-build and basic documentation, such as OCaml Cheat Sheets are developed for the whole community, and available as free software on TypeRex community website and our GitHub account.

A second set of tools, for professional users, is available only to the members of the TypeRex Pro Subscription, also in open-source.