OPAM

miragemirage/mirage

A library operating system for building secure, performant unikernels in OCaml.

BAPBinaryAnalysisPlatform/bap

A suite of utilities and libraries for analyzing binary programs, supporting multiple architectures and offering symbolic execution.

Irminmirage/irmin

Irmin is an OCaml library for building mergeable, branchable distributed data stores using Git-like principles.

ocamlformatocaml-ppx/ocamlformat

An auto-formatter for OCaml code with customizable profiles and comment formatting.

ocaml-graphql-serverandreas/ocaml-graphql-server

A type-safe library for building GraphQL servers in OCaml with support for Lwt, Async, and subscriptions.

Jupyterakabe/ocaml-jupyter

An OCaml kernel for Jupyter notebooks, providing an OCaml REPL with markdown/HTML documentation, LaTeX, and image embedding.

Analysismath-comp/analysis

A formal real analysis library for the Coq/Rocq proof assistant, built on the Mathematical Components library.

Coq Platformcoq/platform

A dependable, cross-platform distribution of the Rocq proof assistant with a curated selection of libraries and tools.

OCaml Debuggerhackwaly/ocamlearlybird

A debug adapter for OCaml programs that implements the Debug Adapter Protocol for VS Code integration.

Freneticfrenetic-lang/frenetic

An open-source SDN controller platform that makes network programming easy, modular, and semantically correct.

GeoCoqGeoCoq/GeoCoq

A formalization of geometry in Coq based on Tarski's axiom system, containing both foundational and high-school style proofs.

ppx_deriving_yojsonwhitequark/ppx_deriving_yojson

A ppx_deriving plugin that generates JSON serializers and deserializers for OCaml types using the Yojson library.

lablqmlKakadu/lablqml

A library for creating QtQuick/QML GUI applications in OCaml and Reason, providing bindings and a PPX syntax extension.

OMicroBstevenvar/omicrob

A generic OCaml virtual machine for running OCaml programs on resource-constrained microcontrollers like AVR and PIC32.

Formalised Undecidable Problemsuds-psl/coq-library-undecidability

A Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.

ExtLibcoq-community/coq-ext-lib

A library of Coq definitions, theorems, and tactics for use in other Coq developments.

ConCertAU-COBRA/ConCert

A Coq framework for formal verification, property-based testing, and extraction of smart contracts.

ppx_importocaml-ppx/ppx_import

An OCaml syntax extension for importing types and signatures from compiled interface files to reduce redundancy.

slackoLeonidas-from-XIV/slacko

A complete OCaml interface to the Slack API with a command-line notification tool.

ocaml-zmqissuu/ocaml-zmq

OCaml bindings for ZeroMQ 4.x, providing message-passing capabilities for distributed systems.

Hydras & Co.coq-community/hydra-battles

A Coq-based project exploring hydra battles, ordinal numbers, addition chains, and Gödel's incompleteness theorem through formalized mathematics.

Monaeaffeldt-aist/monae

A Rocq library providing a formalized hierarchy of monads and their laws for monadic equational reasoning.

CoqEALCoqEAL/CoqEAL

A Coq library for effective algebra, providing optimized algorithms and a refinement framework for changing data representations in proofs.

ocurlygrek/ocurl

OCaml bindings to libcurl for client-side URL transfers supporting HTTP and multiple network protocols.

odsowainlewis/ods

A comprehensive library of data structures and algorithms implemented in OCaml for educational purposes.

Relation Algebradamien-pous/relation-algebra

A modular relation algebra library for Rocq (Coq) with reflexive decision tactics for Kleene algebra with tests and related theories.

Finmapmath-comp/finmap

A Coq library extending Mathematical Components with finite sets, finite maps, and multisets on choicetypes.

Graph Theorycoq-community/graph-theory

A Coq library formalizing graph theory results, including Menger's Theorem, Hall's Marriage Theorem, and Wagner's Theorem.

Waterproof editorimpermeable/waterproof

An educational environment for writing mathematical proofs in interactive notebooks, now available as a VS Code extension.

Docker-Coqcoq-community/docker-coq

Docker images for Coq proof assistant versions 8.4 to 8.20, based on Debian Slim with opam 2.x.

Algebra Tacticsmath-comp/algebra-tactics

Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.

Bazeljin/rules_ocaml

OCaml build rules for Bazel, enabling native and bytecode binary compilation with OPAM dependency management.

Odd Order Theoremmath-comp/odd-order

A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.

FCSL-PCMimdea-software/fcsl-pcm

A Coq library formalizing Partial Commutative Monoids (PCMs) for separation logic-based program verification.

ORaftkomamitsu/oraft

An OCaml implementation of the Raft consensus algorithm for building fault-tolerant distributed systems.

Mczifymath-comp/mczify

Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.