A static analyzer for Java, C, C++, and Objective-C

Simple, fast & type safe code that leverages the JavaScript & OCaml ecosystems

Performant type-checking for python.

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

Compiler from OCaml to Javascript.

A library for incremental computations

An OCaml library for HTTP clients and servers using Lwt or Async

KaRaMeL is a tool for extracting low-level F* programs to readable C code

A proof assistant for general type theories

Formal verification for OCaml

Coq to Rust program extraction. The whole tree is on the original Coq code base.

Sorry about the name

FuzzBALL: Vine-based Binary Symbolic Execution

Hygienic typed literal macros (TLMs) for Reason

[Deprecated see github.com/janestreet/hardcaml] Register Transfer Level Hardware Design in OCaml

OCaml code generator plugin for the Cap'n Proto serialization framework

An interactive theorem prover based on lambda-tree syntax

Semantics for ES5

Coq with native compilation, as well as machine integers and arrays !

An enhanced unification algorithm for Coq

A variant of OCaml's native code compiler ocamlopt using LLVM in the back-end for optimization and code generation. Warning: Binaries produced by this compiler are in no way compatible with binarie…

An OCaml bytecode to LLVM compiler

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 develo…

Outdated version of an LLVM based backend for OCaml. Newer version:

A transpiler that converts C programs into PlusCal specifications

ECOOP 2022 Elementary Type Inference