A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

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 …

(Mirror) A Machine-to-Machine Interaction System for Lean 4

TorchLean is the first unified Lean 4 framework for neural-network specification, execution, and verification.

A verifier for automated and interactive proofs about transition systems.

Lean 4 port of Iris, a higher-order concurrent separation logic framework

LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.

Functional Algorithms Design

Definitional implementation of Cedar language and utilities for DRT

Floating Point Semantics Mechanization for Lean

Lean 4 kernel / 'external checker' written in Lean 4

Lean 4 programming language and theorem prover

Armv8 Native Code Symbolic Simulator in Lean

Public reference documents for the SMT-LIB standard

Experiments on automation for Lean

Tactics for discharging Lean goals into SMT solvers.

Connecting bv_decide to SMTLIB.

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

A Foreign Function Interface (FFI) to cvc5 solver in Lean.