The Arend Proof Assistant

Rust-powered Svelte ecosystem

Formalising the WASM spec in Lean

Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization

Haskell implementation of the Edinburgh Logical Framework

A static verifier for Rust, based on the Viper verification infrastructure.

Development repo for translating Software Foundations to Lean

Iris tutorial in Lean

Lean4lean theorems depending on mathlib

How to verify a computer down to physics

An illustration of good taste in code

Scaling Reasoning for the Age of AI

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses t…

Kani Rust Verifier

x64 semantics in Lean

Verified computational algebra in Lean 4: aggregator for the released hex libraries

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

A full-stack web and TUI framework inspired by Yesod and Elm.