Awesome Lean

• Lean 4The compiler, language server, the Lake build system, and the standard library (Std: async I/O, TCP, HTTP, Std.Time, hash maps, iterators, and more).leanprover/lean4
• elanToolchain manager for Lean, similar to rustup.leanprover/elan
• ReservoirPackage registry and index for Lean packages.
• Batteries"Batteries included" extended library with data structures, utilities and tactics beyond core.leanprover-community/batteries
• Lean 4 WebOnline Lean editor running in the browser (source).
• Lean on Compiler ExplorerInspect the IR, C and assembly that Lean generates on godbolt.org.
• VersoDocumentation authoring tool used for the Lean manual, books and websites, with elaborated and highlighted Lean code (website).leanprover/verso
• doc-gen4API documentation generator for Lean 4 packages.leanprover/doc-gen4
• CSLibThe Lean Computer Science Library: algorithms, semantics, automata, and models of computation.leanprover/cslib

Books & Guides

• Functional Programming in LeanThe standard introduction to Lean as a programming language.
• Theorem Proving in Lean 4Dependent type theory and proofs in Lean.
• The Lean Language ReferenceThe official reference manual.
• Metaprogramming in Lean 4Book on macros, elaborators, tactics and the MetaM stack.leanprover-community/lean4-metaprogramming-book
• From Zero to QEDInformal introduction to Lean 4 for programmers.sdiehl/zero-to-qed
• Lean by ExampleLean and its main libraries explained through code examples (Japanese).lean-ja/lean-by-example
• Lean (meta-)programming CookbookRecipes for common programming and metaprogramming tasks.
• Tactic Programming GuideBeginner's guide to writing tactics.mirefek/lean-tactic-programming-guide
• Lean Symbol ReferenceSearchable list of Unicode symbols and their input abbreviations.
• Lean SnippetsFunctional programming patterns in Lean 4, from lazy evaluation and continuations to category-theory-inspired techniques.palladin/lean-snippets

Programming Languages & Verification

• Software Foundations in LeanThe Software Foundations textbooks, being translated from Rocq to Lean.plclub/sf-in-lean
• Programming Language Foundations in LeanLearn Lean 4 with PLFA.rami3l/PLFaLean
• Essentials of Compilation in LeanAn incremental compiler following "Essentials of Compilation".keilambda/eocia-lean
• CPDT in LeanLean implementations of material from "Certified Programming with Dependent Types".hargoniX/cpdt-lean
• Aeneas TutorialVerifying Rust programs in Lean with Aeneas (ICFP tutorial).AeneasVerif/icfp-tutorial
• Human-eval-leanHand-written, verified Lean solutions to the HumanEval benchmark, useful as idiomatic examples.leanprover/human-eval-lean

Practice

• leetproof.orgPractice platform with Lean challenges and community solutions.

• vscode-lean4Official VS Code extension with infoview, widgets and Unicode input.leanprover/vscode-lean4
• lean.nvimNeovim support for Lean 4, including an infoview.Julian/lean.nvim
• lean.vimPort of lean.nvim to Vim.SamuelSchlesinger/lean.vim
• lean4-modeEmacs major mode for Lean 4.leanprover-community/lean4-mode
• lean-ts-modeTree-sitter-based Emacs mode.lua-vr/lean-ts-mode
• tree-sitter-leanTree-sitter grammar for Lean 4.Julian/tree-sitter-lean
• lean4ijIntelliJ platform plugin for Lean 4.onriv/lean4ij
• acme-lsp-leanLean support for the Acme editor.maksym-radziwill/acme-lsp-lean
• lean-tuiTerminal infoview built with Ratatui, driven by an LSP proxy.
• xeus-leanJupyter kernel for Lean 4 built on the xeus protocol.Verilean/xeus-lean
• lean4_jupyterJupyter kernel for Lean 4 using the REPL.utensil/lean4_jupyter
• ProofWidgets4Build custom interactive UI widgets (React) for the infoview.leanprover-community/ProofWidgets4
• bubbleOpen Lean projects and PRs in sandboxed VS Code containers so untrusted code can't touch your machine.kim-em/bubble
• PaperproofInfoview that shows proofs as pen-and-paper-style trees.Paper-Proof/paperproof

