Lean 4 Proof Suite

View as Markdown

The lean4/ directory contains Lean models of Nucleus algorithms, specifications of their properties, and proofs checked by Lean’s kernel. These models are hand-written; they are not extracted from the production Rust implementation.

Neutron Lean — coming soon

Neutron Lean is the planned application verification framework for the multi-language ecosystem. Reusable application libraries, language conformance adapters, and integrated build tooling are still to be built. This page documents the existing Nucleus suite; the modeling architecture describes the proposed extension.

What is modeled

  • MVCC visibility, B-tree structure, write-ahead logging, and Raft designs.
  • HMAC, PKCE, and bitwise comparison models.
  • Bloom filters, LRU caching, and sliding-window rate limiting.

Properties hold for the model under the hypotheses of each theorem. For example, the LRU specifications require a well-formed cache with a positive capacity, bounded entry count, and no duplicate keys. A proof about bitwise comparison does not by itself establish timing behavior of compiled code.

Source layout

The Lake project is lean4/Nucleus/. Its Nucleus/ source directory contains:

  • Aeneas/: hand-written MVCC, B-tree, WAL, and Raft models. The directory name reflects an extraction ambition, not an implemented Rust-to-Lean pipeline.
  • Spec/ and Proofs/: their specifications and proofs.
  • Crypto/ and Structures/: cryptographic and data-structure models and proofs.
  • Helpers/: shared tactics and lemmas.

Build and audit

Use the toolchain pinned by lean4/Nucleus/lean-toolchain. From lean4/:

(cd Nucleus && lake build)
bash scripts/axioms.sh

The first command checks that proofs elaborate. The audit checks their dependencies against an allowlist, including rejection of sorryAx. A successful build alone does not establish an acceptable assumption set.

Assumptions and scope

The suite declares assumptions about an opaque SHA-256 construction: output length, collision resistance, and HMAC PRF security. The audit also permits the documented Lean logical axioms. Earlier structural proof obligations have been discharged; the old description of twenty-five remaining axioms is obsolete.

These proofs do not certify the shipping database binary, application code in another language, or runtime query results. Linking a theorem to an implementation requires an explicit correspondence argument or verified translation; conformance testing provides narrower evidence for the cases exercised.

See the suite README and sources for theorem statements and audit details.