20 projects
Z3
Z3 is a high-performance theorem prover and satisfiability modulo theories (SMT) solver developed by Microsoft Research. It provides a state-of-the-art solver for logical formulas over multiple theories, supporting applications in software verification, analysis, testing, and automated theorem proving.
2,335
562
$23M
Mathlib4
Mathlib4 is a comprehensive mathematical library for the Lean 4 theorem prover, providing formalized mathematical theorems, definitions, and proofs. It serves as the standard library for mathematical development in Lean 4, supporting areas like algebra, topology, category theory, and analysis.
1,869
173
$56M
Lean 4
Lean 4 is a functional programming language and interactive theorem prover developed by Microsoft Research and the Lean community. It combines powerful automation with expressive logic, enabling both mathematical theorem proving and general-purpose programming. The language features dependent types, metaprogramming capabilities, and a modern build system.
929
218
$25M
Agda
Agda is a dependently typed functional programming language and proof assistant developed by Chalmers University. It allows writing programs and proving properties about them in a unified framework based on intuitionistic type theory.
884
234
$11M
Coq
Coq is a formal proof management system and dependently typed programming language that enables mathematical theorem proving, formal specification and verification of programs, and formalized mathematics. It provides a rich environment for interactive development of machine-checked proofs.
765
120
$16M
F*
F* is a general-purpose functional programming language with dependent types, aimed at program verification. It puts an emphasis on security, verification, and program correctness through its advanced type system and automated theorem proving capabilities.
543
141
$12M
LiquidHaskell
Liquid Types For Haskell
419
132
$7.2M
SAW (Software Analysis Workbench)
SAW (Software Analysis Workbench) is a formal verification tool that enables automated reasoning and proofs about the behavior of software, particularly focused on cryptographic implementations and low-level code. It uses symbolic simulation and automated theorem proving to verify properties of programs written in languages like C, Java, and Cryptol.
259
44
$4.6M
Verus
Verus is a verification framework and programming language built on Rust that enables formal verification of systems software. It allows developers to write and verify code using mathematical proofs to ensure correctness and safety properties.
259
54
$18M
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
239
36
$24M
HoTT Library
A Coq library for Homotopy Type Theory
238
44
$3.6M
CakeML
CakeML: A Verified Implementation of ML
234
27
$26M
CompCert
CompCert is a formally verified C compiler that mathematically proves the generated assembly code is functionally equivalent to the source code, providing extremely high reliability for safety-critical software development
229
75
$7.5M
ACL2
ACL2 System and Books as Maintained by the Community
221
20
$956M
Metamath
Metamath is a formal mathematical proof verification system and database of mathematical proofs. It provides a minimalist foundation for mathematics based on a simple substitution engine with an emphasis on complete rigor and machine verification of proofs.
166
15
$45M
EasyCrypt
EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. It is designed for verifying cryptographic proofs and includes a programming language for describing games, a logic for proving equivalence between programs, and a verification condition generator.
164
20
$2.1M
Fiat
Fiat is a deductive synthesis framework developed at MIT that enables the derivation of correct-by-construction programs from high-level specifications. It focuses on automated generation of efficient implementations while providing formal guarantees about correctness.
62
13
$9.2M
Agda Standard Library
The Agda standard library
Mathematical Components
Mathematical Components