• lean-actionGitHub Action to build, test and lint Lean projects.leanprover/lean-action
• LeanProjectRepository template with CI, docs and blueprint setup.leanprover-community/LeanProject
• lean-updateGitHub Action to keep Lean toolchains and dependencies up to date.leanprover-community/lean-update
• hopscotchCLI that bisects a dependency version range to find where your project breaks (action).leanprover-community/hopscotch
• levPackage and toolchain manager for switching between Lean projects and versions, inspired by uv.Robertboy18/lev
• lean4-nixNix flake for Lean 4 and lake2nix.lenianiva/lean4-nix
• rules_leanBazel rules for Lean 4 and Lake, focused on cross-language native builds.pb64-lean/rules_lean
• setuptools-leanPlugin for setuptools that packages Python modules written in Lean.leanprover/setuptools-lean
• lean-churn-botOpens PRs that fix upstream breakage using only compiler suggestions, no LLM.FawadHa1der/lean-churn-bot
• intentionsGitHub Action for claiming issues and reporting who is working on what.leanprover-community/intentions
• lean-optimizationsProposed optimizations that speed up builds and interactive use (paper).danromik/lean-optimizations

Documentation & Literate Programming

• Verso SlidesVerso genre for reveal.js slide decks with checked Lean code.leanprover/verso-slides
• SubVersoExtracts highlighted Lean code for use in Verso and other tools.leanprover/subverso
• mdgenGenerates Markdown files from Lean sources.Seasawher/mdgen
• LiterateLeanFiles that are valid Markdown and valid Lean at the same time, with no preprocessor.tani/literate-lean
• lean-slidesRenders reveal.js slides from Markdown comments inside the infoview.0art0/lean-slides
• LeanTeXDSL for writing LaTeX Beamer presentations in Lean.kiranandcode/LeanTeX
• versotreedocGenerates a Verso document skeleton that mirrors a source tree.richardlford/versotreedoc
• doc-verification-bridgeDocumentation tool that extracts verification relationships from Lean code.NicolasRouquette/doc-verification-bridge
• lean-i18nTranslate Lean projects with PO files.hhu-adam/lean-i18n

Formatting & Linting

• leanfmtStructure-preserving code formatter.duckki/leanfmt
• lean-fmtCode formatter and linter with editor and CI integration.jcreinhold/lean-fmt
• leanerLinter, formatter and whole-program dead-code eliminator.SrGaabriel/leaner
• lint-llm-proofsLinters for patterns common in LLM-generated proofs.jessealama/lint-llm-proofs

Analysis & Inspection

• import-graphAnalyze and visualize a package's import structure (lake exe graph).leanprover-community/import-graph
• jixiaStatic analysis tool that extracts declarations, dependency graphs and tactic states.frenzymath/jixia
• FlameTCFlame graphs for debugging type class synthesis performance.hargoniX/Flame
• leaffDiff tool for Lean environments.alexjbest/leaff
• lean4exportPlain-text export of declarations for external checkers and tools.leanprover/lean4export
• ast_exportExports Lean 4 ASTs.digama0/ast_export
• lean2sexpConverts .olean files to s-expressions.andrejbauer/lean2sexp
• NodeGraphGenerates dependency graphs between declarations.adamtopaz/NodeGraph
• lean4-dep-auditTraces a constant's transitive dependencies down to axioms, externs and their C sources.levzlotnik/lean4-dep-audit
• Lean FuzzGrammar-based fuzzing for Lean DSLs, using parser tables extracted from the compiler.kiranandcode/lean-fuzz

Kernels & Proof Checking

• lean4checkerReplays an environment to check that the kernel accepts every declaration (archived).leanprover/lean4checker
• ComparatorChecks that a solution proves exactly the stated challenge theorem, using only allowed axioms.leanprover/comparator
• Lean Kernel ArenaTest suite and leaderboard for independent Lean kernel implementations (source).
• SafeVerifyRobustly checks submitted proofs and implementations against a reference.GasStationManager/SafeVerify
• axiom-auditAxiom allowlist check that fails CI on sorry, native_decide or custom axioms.leanprover-community/axiom-audit

• PlausibleProperty-based testing and counterexample search.leanprover-community/plausible
• LSpecSpecification testing framework.argumentcomputer/LSpec
• nestExtensible test framework inspired by Haskell's tasty (unit tests).hargoniX/nest-core
• LTestFixture-based test framework in the style of pytest.alexf91/LTest
• LeanTestUnit testing framework with a wide range of assertions.tim-br/LeanTest
• lean4-assert-commandSimple #assert command for inline checks.pnwamk/lean4-assert-command

