A tool-agnostic formal specification language for OCaml.

A Deductive Verification Tool for OCaml Programs

Public reference documents for the SMT-LIB standard

OCaml + Fly.io

Heterogeneous value maps for OCaml

Mold: A Modern Linker 🦠

Pretty-printing for error source locations

Dissect OCaml compiled programs, and weight their content

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

Memthol is a visualizer for memory profiling data generated from OCaml programs.

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Lookup utility for Path of Exile based on pathofexile.com/trade

print nested boxes, lists, arrays, tables in several formats

Implementation of relative placement tabulation for dance competitions

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…

A website used to host 4temps tournaments

[wip] functorial library with classic algorithms for arithmetic

Prof. Spacetime

An ocaml implementation of conflict-driven reasoning

Implementation of the λΠ-calculus modulo rewriting

Declarative terminal graphics for OCaml

Library for writing IRC bots in OCaml, a collection of plugins, and a dramatic robotic actor.

A modular sat/smt solver with proof output.

Multicore OCaml

QuickCheck inspired property-based testing for OCaml.

The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.

The core OCaml system: compilers, runtime system, base libraries

[private joke] IRC bot for a private channel on freenode

[beta] persistent memoization of computations, e.g. for repeatable tests and benchmarks