Trusted proof-checker for the SMT solver Roole

Satisfiability Modulo Theories (SMT) solver for the theory of bitvectors

Improved fzf.vim written in lua

High Performance GraphQL Runtime

Tinymist [ˈtaɪni mɪst] is an integrated language service for Typst [taɪpst].

The Ott tool for writing definitions of programming languages and calculi

Scalable Automated Reasoning for HPC and Clouds

Bring Microsoft Recall to Linux!

BenchExec: A Framework for Reliable Benchmarking and Resource Measurement

The Q superposition prover

Pedagogical first-order prover in Python

GPU Implementation of the STOMP algorithm for computing the matrix profile

QA for the Lean standard library

Kodkod solver for relational logic

LSP signature hint as you type

A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo

Plain-text declaration export for Lean 4

A verifier for automated and interactive proofs about transition systems.

Experiments on automation for Lean

Floating Point Semantics Mechanization for Lean

Wrangling Untrusted File Formats Safely

Rust reflection, serialization, deserialization, pretty printing, etc. — the last proc macro you should need

Verification infrastructure for the Isabelle/HOL interactive proof assistant

SAT Solver SATCH

The Lean reference manual

PRQL is a modern language for transforming data — a simple, powerful, pipelined SQL replacement

Model finder for higher-order logic