• LeanCollsCollections library with a uniform interface.JamesGallicchio/LeanColls
• hashbrown4leanPort of Rust's hashbrown SwissTable hash map.SchrodingerZhu/hashbrown4lean
• CCtxFirst-class constructor contexts for writing tail-recursive builders.pandaman64/CCtx
• itertoolsIterator library.tydeu/lean4-itertools
• ac-libraryPort of AtCoder Library for competitive programming.zer0-star/lean-ac-library
• AlgorithmVerified efficient algorithms.astrainfinita/Algorithm
• podLow-level utilities: single-precision floats, byte spans, unboxed vectors, finalizers.KislyjKisel/lean-pod
• bitmapImage utilities with verified PNG encoding and decoding.varosi/Bitmap

• lean4-parserParser combinator library.fgdorais/lean4-parser
• Megaparsec.leanPort of Haskell's Megaparsec.argumentcomputer/Megaparsec.lean
• prim-parserTotal parser combinators whose termination is guaranteed by graded monads.janmasrovira/prim-parser
• leansecTotal parser combinators.remimimimimi/leansec
• PartaxCompiles Lean syntax and parser definitions into standalone parsers.tydeu/lean4-partax
• lean-regexRegular expression engine with correctness proofs.pandaman64/lean-regex
• RegexPCRE2-compatible regular expression engine.bergmannjg/regex
• UnicodeBasicBasic Unicode character properties.fgdorais/lean4-unicode-basic
• lean-markdownCommonMark and GFM implementation that passes the official test suites and is proved total and HTML-safe.paulbutcher/lean-markdown
• lean4-markdownTyped DSL for building and rendering Markdown documents.predictable-machines/lean4-markdown
• MD4LeanWrapper for the MD4C Markdown parser.acmepjz/md4lean
• L4YAMLYAML 1.2.2 parser and dumper with verified properties.nasa-jpl/L4YAML
• lean-urlURL parsing based on the WHATWG standard.ammkrn/lean-url
• lean-semverSemantic versioning.runbikeswim/lean-semver
• printiestPretty printer library.ammkrn/printiest
• BibtexQueryCommand-line BibTeX query utility.dupuisf/BibtexQuery

• lean-jsonJSON library with no partial functions or panics, proved against the RFC 8259 grammar, with small binaries.paulbutcher/lean-json
• lean4-json-schemaDerives JSON Schema from types, with kernel-checked proofs that serialization validates.predictable-machines/lean4-json-schema
• protobufProtocol Buffers implementation.Lean-zh/protobuf
• binarySerialization and deserialization of binary data, inspired by Haskell's binary.Lean-zh/binary
• LeanSerdeSerialization framework with deriving handlers.oOo0oOo/LeanSerde
• ln-messagepackMessagePack serialization in pure Lean.ItsMeForLua/ln_messagepack
• lean4-base64RFC 4648 Base64 encoding and decoding.predictable-machines/lean4-base64
• protovalidate-leanTurns CEL constraints on protobuf fields into refinement types.pb64-lean/protovalidate-lean
• leanxml2libxml2 bindings: DOM parsing, namespaces, serialization and XPath.paulbutcher/leanxml2

Servers & Frameworks

• LeanIOHTTP router for Std.Http with compile-time checked routes, JSON handling and middleware.ecyrbe/leanio
• LeanTEAFull-stack web and TUI framework based on The Elm Architecture.Verilean/lean-tea
• lean-htmlTyped HTML5 (lean-htmx adds typed hx-* attributes).paulbutcher/lean-html
• lean-routingTyped router and route table.paulbutcher/lean-routing
• lean-middlewareSessions, sealed cookie store, anti-forgery, static files and request tracing.paulbutcher/lean-middleware
• lean-formsWeb forms library.paulbutcher/lean-forms
• lean-authenticationMagic-link authentication, sessions and rate limiting.paulbutcher/lean-authentication
• datastar-leanDatastar SDK for Lean.saviorand/datastar-lean
• LeanRPCExpose Lean functions as JSON-RPC endpoints over HTTP with @[rpc].oOo0oOo/LeanRPC
• litheSimple web service framework.JoshuaPurtell/lithe

Protocols & Clients

• socket.leanBSD socket bindings.hargoniX/socket.lean
• http2-leanHTTP/2 protocol foundation and managed transports.pb64-lean/http2-lean
• ws-leanWebSocket protocol and networking library.pb64-lean/ws-lean
• tls13-leanTLS 1.3 client and server built on HACL* verified crypto primitives.pb64-lean/tls13-lean
• grpc-leanProtobuf code generation and a gRPC client/server runtime.pb64-lean/grpc-lean
• lean-grpcPure Lean gRPC stack (HTTP/2, HPACK, gRPC).RileyBetts/lean-grpc
• leancurllibcurl bindings (see also leanCurl).paulbutcher/leancurl
• lean-llmclientProvider-agnostic LLM chat client with tool calling.paulbutcher/lean-llmclient
• lean-mcpModel Context Protocol server library for writing MCP servers in Lean.paulbutcher/lean-mcp

