Shadowgraph

Tech stack & purpose

HOL Light is a theorem prover built in OCaml that comes with multiple specialized libraries and tools for formal verification. The repository contains formalizations across diverse domains: IEEE floating-point numbers (treating them as a subset of real numbers, excluding signed zero and NaNs); first-order logic metatheory and automated theorem proving methods like resolution; elliptic curves over arbitrary fields; geometric algebra; and provability logic. It integrates with external SAT solvers including MiniSat and Cadical to prove propositional tautologies, includes a Boyer-Moore automation library for inductive proofs, and provides tools like ProofTrace for recording proof steps as JSON datasets. The codebase spans contributions from individuals including John Harrison, Charlie Jacobsen, Bill Richter, and various academic institutions such as the University of Utah and Concordia University, with most components distributed under HOL Light's BSD-2-Clause license.