The CompCert formally-verified C compiler

A Lean 4 port of the CompCert C front-end operational semantics.

LaTeX code for a paper on lean's type theory

Coq plugin for extracting Rust code

Verified implementation of TLS 1.3 in F*

An SoA library for Rust

Formalization of Algorithmic Information Theory in Lean 4

🔥LeetCode solutions in any programming language | 多种编程语言实现 LeetCode、《剑指 Offer（第 2 版）》、《程序员面试金典（第 6 版）》题解

Lean4: Total parser combinator library with do notation

An auto-active verifier embedded into Lean

Faster builds, zero effort.

HTTP API for Claude Code, Goose, Aider, Gemini, Amp, and Codex

It's a New Kind of Wrapper for Exposing LLVM (Safely)

A Rust verification tool

Formal Verification of the OpenVM RISC-V Extension

Formally verified smart contracts gives mathematical certainty across all inputs and execution paths. We bet that agents will make full formal verification practical.

earlyoom - Early OOM Daemon for Linux

Some lemmas for Lean 4 / Parser

♾️ A library for universe levels and universe polymorphism

Postgres rewritten in Rust, now passing 100% of the Postgres regression tests

Proof assistant based on the λΠ-calculus modulo rewriting

Formalization of pi injectivity and unique typing for MLTT in Lean

A blueprint for a formalization of infinity-cosmos theory in Lean.

WIP model of floats for the standard library

Directed type theory for formal category theory