feat: Add lean toolchain to nix

[v3lmx]

High Level Overview of Change

Add the lean4 toolchain to the nix development shell. This will be used by the upcoming formal verification work, and is not currently used in the build.

Context of change

We add a new development shell for formal verification containing the Lean 4 toolchain. We use a separate shell as the tool is quite large and won't be used by most users.

check-tools will check depending on the shell it's in using the XRPL_DEVSHELL env variable.

API Impact

No impact, development environment change only.

---

OLD: previous approach, kept for context on previous approach

## Context of Change

We add a new `nix/lean4.nix` that fetches the `lean4 4.28.0` tarball directly.

The version is pinned in `nix/lean4.nix` for now. Once the Lean sources are in the tree it should read `formal_verification/lean-toolchain` instead, so the toolchain Nix provides and the one lake expects cannot drift apart.

### Why?

nixpkgs carries one `lean4` version at a time, currently 4.30.0, and we need  4.28.0. 

There were a few alternatives considered that we could not use:

1. override the lean `version` and `src` in the nix package: does not work because the packaging changed between 4.28 and current: nixpkgs' `mimalloc.patch` is cut against 4.30 sources and the hunk fails to apply, because Lean reformatted `CMakeLists.txt` between  the two releases. 
2. pinning nixpkgs to a rev when lean4 was 4.28: the toolchain is cached so this is cheap, but nixpkgs builds with `-DUSE_GITHASH=OFF` and substitutes the tag string, so `lean --githash` reports `v4.28.0` rather than the release commit `7e01a1bf5c70fc6167d49c345d3bf80596e9a79b`. Lake writes the githash into its traces, so artifacts built by a stock toolchain get discarded and (0 vs 41 modules on a test project with one prebuilt dependency). the githash fixes that, but the override is no longer cached, so becomes a 25 minute source build, plus an old `nixpkgs` in the inputs.
3. [`lean4-nix`](https://github.com/lenianiva/lean4-nix) external flake: fetches the tarball the same way we do, would just be an added external dependency

## Development environment impact

The tarball is around 500 MB and unpacks to 2.6 GB, and being a  plain `fetchurl` there is nothing on cache.nixos.org to substitute. Anything pulling in `commonPackages` grows by that, including the CI images, and all developers updating their flake will get this 500MB download once.
If this is too much for the common packages, it is always an option to have a separate development shell for formal verification, allowing for an override in the `.envrc`, such that developers who work with those tools can just keep `.envrc.override` that loads the correct shell.

[kuznetsss]

I would suggest to move it to a separate devshell because most of developers don't need it. And it is quite large (500-800 MB artefacts on the releases page)

[mathbunnyru]

We discussed with Sergey and to make it both easy for people who need lean and everything else we need to add support for .envrc.local which will be gitignored and those who need a non standard devshell could create .envrc.local containing:
use flake .#lean_devshell
This lean devshell will have our regular devshell + lean

[kuznetsss]

@mathbunnyru, is it ok to bring stdlib here? Because I remember we have a custom built one but you probably know this part better

[mathbunnyru]

lean from nix should only be used as a tool, not something linked to, so this should be ok

[mathbunnyru]

My check-tools found this brings another problem: https://github.com/XRPLF/rippled/actions/runs/34207349071/job/102029155206?pr=8186

This downgrades clang from 22 to 19, which we would definitely would like to avoid

[mathbunnyru]

1. Can we maybe use 4.30.0? Not being able to use latest version of a tool is usually a pain in the future, when the gap will become even wider.
2. Please, update https://github.com/XRPLF/rippled/blob/develop/bin/check-tools.sh accordingly

[v3lmx]

1. Can we maybe use 4.30.0? Not being able to use latest version of a tool is usually a pain in the future, when the gap will become even wider.

Latest Lean4 release is 4.33, there are frequent version bumps. Using 4.30 helps us now as it's the latest in unstable, but it will be updated in the future. That means if there are ever breaking changes in Lean that break the formal verification code or proofs, that will have to be fixed as well.
We don't know exactly if that will happen, and if yes how much impact it will be, which is why we pinned it to the version we started with.
I'm currently checking other versions to get a sense of the impact.

What do you recommend here?

[mathbunnyru]

1. Can we maybe use 4.30.0? Not being able to use latest version of a tool is usually a pain in the future, when the gap will become even wider.

Latest Lean4 release is 4.33, there are frequent version bumps. Using 4.30 helps us now as it's the latest in unstable, but it will be updated in the future. That means if there are ever breaking changes in Lean that break the formal verification code or proofs, that will have to be fixed as well. We don't know exactly if that will happen, and if yes how much impact it will be, which is why we pinned it to the version we started with. I'm currently checking other versions to get a sense of the impact.

What do you recommend here?

I would use the version provided by Nix if it works.

Note that we don't pin specific versions of any software except for major gcc/clang (and libc version, but that's a different story).
We don't pin cmake/conan/etc versions manually, and just use the version that our pinned Nix provides.
In reality, major compilers are likely to require work to update (less and less, though), but "tools" are relatively easy to update.