Cloud & Observability

• lean-awsAWS SigV4 signing (lean-aws-lambda implements the Lambda runtime interface).paulbutcher/lean-aws
• lean-telemetryOpenTelemetry traces and logs.paulbutcher/lean-telemetry
• otel-leanOpenTelemetry logs API, proved batch SDK and OTLP exporters.pb64-lean/otel-lean
• infraTerraform-style infrastructure as code with dependent types.typednotes/infra
• iam-leanFormal models of AWS IAM policies (catalog).sufield/iam-lean

• leansqliteSQLite bindings from the Lean FRO.leanprover/leansqlite
• leanpostgreslibpq bindings with a connection pool, in the style of leansqlite (leanmigrate runs plain-SQL migrations).paulbutcher/leanpostgres
• pg-leanPostgreSQL client with a pure Lean wire protocol, SCRAM, TLS, COPY and pipelining.pb64-lean/pg-lean
• lean-pgxChecked Lean types and query runners generated from PostgreSQL DDL and SQL.pb64-lean/lean-pgx
• lean-linqType-safe LINQ-style SQL query DSL that compiles to parameterized SQL.palladin/lean-linq
• LeanMySQLMySQL API.arthurpaulino/LeanMySQL
• lean-redisAsync Redis client written in pure Lean on the Std TCP stack.ecyrbe/lean-redis
• redisLeanBindings to the hiredis Redis client.marcellop71/redis-lean
• mini-redisImplementation of the mini-redis server.hargoniX/mini-redis

• leancryptoSHA-256, HMAC-SHA256, RSA verification, codecs and DER.paulbutcher/leancrypto
• lean-cryptoCryptographic routines.joehendrix/lean-crypto
• lean-joseJSON Web Signature, JSON Web Key and JSON Web Token in pure Lean.paulbutcher/lean-jose
• jose-libcryptoOpenSSL backend for lean-jose that adds ECDSA, EdDSA and asymmetric signing.paulbutcher/jose-libcrypto
• lean-libcryptoBindings to OpenSSL 3's libcrypto through its generic EVP interfaces.paulbutcher/lean-libcrypto
• Blake3Bindings to the BLAKE3 hash function (see also Blake3Lean4, a pure Lean implementation).argumentcomputer/BLAKE3
• OpenSSL.leanOpenSSL bindings.argumentcomputer/OpenSSL.lean
• lean-cryptolibVerified Montgomery and Barrett modular reduction.atrieu/lean-cryptolib
• lean-zipCompression library (blog post: "Why Lean is faster than Rust").kim-em/lean-zip
• LeanHuffmanCodingHuffman coding with correctness proofs.AnirudhG07/LeanHuffmanCoding
• LeanBWT-Bzip2bzip2 via the Burrows-Wheeler transform, in pure Lean with proofs.AnirudhG07/LeanBWT-Bzip2

• Std.TimeDates, times, time zones and formatting in the core standard library.
• DateTimeISO 8601 date and time utilities.T-Brick/DateTime
• timelibDate and time library.ammkrn/timelib
• timePort of Haskell's time library, with verified date calculations.bergmannjg/time

• lean4-cliConfigure command-line interfaces and parse arguments (used by Lake).leanprover/lean4-cli
• LeansiTerminal formatting.schergen-org/Leansi
• PigmentTerminal colors and styling.RSoulatIOHK/Pigment
• asciiplotPlot functions as ASCII art in the infoview.alok/AsciiPlot

• flowReactive streams (Flow, SharedFlow, StateFlow).predictable-machines/lean4-flow
• StraumeStreams library.argumentcomputer/straume
• lean-effSmall extensible-effects library.palladin/lean-eff
• lean-effectsAlgebraic effects.paulcadman/lean-effects
• lean-reducersParallel, fused reducers.palladin/lean-reducers
• EffSpecEffect monads with specifications (Dijkstra monads).Izzimach/EffSpec-lean
• lentilCompile-time dependency injection.pb64-lean/lentil
• lean-cloudParallel and distributed programming with monadic workflows over shared blob storage.palladin/lean-cloud

