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

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…

A website used to host 4temps tournaments

[wip] functorial library with classic algorithms for arithmetic

Prof. Spacetime

An ocaml implementation of conflict-driven reasoning

Type-checker for 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