So, I would try the simple approach we already use and only start doing something more custom (which we'll have to maintain), only when we get evidence we need to.

[v3lmx]

1. Can we maybe use 4.30.0? Not being able to use latest version of a tool is usually a pain in the future, when the gap will become even wider.

Latest Lean4 release is 4.33, there are frequent version bumps. Using 4.30 helps us now as it's the latest in unstable, but it will be updated in the future. That means if there are ever breaking changes in Lean that break the formal verification code or proofs, that will have to be fixed as well. We don't know exactly if that will happen, and if yes how much impact it will be, which is why we pinned it to the version we started with. I'm currently checking other versions to get a sense of the impact.
What do you recommend here?

I would use the version provided by Nix if it works.

Note that we don't pin specific versions of any software except for major gcc/clang (and libc version, but that's a different story). We don't pin cmake/conan/etc versions manually, and just use the version that our pinned Nix provides. In reality, major compilers are likely to require work to update (less and less, though), but "tools" are relatively easy to update.

So, I would try the simple approach we already use and only start doing something more custom (which we'll have to maintain), only when we get evidence we need to.

I tested the proofs against all the versions from 4.28 to 4.33, and each version bump adds some additional breakages. It seems most of them are minor, but we still need to deal with them.
I agree with you that the better solution would be to use the lean4 provided by nixpkgs, so that we stay up to date. However, that comes with the cost of potentially having to fix the proofs every time lean4 is updated. lean4 currently does not guarantee backwards compatibility.

We are fine with either solution, they have different tradeoffs on long-term maintenance.

@Tapanito any opinion on this? Depending on the plans for formal verification in the future, that might push towards one option or another

Here is the AI generated report of checking each version:

Lean version compatibility report

Result matrix (full lake build: model + FFI + proofs, 348 files)

Lean	Mathlib	Result	Broken decls / files
4.28.0	v4.28.0	✅ clean	0
4.29.1	v4.29.1	❌	5 decls / 3 files
4.30.0	v4.30.0	❌	6 decls / 4 files
4.31.0	v4.31.0	❌	30 decls / 16 files
4.32.2	v4.32.2	❌	86 decls / 32 files
4.33.1	v4.33.1	❌	126 decls / 40 files

The model (XRPL/Model, 33 files) and FFI (XRPL/FFI, 14 files) build cleanly on every version. All breakage is in XRPL/Properties. To verify completeness I stubbed each failing declaration's proof with sorry and re-ran until green — the counts above are the exact, full breakage sets (no defs were stubbed, so no false downstream failures; statements untouched).

Failure causes (cumulative per version)

1. 4.29+ — omega hits max-recursion-depth on goals mixing big Nat literals (10^15, 16^15) and Finset sums: Rounding/Guard.lean (hex_lt_iff_dec_lt, round_to_nearest_def), Rounding/SmallRangeBound.lean (×2), Rounding/DivQuotient.lean, and on 4.30+ STAmount/Add/Common/IOU.lean. Raising maxRecDepth to 8192 causes a hard stack overflow — so this needs genuine restructuring (clear/unfold/generalize before omega), but only at ~5–6 sites.
2. 4.31+ — simp/simp only "made no progress" is now an error (was tolerated in ≤4.30). This is by far the largest category: whole families like Number/Add|Mul|Normalize/**/BoundProof.lean, RoundsWithinProofs.lean, Closest/NoInbetween.lean. Plus minor convert … using 1 leftovers in Closest/Normalize.lean (fix: append norm_num/rfl). All mechanical, 1-line-ish each — but dozens of sites.
3. 4.32+ — stricter application matching: bind_ok_peel no longer applies after unfold+rw in most Vault/Common/* proofs (hypothesis is only definitionally a >>= chain now). Also BurnExits.lean no-op simp. Fixable per-site with change/dsimp/simp only [Bind.bind] shims — small but widespread (~50 sites).
4. 4.33+ — stricter rw: "motive is not type correct" ×10 and whnf heartbeat timeouts ×3 in the heavy DoRoundUp/Bounds.lean / ValueChar.lean proofs, plus one linarith regression (ScaleDown.lean). These are the least mechanical — some proofs will need real reworking (or conv/occs/simp instead of rw).

Verdict

• Big fixes? No refactoring of model/statements is needed anywhere — every failure is local to proof bodies, and I confirmed a green build on 4.33.1 with only those 126 proof bodies stubbed.
• Small fixes? Individually yes for ~80% of sites (del no-op simp, add norm_num, shuffle rw/change), but the volume makes the 4.33.1 upgrade a moderate effort: ~126 proof sites over 40 files, of which a handful (DoRoundUp motive-errors, whnf timeouts, omega recursion) need real attention.
• Suggested path if upgrading: go to 4.29.1 first (only 5 sites, all the omega issue), then 4.31 (simp sweep), 4.32 (Vault bind gymnastics), 4.33 (rw/motive + timeouts).

[mathbunnyru]

Let's use nix-provided 4.30 for now, also let's update when this is merged: NixOS/nixpkgs#545312

[v3lmx]

Let's use nix-provided 4.30 for now, also let's update when this is merged: NixOS/nixpkgs#545312

Sounds good.

One remaining question about check-tools.sh, what about programs in the fv (non-default) shell? Should we check based on the shell name, eg.

if [ "${XRPL_DEVSHELL:-}" = "formal-verification" ]; then
    echo
    echo "Formal verification toolchain:"
    check lean
    check lake
fi

[v3lmx]

Let's use nix-provided 4.30 for now, also let's update when this is merged: NixOS/nixpkgs#545312

Sounds good.

One remaining question about check-tools.sh, what about programs in the fv (non-default) shell? Should we check based on the shell name, eg.

if [ "${XRPL_DEVSHELL:-}" = "formal-verification" ]; then
    echo
    echo "Formal verification toolchain:"
    check lean
    check lake
fi

hey @mathbunnyru, sorry to ping you again, did you have a chance to see this question?

[mathbunnyru]

Let's use nix-provided 4.30 for now, also let's update when this is merged: NixOS/nixpkgs#545312

Sounds good.

One remaining question about check-tools.sh, what about programs in the fv (non-default) shell? Should we check based on the shell name, eg.

if [ "${XRPL_DEVSHELL:-}" = "formal-verification" ]; then
    echo
    echo "Formal verification toolchain:"
    check lean
    check lake
fi

Sorry for not answering you before, I was on vacation :)
I think since we're using another shell, it won't be tested (at least rn) in CI, but your approach sounds reasonable, so let's do it as you suggested.

[Copilot]

Copilot review overview

🟢 Approval recommended

The isolated toolchain, environment selection, and validation logic are consistent and introduce no unresolved issues.

Review effort: Balanced
Findings: None

What changed in this PR

Adds an opt-in Nix development shell for Lean 4 formal verification without affecting standard development environments.

Changes:

• Adds the formal-verification shell with Lean and Lake.
• Extends tool checks for the new shell.
• Supports local direnv shell overrides.

File	Description
nix/​devshell.nix	Defines the formal-verification shell.
bin/​check-tools.sh	Checks Lean and Lake in that shell.
nix/​check-tools/​README.md	Documents shell-specific tool snapshots.
.envrc	Loads optional local overrides.
.gitignore	Excludes local direnv overrides.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!