• lean-sdl3SDL3 bindings.ValorZard/lean-sdl3
• lean-sdl3 (philnguyen)Comprehensive SDL3 bindings (lean-compose-ui is a cross-platform UI library built on them).philnguyen/lean-sdl3
• SDL.leanSDL2 bindings.Anderssorby/SDL.lean
• Raylib.leanBindings to the raylib game library.KislyjKisel/Raylib.lean
• rayleanBindings to the raylib game library.funexists/raylean
• lean-vulkanProof-of-concept Vulkan bindings.kuruczgy/lean-vulkan
• lean-wgpuWebGPU bindings via wgpu-native.Kiiyya/lean-wgpu
• HesperVerified GPU programming with type-safe WebGPU shaders.Verilean/hesper
• LeanPlotPlotting with deterministic SVG and PNG backends.alok/LeanPlot
• vizagramsVisualization library.arademaker/vizagrams
• LeanReactWrite React components in Lean that compile to JavaScript (experimental).theoriclabs/lean-react
• lean4-godotExperimental bindings to the Godot 4 game engine.kiranandcode/lean4-godot

• lean-iosBuild iOS apps with Lean: patched runtime, SDL3 bindings and build scaffolding.paulcadman/lean-ios
• lean4-androidCross-compiles the Lean runtime for Android (aarch64) with the NDK.saviorand/lean4-android
• lean-composeTyped DSL for authoring Jetpack Compose UI in Lean (example app calling Lean over JNI).saviorand/lean-compose

• SciLeanScientific computing: arrays, automatic differentiation and numerical methods.lecopivo/SciLean
• TorchLeanNeural networks with typed tensors, autograd, CUDA support and verification.lean-dojo/TorchLean
• TensorLibVerified tensor library.leanprover/TensorLib
• TablesDataframe library compatible with the B2T2 benchmark, with provable invariants.pandaman64/Tables
• HexVerified computational algebra: matrices, row reduction, polynomial factoring, LLL, graph isomorphism.leanprover/hex
• lpVerified linear programming solver that returns proof-carrying results, plus an lp tactic.leanprover/lp
• LeanBLASBLAS bindings with specifications.lecopivo/LeanBLAS
• EigenLeanEigen linear algebra bindings.lecopivo/EigenLean
• NumLeanNumerical matrix computations.arthurpaulino/NumLean
• FloatLibVerified floating-point arithmetic across formats.
• FloatSpecFormally verified float implementation.Beneficial-AI-Foundation/FloatSpec
• fp-leanFloating-point semantics mechanization.opencompl/fp-lean
• LeanCertVerified interval arithmetic: bounds, root finding and optimization.alerad/leancert
• intervalConservative floating-point interval arithmetic.girving/interval
• lean-unitsSI physical unit system.ecyrbe/lean-units
• lean-autogradAutomatic differentiation following JAX's autodidax.alok/lean-autograd
• lean4-mlirNeural architectures specified in Lean, with verified GPU codegen.brettkoonce/lean4-mlir
• ginac-leanGiNaC computer algebra bindings.utensil/ginac-lean
• LeanSageCall SageMath from Lean.oOo0oOo/LeanSage

• AlloyWrite C shims inline in Lean code.tydeu/lean4-alloy
• lean-sysRust bindings to the Lean runtime (lean-rs is a safe wrapper).digama0/lean-sys
• RustFFI.leanTemplate for Lean-Rust FFI.argumentcomputer/RustFFI.lean
• NerodiaWrite Python modules in pure Lean, inspired by PyO3 (preview, Lean FRO).leanprover/nerodia
• lean.pyTwo-way Lean/Python interop with automatic marshalling.BasisResearch/lean.py
• Extism Lean SDKCall WebAssembly plugins from Lean.extism/lean4-sdk
• lean-bindgenGenerates @[extern] declarations and C shims from a concise spec of a C header.kiranandcode/lean-bindgen

• SparkleType-safe, verifiable HDL compiler inspired by Clash.Verilean/sparkle
• CircuitlibDigital circuit verification using categorical semantics.matthunz/circuitlib
• LNSymArmv8 native-code symbolic simulator.leanprover/LNSym
• MRiscXCertified RISC-V interpreter with Hoare logic.JulsDE/MRiscX

