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.
Contributors
2,335
Organizations
562
Software value
$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.
Contributors
1,869
Organizations
173
Software value
$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.
Contributors
929
Organizations
218
Software value
$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.
Contributors
884
Organizations
234
Software value
$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.
Contributors
765
Organizations
120
Software value
$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.
Contributors
543
Organizations
141
Software value
$12M
LiquidHaskell
Liquid Types For Haskell
Contributors
419
Organizations
132
Software value
$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.
Contributors
259
Organizations
44
Software value
$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.
Contributors
259
Organizations
54
Software value
$18M
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Contributors
239
Organizations
36
Software value
$24M
HoTT Library
A Coq library for Homotopy Type Theory
Contributors
238
Organizations
44
Software value
$3.6M
CakeML
CakeML: A Verified Implementation of ML
Contributors
234
Organizations
27
Software value
$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
Contributors
229
Organizations
75
Software value
$7.5M
ACL2
ACL2 System and Books as Maintained by the Community
Contributors
221
Organizations
20
Software value
$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.
Contributors
166
Organizations
15
Software value
$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.
Contributors
164
Organizations
20
Software value
$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.
Contributors
62
Organizations
13
Software value
$9.2M
Agda Standard Library
The Agda standard library
This project hasn't been onboarded to LFX Insights.
Mathematical Components
Mathematical Components
This project hasn't been onboarded to LFX Insights.