xlade 1.6.0

eXperimental Lean 4 advanced Development ecosystem

xLaDe

eXperimental Lean 4 advanced Development ecosystem

---

Lean 4 proofs break silently across versions. Projects built on Lean drift from upstream until one day they simply stop working. Nobody knows why. These are not edge cases. They are the normal experience of working with a proof assistant under rapid development.

xLaDe is a research platform that studies these problems and builds tooling to address them. It is not a theorem library, a fork of Lean, or a replacement for any existing tool. It is an ecosystem layer — a controlled environment for running experiments on how Lean is used, enforcing architectural boundaries that prevent kernel drift, and recording enough metadata to reproduce any experiment correctly, years later.

xLaDe is built primarily as a command-line tool for Linux, with tested support for Windows (via WSL) and Android (via Termux). It installs through pip, ships with a comprehensive test suite and remains experimental.

---

The Problems

Lean proofs are fragile over time

Lean 4 evolves fast. A proof that compiles today may fail elaboration next year as the toolchain changes. This is acknowledged by the Lean core team. It is a deliberate trade-off for a language under active research development. But it makes reproducible research with Lean genuinely difficult. Experiments become snapshots. Snapshots rot.

xLaDe's response: treat each experiment as inseparable from its environment. Every experiment records its toolchain version, dependencies, and execution context. The goal is reproducibility i.e., being able to reconstruct the exact environment an experiment ran in, on demand, years later rather than backward compatibility, which Lean cannot guarantee.

Lean projects drift from upstream and break

When a project builds directly on top of a Lean fork, it gradually diverges. Features get patched in. Workarounds accumulate. The fork drifts. One day something breaks and there is no clear record of what was keeping it stable. Diagnosing this often requires understanding both the original Lean codebase and every local modification made on top of it. Sometimes it is simply not recoverable.

xLaDe's response: treat the Lean kernel as immutable infrastructure. Lean is included as a Git submodule. Any modification to it is detected by CI and the build fails. The boundary is enforced, not just documented. All experimental effects are attributable to ecosystem decisions, not kernel changes.

---

What xLaDe Provides

xlade init                          Initialise a workspace
xlade mode experimental             Select a mode
xlade list experiments              Discover available experiments
xlade run <experiment-id>           Run an experiment
xlade status                        View run summary
xlade metrics                       View full run history
xlade doctor                        Diagnose environment issues
xlade check                         Quick structural check

Experiments are the primary artifact. Each is a self-contained directory with a declared hypothesis, enforcement mechanism, lifecycle state, and exit criteria. They run via xlade run. Results are written to .xlade/metrics.json on every execution - success, failure, or skip.

Modes control which experiments are enabled and how strictly policies are enforced. Three modes: experimental, stable, onboarding.

Doctor diagnoses your environment and tells you exactly what to run to fix each issue, not just what is missing.

Metrics give you a structured audit trail of every experiment run, readable in the terminal or processable as JSON.

---

Working

xLaDe is not just a theoretical framework or concept. It runs experiments on real external Lean 4 projects.

$ xlade list experiments

  Experiments  (5 found)
  ----------------------------------------------------------------------------------------------------
  Experiment               Status    Type              Modes
  ----------------------------------------------------------------------------------------------------
  exp-001-proof-review     active    lean-policy       experimental
  exp-002-kernel-boundary  active    script-policy     experimental
  exp-003-doc-coverage     active    script-policy     experimental
  exp-004-project-proof-1  active    script-policy     experimental
  exp-005-lean4-courses    active    script-policy     experimental

$ xlade run exp-005-lean4-courses

  Running experiment:  exp-005-lean4-courses
  Mode:                experimental
  Toolchain:           leanprover/lean4:v4.30.0
  Timestamp:           2026-06-01 12:00:00
  ----------------------------------------------------------------------------------------------------
  xLaDe EXP-005: Lean4 Courses
  ----------------------------------------------------------------------------------------------------
  [info]   Project: experiments/exp-005-lean4-courses/lean4-courses
  [info]   Running: lake build
  ----------------------------------------------------------------------------------------------------
  ℹ [2/4] Replayed Solutions
  ...                           # Truncated for display
  ℹ [3/4] Replayed Examples
  ...                           # Truncated for display
  info: 0000-startup/Examples.lean:76:0: 3628800
  Build completed successfully (4 jobs).
  ----------------------------------------------------------------------------------------------------
  [pass]   lake build succeeded. 32 modules compiled.
  ----------------------------------------------------------------------------------------------------
  Status: success

EXP-004 and EXP-005 wrap real external Lean 4 repositories added as git submodules. Neither project has any code connection to xLaDe. xLaDe wraps them, runs lake build, and records full environment metadata — toolchain version, timestamp, status without touching their source.

That is the non-invasive ecosystem layer claim demonstrated, not just described.

Quick Start

Requirements: Python 3.11+, git, bash. For Lean experiments: elan + Lake (see INSTALL.md).

git clone --recurse-submodules https://github.com/LakshitSinghBishtTM/xLaDe.git
cd xLaDe
pip install -e .
xlade doctor
xlade init
xlade mode experimental
xlade list experiments
xlade run exp-002-kernel-boundary
xlade run exp-003-doc-coverage
xlade status

Full installation guide including elan, Lean toolchain, and platform-specific notes: INSTALL.md.

---

Active Experiments

