Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Flow is a static typechecker for JavaScript. To find out more about Flow, check out flowtype.org.
Infer is a static analysis tool for Java, Objective-C and C, written in OCaml.
Reason is a alternate syntax for OCaml. It's simple, fast & type safe code that leverages the JavaScript & OCaml ecosystems.
ReScript is a JavaScript backend for OCaml focused on smooth integration and clean generated code.