Project Tapestry aims to give every nation and participant frontier AI they can call their own — uniting a global consortium to train a shared frontier model from which partners build and own sover…

Formally Verified Float Implementation with lean4

Early experiments fuzzing the Lean theorem-prover.

ACL2 System and Books as Maintained by the Community

syzkaller is an unsupervised coverage-guided kernel fuzzer

CN separation logic refinement type system for C

Checked C is an extension to C that lets programmers write C code with bounds checking and improved type-safety. The goal is to let people easily make their existing C code type-safe and eliminate …

Formalized Cryptography Proofs in Lean 4

There is always loom for family.

Verified compiler from LambdaBox to WebAssembly, C, Rust, and OCaml

Lean playground for programming language modeling tooling.

Unified TUI and CLI to index and search your local coding agent session history across 11+ providers (Codex, Claude, Gemini, Cursor, Aider, etc.)

Display Zotero collection on E-Readers with KOReader

FLOPS: Formalization in the Lean Theorem Prover of the P3109 Standard

An auto-active verifier embedded into Lean

SMT-based reasoning core for Lean4

Are We Fast Yet? Comparing Language Implementations with Objects, Closures, and Arrays

Yet another implementation of computer language benchmarks game

This work in progress aims to compare various HOT (higher-order and statically typed, a term coined by Phil Wadler) through reproducible course-grained, wall-time benchmarks. Our overall goals incl…

Electrum is a temporal extension to Alloy. Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in securi…

A model checker for relational first-order temporal specifications

The LTSmin model checking toolset

A deprecated equality saturation tactic for Lean based on egg.

SQLite bindings for Lean