Experiment	Type	What it does	Requires	External
exp-001-proof-review	lean-policy	Enforces proof review markers via Lake script	Lake	No
exp-002-kernel-boundary	script-policy	Detects modifications to lean-core/	bash	No
exp-003-doc-coverage	script-policy	README present in all experiments, modes, policies	bash	No
exp-004-project-proof-1	script-policy	Builds an external proof repo via lake build	Lake	Yes
exp-005-lean4-courses	script-policy	Builds a 32-module external Lean 4 course repo	Lake	Yes

EXP-002 and EXP-003 run on any machine with bash. EXP-001, EXP-004, and EXP-005 require a full Lean 4 + Lake installation via elan and skip cleanly without it.

EXP-004 and EXP-005 are external projects with no code connection to xLaDe. They are included as git submodules and executed without modification.

---

Build Modes

Mode	Experiments	Enforcement	For
experimental	Enabled	Warnings	Research, development
stable	Disabled	Strict	Validation, review
onboarding	Disabled	Minimal	New users

---

Distribution

xLaDe is distributed across multiple platforms to reduce reliance on any single provider.

Platform	URL
GitHub (primary)	https://github.com/LakshitSinghBishtTM/xLaDe
GitLab	https://gitlab.com/LakshitSinghBishtTM/xLaDe
Codeberg	https://codeberg.org/lakshitsinghbishttm/xLaDe
Bitbucket	https://bitbucket.org/lakshitsinghbishttm/xlade
Gitea	https://gitea.com/LakshitSinghBishtTM/xLaDe
Sourceforge	https://sourceforge.net/projects/xlade
Website	http://xladeajfgkh32qgq5sj2mtmho3te5pivto7lav44dsbov6uduciz6hqd.onion

The onion service is the official project website, not a mirror or fallback. See ONION.md for the rationale.

Torrent: assets/torrent/xlade_v1.6.0.torrent

magnet:?xt=urn:btih:c51367572a7de7ccf6c80781d4b58c9b085afeb3&xt=urn:btmh:12202868787fb22c69b1f67a056d1608df59fac198a33f3a3e939b539200f4f08771&dn=xLaDe-1.6.0&xl=5449710&tr=udp%3A%2F%2Ftracker.opentrackr.org%3A1337%2Fannounce&tr=udp%3A%2F%2Ftracker.torrent.eu.org%3A451%2Fannounce&tr=udp%3A%2F%2Fopen.stealth.si%3A80%2Fannounce&ws=https://github.com/LakshitSinghBishtTM/xLaDe/archive/refs/tags/v1.6.0.tar.gz

---

Documentation

Document	Objective
INSTALL.md	Installation - elan, Lean, pip, all platforms
docs/WHY_xLaDe.md	The problems in detail and why this approach
docs/CLI_DEMO.md	Every command, with real expected output
docs/END_TO_END_TRACE.md	Full session trace from clone to results
docs/architecture.md	Component boundaries, directory structure, CLI layer
docs/RESEARCH_SCOPE.md	Scope, non-goals, what is permanently out of scope
docs/roadmap.md	Engineering roadmap from v1.5.0 to v2.0.0
docs/research_roadmap.md	Long-term research directions
docs/REPRODUCIBILITY_AND_COMPATIBILITY.md	Reproducibility model and staged plan
LIMITATIONS.md	Honest current limitations
CHANGELOG.md	Full version history
HOW_TO_READ_THIS_REPO.md	Where to start for new contributors

---

Repository Structure

xLaDe/
├── .github/           CI - tests, kernel protection, mirrors
├── experiments/       Ecosystem experiments (directory name = experiment ID)
├── xlade/             Python CLI package
│   ├── cli/           
│   └── core/          
├── scripts/           Policy enforcement shell scripts
├── modes/             Mode definitions (experimental / stable / onboarding)
├── policies/          Governance documents
├── metrics/           Research artifact files
├── security/          Threat model, trust model, security policy
├── tests/             Comprehensive test suite
├── lean-core/         Lean 4 submodule (immutable)
├── docs/              All documentation
├── pyproject.toml     Python packaging
├── lean-toolchain     Pinned Lean compiler version
└── VERSION            Current version

---

Security

xLaDe operates under a minimal-trust model. No single platform is treated as inherently trustworthy.

• security/SECURITY.md - how to report vulnerabilities
• security/THREAT_MODEL.md - what is and is not in scope
• security/TRUST_MODEL.md - distribution trust model
• security/SECURITY_POLICY.md - security philosophy

---

Contributing

Contributions are welcome - experiments, documentation, tooling, tests, and feedback at any stage of development.

• CONTRIBUTING.md - how to contribute
• CODE_OF_CONDUCT.md - community standards
• CONTRIBUTORS.md - acknowledgements

Contributions that modify the Lean kernel are not accepted. This is not a policy that will change.

---

Status

xLaDe is experimental. It is a research tool, not production software. No stability guarantees, no backward compatibility guarantees, no support SLA.

As of v1.6.0:

• CLI tool improved massively
• CI and CD added and integrated
• A comprehensive suite with 83 tests

---

License

Copyright (C) 2026 Lakshit Singh Bisht

Licensed under the GNU General Public License v3.0. See LICENSE for full terms.

This project depends on Lean 4, licensed under the Apache License 2.0, included unmodified as a Git submodule.

---

Developer Note

Thank you for taking the time to read this documentation.

xLaDe is still experimental and continues to evolve with every release. If you have ideas, feedback, criticisms, or would like to contribute, we would be happy to hear from you.

Every contribution, suggestion, bug report, and discussion helps make the project better.