• QqIntuitive, type-safe expression quotations.leanprover-community/quote4
• ThymeTyped, staged metaprogramming with dependent types and reasoning about metaprograms.frangio/thyme
• LeanductionGenerates usable induction principles for nested inductive types.arthur-adjedj/Leanduction
• MutualInductionMutual induction tactic.ionathanch/MutualInduction
• QPF(Co)datatype package built on quotients of polynomial functors.alexkeizer/QPFTypes
• CoinductiveLibrary for coinductive types built on polynomial functors, used to define interaction trees.ISTA-PLV/coinductive
• leansesLenses with custom notation.VCA-EPFL/leanses
• lean-substSubstitution library inspired by Autosubst.amarmaduke/lean-subst
• HexLuthorHex color literal syntax with inline VS Code preview.alok/HexLuthor
• ImperiaAlternative do notation for imperative code over non-monadic types (experimental).tydeu/imperia
• LeanBitsyntaxErlang-style <<...>> bit syntax for building and matching BitVec values (experimental).palladin/lean-bitsyntax

• grindBuilt-in SMT-style tactic combining congruence closure, E-matching and arithmetic.
• bv_decideBuilt-in bit-blasting decision procedure for BitVec goals, backed by a verified SAT proof checker (LeanSAT).leanprover/lean4
• AesopWhite-box, rule-based proof search.leanprover-community/aesop
• lean-smtDischarge goals to SMT solvers with proof reconstruction.ufmg-smite/lean-smt
• lean-cvc5FFI bindings to the cvc5 SMT solver.abdoo8080/lean-cvc5
• lean-autoInterface between Lean and automated theorem provers.leanprover-community/lean-auto
• DuperSuperposition-based automatic prover.leanprover-community/duper
• LeanHammerHammer combining premise selection, ATPs and proof reconstruction.JOSHCLUNE/LeanHammer
• CanonicalExhaustive term search in dependent type theory.chasenorman/CanonicalLean
• LeanwuzlaConnects bv_decide to SMT-LIB.hargoniX/Leanwuzla
• BlasterSMT-based reasoning core.input-output-hk/Lean-blaster
• eggEquality saturation tactic based on egg (deprecated).marcusrossel/lean-egg
• OptiSatVerified equality saturation engine.lambdaclass/truth_research
• SaturnSAT solvers with proofs.siddhartha-gadgil/Saturn
• trestleSAT utilities: encodings, solver APIs, and file format parsers and printers.FormalSAT/trestle
• CLeanGoBindings and DSL for the Clingo answer set programming solver.kiranandcode/cleango
• waterfallACL2-style proof search for inductive goals.samth/waterfall
• sosSum-of-squares tactic for nonlinear real arithmetic.leanprover/sos
• SmtLibDslTyped SMT-LIB DSL with backends for Z3, cvc5, Kissat and CaDiCaL.palladin/SmtLibDsl
• cpsatBindings to the OR-Tools CP-SAT constraint solver.paulbutcher/leancpsat
• deriving such thatPort of Rocq's program derivation tactic.kiranandcode/deriving-such-that
• BetterFindExtended #find for searching declarations by pattern, closer to Rocq's Search.kiranandcode/BetterFind.lean

Frameworks

• Std.Do / mvcgenBuilt-in monadic program logic and verification condition generator for do code.
• LoomFramework for building multi-modal verifiers of effectful programs.verse-lab/loom
• VelvetAuto-active program verifier.verse-lab/velvet
• VeilAutomated and interactive verification of distributed protocols and transition systems.verse-lab/veil
• Iris-LeanPort of the Iris higher-order concurrent separation logic framework.leanprover-community/iris-lean
• LentilLTL reasoning infrastructure.verse-lab/Lentil
• LeanSSRSSReflect-style tactic language.verse-lab/lean-ssr
• lean-machinesModelling and refinement of stateful systems.lean-machines-central/lean-machines
• leanSpecProgram specification in Lean 4.paulch42/lean-spec
• WybeCoderAgentic verified imperative code generation on Loom/Velvet.facebookresearch/wybecoder

Verifying Other Languages

• AeneasTranslates safe Rust to Lean for verification.AeneasVerif/aeneas
• haxExtracts Rust code to Lean (and other backends).cryspen/hax
• StrataPlatform for formalizing language syntax and semantics through extensible dialects and building automated reasoning tools on them.strata-org/Strata
• LemmaScriptVerification toolchain for TypeScript (tech preview).midspiral/LemmaScript
• rust-lean-modelsLean models of Rust standard library functions.model-checking/rust-lean-models
• ACL2LeanReplay ACL2 proofs as kernel-checked Lean theorems.OathTech/ACL2Lean
• TalosWebAssembly interpreter and weakest-precondition calculus for verifying WebAssembly modules.cajal-technologies/talos
• lean-mlirMLIR semantics and verified peephole rewrites.opencompl/lean-mlir

Semantics & Specifications

