rules_lean

Bazel rules for building and verifying Lean 4 libraries and proofs, with optional Mathlib support.

Quick Start

Add to your MODULE.bazel:

bazel_dep(name="rules_lean", version="0.1.0")
lean=use_extension("@rules_lean//lean:extensions.bzl", "lean")
lean.toolchain(version="4.29.1")
use_repo(lean, "lean_toolchains")
register_toolchains("@lean_toolchains//:all")

With Mathlib

lean=use_extension("@rules_lean//lean:extensions.bzl", "lean")
lean.toolchain(version="4.29.1")
lean.mathlib(rev="v4.29.1")
use_repo(lean, "lean_toolchains", "mathlib")
register_toolchains("@lean_toolchains//:all")

Usage

load("@rules_lean//lean:defs.bzl", "lean_library", "lean_proof_test")
# Compile Lean sources and produce .olean files for downstream depslean_library(
name="my_lib",
srcs= [
"MyLib/Basic.lean",
"MyLib/Defs.lean",
],
)
# Write proofs that depend on your library and/or Mathliblean_library(
name="my_proofs",
srcs= ["Proofs/Correctness.lean"],
deps= [
":my_lib",
"@mathlib//:Mathlib",
],
)
# Verify proofs type-check (test target)lean_proof_test(
name="my_proofs_test",
srcs= ["Proofs/Correctness.lean"],
deps= [
":my_lib",
"@mathlib//:Mathlib",
],
)

Rules

lean_library

Compiles Lean 4 .lean source files and produces .olean outputs.

Attribute	Type	Default	Description
srcs	label_list	required	.lean source files, listed in compilation order
deps	label_list	[]	lean_library or lean_prebuilt_library targets
extra_flags	string_list	[]	Additional flags passed to lean

lean_proof_test

Test rule that verifies .lean proofs type-check (proofs are valid). Verification happens at build time; the test reports success.

Attribute	Type	Default	Description
srcs	label_list	required	.lean source files to verify
deps	label_list	[]	lean_library or lean_prebuilt_library targets
extra_flags	string_list	[]	Additional flags passed to lean

lean_prebuilt_library

Wraps pre-built .olean files (e.g. Mathlib) as a Lean dependency.

Attribute	Type	Default	Description
srcs	label_list	required	Pre-built .olean and related files
path_marker	label	None	Marker file at the root of the .olean directory tree

Toolchain Configuration

SHA-256 Verification

For reproducible builds, provide SHA-256 hashes per platform:

lean.toolchain(
version="4.29.1",
sha256= {
"darwin_aarch64": "abc123...",
"darwin_x86_64": "def456...",
"linux_x86_64": "789abc...",
"linux_aarch64": "012def...",
},
)

Hashes can be obtained from the Lean 4 releases page.

Supported Platforms

Platform	Lean Artifact
macOS (Apple Silicon)	darwin_aarch64
macOS (Intel)	darwin_x86_64
Linux (x86_64)	linux_x86_64
Linux (aarch64)	linux_aarch64

Aeneas Integration

Aeneas translates Rust programs (via Charon LLBC intermediate representation) into Lean 4 for formal verification.

Setup

aeneas=use_extension("@rules_lean//aeneas:extensions.bzl", "aeneas")
aeneas.toolchain(
version="build-2026.03.14.003732-912707da86162a566cd8b01f137383ec411b31de",
rev="912707da86162a566cd8b01f137383ec411b31de",
lean_version="4.29.1",
)
use_repo(aeneas, "aeneas_toolchains", "aeneas_lean_lib")
register_toolchains("@aeneas_toolchains//:all")

Usage

load("@rules_lean//aeneas:defs.bzl", "aeneas_translate")
load("@rules_lean//lean:defs.bzl", "lean_library", "lean_proof_test")
# Step 1: Translate LLBC (produced by Charon) to Leanaeneas_translate(
name="my_crate_translated",
srcs= ["my_crate.llbc"],
)
# Step 2: Compile the generated Lean codelean_library(
name="my_crate_compiled",
srcs= [":my_crate_translated"],
deps= ["@aeneas_lean_lib//:Aeneas"],
)
# Step 3: Write and verify proofslean_proof_test(
name="my_proofs_test",
srcs= ["MyProofs.lean"],
deps= [":my_crate_compiled"],
)

aeneas_translate

Translates LLBC files to Lean 4 using Aeneas.

Attribute	Type	Default	Description
srcs	label_list	required	.llbc files produced by Charon
extra_flags	string_list	[]	Additional aeneas flags (e.g. ["-split-files"])

How It Works

1. Toolchain download: lean_release downloads pre-built Lean 4 binaries from GitHub releases for each supported platform.
2. Toolchain resolution: Bazel's toolchain system selects the correct platform binary at build time.
3. Compilation: lean_library compiles .lean files to .olean using the downloaded lean binary, with LEAN_PATH set to resolve imports from the standard library, Mathlib, and other dependencies.
4. Mathlib: mathlib_repo uses lake to fetch Mathlib and download pre-built oleans, consolidating them into a single directory for import resolution.
5. Aeneas: Downloads pre-built Aeneas binaries, builds the Lean support library, and translates Rust LLBC to Lean 4 for verification.

License

Apache-2.0