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.
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.
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.