• Wasm.leanWebAssembly implementation.argumentcomputer/Wasm.lean
• lean-wasmFormalization of the WebAssembly spec.T-Brick/lean-wasm
• haskell-specFormal specification of the Haskell Language Report.haskell-spec/haskell-spec
• graphql-leanFormalization of the GraphQL specification.duckki/graphql-lean
• ELFSageELF parser and validator.draperlaboratory/ELFSage
• SHerLOCStableHLO analyzer.leanprover/SHerLOC
• TenCertVerified tensor compilation.leanprover/TenCert
• graphitiVerified graph rewriting for dataflow circuits.VCA-EPFL/graphiti
• lean-yjsVerification of the Yjs CRDT integration algorithm.iasakura/lean-yjs
• langlibEsoteric programming languages, formally.ilyasergey/langlib

Industrial & Security

• cedar-specLean specification and verification of AWS's Cedar authorization language, used for differential testing of the production implementation.cedar-policy/cedar-spec
• SampCertVerified differential privacy, used in production by AWS Clean Rooms.leanprover/SampCert
• VCVioMachine-checked cryptographic proofs with oracle computations.Verified-zkEVM/VCVio
• DyLeanSymbolic analysis of cryptographic protocols.BobDyLean/dylean
• verified-3d-mesh-intersectionVerified 3D constructive solid geometry.schildep/verified-3d-mesh-intersection
• bitrepRust crate for bit-identical float reductions, with the merge algebra proved in Lean.KyleClouthier/bitrep

Blockchain & Zero Knowledge

• EVMYulLeanExecutable formal model of the EVM and Yul.NethermindEth/EVMYulLean
• evm-smithFramework for AI systems to write EVM bytecode and prove it safe.leonardoalt/evm-smith
• BlancMinimal EVM contract language, with proofs about the deployed bytecode.skbaek/blanc
• CleanDSL for ZK circuits with soundness and completeness proofs (zk.golf).Verified-zkEVM/clean
• ArkLibFormally verified arguments of knowledge.Verified-zkEVM/ArkLib
• zkLeanDSL for specifying zero-knowledge statements.GaloisInc/zkLean
• risc0-lean4Model of the RISC Zero zkVM.risc0/risc0-lean4
• aegisVerify Cairo contracts.lindy-labs/aegis
• btc-verifiedVerified Bitcoin serialization, txids and Merkle commitments.ProofOfKeags/btc-verified

• lean4leanLean 4 kernel written in Lean 4.digama0/lean4lean
• nanodaIndependent Lean 4 type checker written in Rust.ammkrn/nanoda_lib
• con-lecheExternal Lean checker with a consistency proof (con-ron is a Rust port proved with Aeneas).leanprover/con-leche
• MetaleanVerified type checker for an idealized Lean type theory.intgrah/metalean
• Lean4LessTranslates Lean into smaller theories by eliminating definitional equalities.Deducteam/Lean4Less
• lean2agdaExports elaborated Lean code to Agda.lyphyser/lean2agda
• thalesTypeScript compiler and JavaScript engine in Lean.jessealama/thales
• leanexeCompiler for a Lean dialect that targets verified WebAssembly.jsmorph/leanexe
• lean2wasmCompile Lean to WebAssembly.T-Brick/lean2wasm
• lean-virProof of concept compiling Lean IR to wasm32-wasi.ejgallego/lean-vir
• lean-gccjitBindings to libgccjit, a basis for alternative backends.SchrodingerZhu/lean-gccjit
• QED64Lean and Mathlib running in the browser via wasm64.FawadHa1der/QED64
• yatimaZero-knowledge Lean 4 compiler and kernel.argumentcomputer/yatima
• ixZero-knowledge proof-carrying code for Lean 4.argumentcomputer/ix
• mm-lean4High-performance Metamath verifier.digama0/mm-lean4
• SomaDependently typed language powered by interaction nets.SrGaabriel/soma
• lapisConcurrent Language Server Protocol framework.SrGaabriel/lapis
• qdtQuery-based dependent type elaborator.intgrah/qdt
• DeBruijnSSAFormalization of SSA.imbrem/debruijn-ssa
• verified-compilerToy verified compiler.marcusrossel/verified-compiler
• LyreWrite Lean IR as Lean syntax.tydeu/lyre
• LRTModel of Lean's runtime primitives in Lean, partly porting the C runtime (work in progress).tydeu/lrt
• LeanPyExperimental implementation of Python in Lean.tydeu/leanpy

Agents & MCP

