HOL - Canonical sources for HOL4 theorem-proving system

  •        8

This is the distribution directory for the Kananaskis release of HOL4. See http://hol-theorem-prover.org for online resources. The following is a brief listing of what's available in the distribution.




Related Projects

HOL theorem-proving system


HOL is a system for proving theorems in Higher Order Logic. It comes with a large variety of existing theories formalising various parts of mathematics and theoretical computer science.

cakeml - CakeML: A Verified Implementation of ML

  •    Standard

CakeML is a verified implementation of a significant subset of Standard ML. The source and proofs for CakeML are developed in the HOL4 theorem prover. We use the latest development version of HOL4, which we build on PolyML 5.7. Example build instructions can be found in build-instructions.sh.

Intercalation Calculus Prover


An ML-based automated theorem prover for propositional logic making use of an algorithm in the intercalation calculus.

lean - Lean Theorem Prover

  •    C++

Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.

certigrad - Bug-free machine learning on stochastic computation graphs

  •    Lean

Specifically, Certigrad is a system for optimizing over stochastic computation graphs, that we debugged systematically in the Lean Theorem Prover, and ultimately proved correct in terms of the underlying mathematics. Stochastic computation graphs extend the computation graphs that underlie systems like TensorFlow and Theano by allowing nodes to represent random variables and by defining the loss function to be the expected value of the sum of the leaf nodes over all the random choices in the graph. Certigrad allows users to construct arbitrary stochastic computation graphs out of the primitives that we provide. The main purpose of the system is to take a program describing a stochastic computation graph and to run a randomized algorithm (stochastic backpropagation) that, in expectation, samples the gradients of the loss function with respect to the parameters.

deepmath - Experiments towards neural network theorem proving

  •    C++

The Deepmath project seeks to improve automated theorem proving using deep learning and other machine learning techniques. Deepmath is a collaboration between Google Research and several universities. The source code in this repository is not an official Google product, but is a research collaboration with external research teams.

CVC4 - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems

  •    SMT

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

z3 - The Z3 Theorem Prover

  •    C++

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. If you are not familiar with Z3, you can start here.



A beginners' level theorem prover project for logic students. Okitsune is written in Haskell and open for contributions.

coq - Coq is a formal proof management system

  •    OCaml

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. Download the pre-built packages of the latest release for Windows and MacOS; read the help page on how to install Coq with OPAM; or refer to the INSTALL file for the procedure to install from source.

FStar - Verification system for effectful programs

  •    OCaml

The F* tutorial provides a first taste of verified programming in F*, explaining things by example. The F* wiki contains additional, usually more in-depth, technical documentation on F*.

Archive of Formal Proofs


The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientifc developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal. Submissions are refereed.

Z3 Test Suite


Test suite for the Z3 theorem prover.



Z3 is a high-performance theorem prover being developed at Microsoft Research.


  •    C

ManTa is an equational specification language and tools to support it: theorem prover, code generators (C and Ocaml), frontends.

IsaPlanner Reasoning Tools

  •    Java

IsaPlanner is a collection of reasoning tools: a proof planner for Isabelle, implementing a Rippling based inductive theorem prover; theory synthesis tools for Isabelle; an open-graph based tool for reasoning about quantum information (quantomatic);

agda - Agda is a dependently typed programming language / interactive theorem prover.

  •    Haskell

Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.

cap-faq - The CAP FAQ


No subject appears to be more controversial to distributed systems engineers than the oft-quoted, oft-misunderstood CAP theorem. The purpose of this FAQ is to explain what is known about CAP, so as to help those new to the theorem get up to speed quickly, and to settle some common misconceptions or points of disagreement. Of course, there's every possibility I've made superficial or completely thorough mistakes here. Corrections and comments are welcome: let me have them.

Haskell-Morte-Library - A bare-bones calculus-of-constructions

  •    Haskell

Morte is a super-optimizing intermediate language for functional languages. morte centers around a single idea: a strongly normalizing, typed, and polymorphic lambda calculus is the ideal language for super-optimization of programs. Optimization is just normalization of lambda terms. All abstractions desugar to lambda abstraction.


  •    C

Hosting home-made software which is mathematically proven to be correct. We make use of tools like HOL, PVS, ...