Stars
Lean 4 programming language and theorem prover
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name …
A verifier for automated and interactive proofs about transition systems.
Tactics for discharging Lean goals into SMT solvers.
Lean 4 kernel / 'external checker' written in Lean 4
Lean 4 port of Iris, a higher-order concurrent separation logic framework
Definitional implementation of Cedar language and utilities for DRT
Experiments on automation for Lean
TorchLean is the first unified Lean 4 framework for neural-network specification, execution, and verification.
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.
(Mirror) A Machine-to-Machine Interaction System for Lean 4
A Foreign Function Interface (FFI) to cvc5 solver in Lean.
Public reference documents for the SMT-LIB standard