Download
xLaDe is a simple Python-based CLI tool built for executing and preserving Lean 4 projects. It is an ecosystem-level tool, which records the toolchain and other metadata of projects and allows the reconstruction and rebuilding of that exact environment later.
Lean 4 undergoes rapid development, which can introduce backward-compatibility issues. This problem becomes more difficult as the versions accumulate over time. xLaDe is built to mitigate the practical issues of backward-compatibility problems and improve ecosystem-level tooling for the Lean 4 theorem prover.
Instead of directly solving backward-compatibility issues by storing every version of Lean 4 and other tools or providing cross-version compatibility, xLaDe tries to store sufficient environment metadata such as toolchains, dependencies, and other context, and then recreates the environment for running Lean 4 projects upon request, also termed as experiments in xLaDe.
Features
- Lean 4
- Proof Assistants
- Reproducibility
- Formal Verification
- Software Preservation
Project Samples
License
GNU General Public License version 3.0 (GPLv3)Follow xLaDe
User Reviews
-
I noticed you're focused on helping teams maintain visibility as AI-generated code becomes a larger part of the development process. One challenge we hear often is that teams can review the code itself but still struggle to understand the broader architectural impact of those changes. Is that something your users are running into as well?Reply from xLaDePosted 2026-09-28
Brother...we don't have a userbase. For info: I just use AI agents for minimal precise changes. No major changes are AI driven which includes architecture too. All the final architectural and major decisions are made by me or our CEO, Manpreet. -
I like the project because I made it :)