• lean-lsp-mcpMCP server that gives agents diagnostics, goals, hovers and search through the Lean LSP.oOo0oOo/lean-lsp-mcp
• lean4-skillsClaude Code skills and plugins for Lean work.cameronfreer/lean4-skills
• Lean BeamExtends the Lean LSP server for agent- and tool-driven workflows.leanprover/lean-beam
• LeanTool"Code interpreter" for Lean that LLMs can call.GasStationManager/LeanTool
• AXLEAxiom's Lean engine for proof verification, manipulation and runtime tasks (MCP).
• Archon HorizonWorkspace-first orchestration for long-running Codex or Claude Code sessions on Lean.frenzymath/Archon-Horizon
• ArchonMulti-agent coding and proving workflows over a Lean project, driven by blueprint DAGs.frenzymath/Archon
• Lean skillsOfficial agent skills for proofs, toolchain setup, bisection and more.leanprover/skills
• LeanSlopCall LLMs from inside Lean code as black-box automation.kiranandcode/leanslop
• AristotleHarmonic's formal reasoning agent, available via web, CLI and API.

Programmatic Access to Lean

• REPLJSON REPL that reports errors, sorries and proof states.leanprover-community/repl
• PantographMachine-to-machine interaction interface for Lean 4.leanprover/Pantograph
• PyPantographPython interface to Pantograph.stanford-centaur/PyPantograph
• leanclientDrive Lean from Python via the LSP.oOo0oOo/leanclient
• Kimina Lean ServerFast, scalable server for checking Lean code in batches.project-numina/kimina-lean-server
• LeanDojoExtract data from and interact with Lean repositories programmatically.lean-dojo/LeanDojo
• LeanCopilotLLMs as copilots inside Lean.lean-dojo/LeanCopilot
• llmleanLLM tactic suggestions from local or cloud models.cmu-l3/llmlean

Search

• LoogleSearch declarations by name, type pattern or constant (web).nomeata/loogle
• LeanSearchClient#search syntax for LeanSearch, Loogle and LeanStateSearch from the editor.leanprover-community/LeanSearchClient
• LeanExploreSemantic search engine with an MCP server.justincasher/lean-explore

Verified Code Generation Benchmarks

• VerinaBenchmark for verifiable code generation (code, specs and proofs).sunblaze-ucb/verina
• CLEVERCurated Lean benchmark for verified code generation.trishullab/clever
• VericodingTools and benchmarks for verified coding.Beneficial-AI-Foundation/vericoding
• SorryDBContinuously updated benchmark built from sorrys in real projects.SorryDB/SorryDB

Apps & Services

• lean-todomvc-maxProduction-style TodoMVC with passwordless sign-in, migrations, telemetry, an LLM panel and AWS Lambda deployment.paulbutcher/lean-todomvc-max
• LeanToDoWeb app built with leansqlite, Verso and htmx.pandaman64/LeanToDo
• lean-acme-widgetsCRUD service combining gRPC, refinement-typed protobuf validation, PostgreSQL and TLS.pb64-lean/lean-acme-widgets
• viperPython environment manager written in Lean.arthurpaulino/viper
• lean4-raytracerSimple raytracer.kmill/lean4-raytracer
• Shirika-RPCTypeScript worker RPC library whose protocol layer is checked in Lean.eluvane/Shirika-RPC

Games

• flappyClone of Flappy Bird built with raylean.paulcadman/flappy
• LeanDoomedRaycasting demo using SDL3.oOo0oOo/LeanDoomed
• lean4-mazeMaze game encoded in Lean syntax.dwrensha/lean4-maze
• Chess.leanChess in Lean 4.dwrensha/Chess.lean
• ChessProverChess engine with a theory for proving endgame statements.parabamoghv/ChessProver
• PuzzleLeanPuzzleScript engine: play grid puzzles in the infoview and prove them solvable.
• EleanvatorSagaElevator Saga played in the infoview.Julian/EleanvatorSaga
• lean-snakebirdSnakebird implementation.marcusrossel/lean-snakebird
• FunctorioBuild Factorio factories in Lean with types, functions and recursion.konne88/functorio
• lean4gameEngine and server for interactive Lean games (live).leanprover-community/lean4game

• Lean ZulipMain community chat; see the #Project announcements, #Program verification and #lean4 channels.
• Lean Community websiteCommunity resources, installation guides and documentation overview.
• Lean FROThe Focused Research Organization developing Lean, including roadmaps.
• Awesome Logic FormalizationRelated list about formalized logic.FormalizedFormalLogic/awesome-logic-formalization