feat: formalize slot_is_justifiable_after in Lean4

.github/workflows/ci.yml

@@ -24,7 +24,7 @@ jobs:
       - uses: actions/checkout@v6
 
       - name: Setup Rust
-        uses: dtolnay/rust-toolchain@master
+        uses: dtolnay/rust-toolchain@stable
         with:
           toolchain: "1.92.0"
           components: rustfmt, clippy
@@ -36,10 +36,10 @@ jobs:
         run: cargo fmt --all -- --check
 
       - name: Cargo check
-        run: cargo check --workspace --all-targets
+        run: cargo check --workspace --all-targets --exclude ethlambda-lean-ffi
 
       - name: Clippy
-        run: cargo clippy --workspace --all-targets -- -D warnings
+        run: cargo clippy --workspace --all-targets --exclude ethlambda-lean-ffi -- -D warnings
 
   test:
     name: Test
@@ -54,7 +54,7 @@ jobs:
 
       - name: Cache test fixtures
         id: cache-fixtures
-        uses: actions/cache@v4
+        uses: actions/cache@v5
         with:
           path: leanSpec/fixtures
           key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }}
@@ -93,7 +93,7 @@ jobs:
       - name: Cache production keys
         if: steps.cache-fixtures.outputs.cache-hit != 'true'
         id: cache-prod-keys
-        uses: actions/cache@v4
+        uses: actions/cache@v5
         with:
           path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
           key: prod-keys-${{ steps.prod-keys-url.outputs.hash }}
@@ -114,7 +114,7 @@ jobs:
         run: touch leanSpec/fixtures
 
       - name: Setup Rust
-        uses: dtolnay/rust-toolchain@master
+        uses: dtolnay/rust-toolchain@stable
         with:
           toolchain: "1.92.0"
 
@@ -123,3 +123,146 @@ jobs:
 
       - name: Run tests
         run: make test
+
+  lean-build:
+    name: Build Lean
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+
+      - name: Install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache Lake packages
+        uses: actions/cache@v5
+        with:
+          path: |
+            ~/.elan
+            formal/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-
+
+      - name: Fetch Mathlib cache
+        working-directory: formal
+        run: lake exe cache get
+
+      - name: Build both libraries
+        working-directory: formal
+        run: lake build
+
+      - name: Verify zero sorries
+        working-directory: formal
+        run: |
+          if grep -rn "sorry" EthLambda/ EthLambdaProofs/ --include="*.lean"; then
+            echo "::error::Found sorry in Lean sources"
+            exit 1
+          fi
+
+  lean-ffi-test:
+    name: Test with Lean FFI
+    runs-on: ubuntu-latest
+    needs: [lean-build, test]
+    steps:
+      - uses: actions/checkout@v6
+
+      - name: Install system dependencies
+        run: sudo apt-get install -y libc++-dev libc++abi-dev
+
+      - name: Install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      # Reuse the Lake cache from the lean-build job
+      - name: Cache Lake packages
+        uses: actions/cache@v5
+        with:
+          path: |
+            ~/.elan
+            formal/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-
+
+      # Read the pinned leanSpec commit from the Makefile (single source of truth)
+      - name: Get leanSpec pinned commit
+        id: lean-spec
+        run: echo "commit=$(sed -n 's/^LEAN_SPEC_COMMIT_HASH:= *//p' Makefile)" >> $GITHUB_OUTPUT
+
+      # Reuse the fixtures cache from the test job
+      - name: Cache test fixtures
+        id: cache-fixtures
+        uses: actions/cache@v5
+        with:
+          path: leanSpec/fixtures
+          key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }}
+
+      # All fixture generation steps are skipped when the cache hits
+      - name: Checkout leanSpec at pinned commit
+        if: steps.cache-fixtures.outputs.cache-hit != 'true'
+        uses: actions/checkout@v6
+        with:
+          repository: leanEthereum/leanSpec
+          ref: ${{ steps.lean-spec.outputs.commit }}
+          path: leanSpec
+
+      - name: Install uv and Python 3.14
+        if: steps.cache-fixtures.outputs.cache-hit != 'true'
+        uses: astral-sh/setup-uv@v4
+        with:
+          enable-cache: true
+          cache-dependency-glob: "leanSpec/pyproject.toml"
+          python-version: "3.14"
+
+      - name: Sync leanSpec dependencies
+        if: steps.cache-fixtures.outputs.cache-hit != 'true'
+        working-directory: leanSpec
+        run: uv sync --no-progress
+
+      - name: Get production keys URL hash
+        if: steps.cache-fixtures.outputs.cache-hit != 'true'
+        id: prod-keys-url
+        working-directory: leanSpec
+        run: |
+          URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])")
+          HASH=$(echo -n "$URL" | sha256sum | awk '{print $1}')
+          echo "hash=$HASH" >> $GITHUB_OUTPUT
+
+      - name: Cache production keys
+        if: steps.cache-fixtures.outputs.cache-hit != 'true'
+        id: cache-prod-keys
+        uses: actions/cache@v5
+        with:
+          path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
+          key: prod-keys-${{ steps.prod-keys-url.outputs.hash }}
+
+      - name: Download production keys
+        if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true'
+        working-directory: leanSpec
+        run: uv run python -m consensus_testing.keys --download --scheme prod
+
+      - name: Generate test fixtures
+        if: steps.cache-fixtures.outputs.cache-hit != 'true'
+        working-directory: leanSpec
+        run: uv run fill --fork=Devnet --scheme prod -o fixtures -n 2
+
+      - name: Mark fixtures as up-to-date
+        run: touch leanSpec/fixtures
+
+      - name: Setup Rust
+        uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: "1.92.0"
+          components: clippy
+
+      - name: Setup Rust cache
+        uses: Swatinem/rust-cache@v2
+
+      - name: Clippy (lean-ffi)
+        run: cargo clippy -p ethlambda-lean-ffi -- -D warnings
+
+      - name: Test with lean-ffi
+        run: cargo test --workspace --release --features lean-ffi

CLAUDE.md

@@ -35,6 +35,10 @@ crates/
     └─ rpc/                 # Axum HTTP: API server + metrics server (independent ports)
   storage/                  # RocksDB backend, in-memory for tests
     └─ src/api/             # StorageBackend trait + Table enum
+formal/                     # Lean 4 formal verification (see formal/README.md)
+  EthLambda/                # Implementation lib (no Mathlib, compiled into binary via FFI)
+  EthLambdaProofs/          # Proofs lib (Mathlib, verification only)
+  lean-ffi/                 # Rust FFI crate (builds Lean C IR, links leanrt)
 ```
 
 ## Key Architecture Patterns
@@ -90,6 +94,28 @@ make run-devnet                                          # Run local devnet with
 
 See `.claude/skills/test-pr-devnet/SKILL.md` for multi-client devnet testing workflows.
 
+## Formal Verification
+
+Lean 4 proofs live in `formal/`. Two libraries: `EthLambda` (implementation, no Mathlib) and
+`EthLambdaProofs` (theorems, uses Mathlib). See `formal/README.md` for details.
+
+### Building
+```bash
+make formally-verify                         # Build both Lean libraries
+```
+
+### Lean FFI
+The `lean-ffi` Cargo feature replaces Rust implementations with formally verified Lean code
+via C FFI. The Lean runtime is statically linked (+2 MB binary size).
+
+```bash
+cargo build --features lean-ffi              # Use verified Lean implementation
+cargo test --features lean-ffi               # Run all tests through Lean
+```
+
+The feature flag threads through `ethlambda` → `ethlambda-blockchain` → `ethlambda-state-transition`.
+Without it, the native Rust implementation is used and no Lean toolchain is needed.
+
 ## Important Patterns & Idioms
 
 ### Trait Implementations

Cargo.toml

@@ -14,6 +14,7 @@ members = [
     "crates/net/p2p",
     "crates/net/rpc",
     "crates/storage",
+    "formal/lean-ffi",
 ]
 
 [workspace.package]
@@ -38,6 +39,7 @@ ethlambda-network-api = { path = "crates/net/api" }
 ethlambda-p2p = { path = "crates/net/p2p" }
 ethlambda-rpc = { path = "crates/net/rpc" }
 ethlambda-storage = { path = "crates/storage" }
+ethlambda-lean-ffi = { path = "formal/lean-ffi" }
 
 tracing = "0.1"
 thiserror = "2.0.9"
@@ -68,9 +70,15 @@ vergen-git2 = { version = "9", features = ["rustc"] }
 
 rand = "0.9"
 rocksdb = "0.24"
-reqwest = { version = "0.12", default-features = false, features = ["rustls-tls"] }
+reqwest = { version = "0.12", default-features = false, features = [
+    "rustls-tls",
+] }
 eyre = "0.6"
 
 # Allocator + heap profiling
-tikv-jemallocator = { version = "0.6", features = ["stats", "unprefixed_malloc_on_supported_platforms", "profiling"] }
+tikv-jemallocator = { version = "0.6", features = [
+    "stats",
+    "unprefixed_malloc_on_supported_platforms",
+    "profiling",
+] }
 jemalloc_pprof = { version = "0.8", features = ["flamegraph"] }

Makefile

@@ -1,4 +1,4 @@
-.PHONY: help fmt lint docker-build run-devnet test
+.PHONY: help fmt lint docker-build run-devnet test formally-verify
 
 help: ## 📚 Show help for each of the Makefile recipes
 	@grep -E '^[a-zA-Z0-9_-]+:.*?## .*$$' $(MAKEFILE_LIST) | sort | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'
@@ -11,7 +11,10 @@ lint: ## 🔍 Run clippy on all workspace crates
 
 test: leanSpec/fixtures ## 🧪 Run all tests
 	# Tests need to be run on release to avoid stack overflows during signature verification/aggregation
-	cargo test --workspace --release
+	cargo test --workspace --release --exclude ethlambda-lean-ffi
+
+formally-verify: ## 🔬 Build and verify Lean formal proofs
+	cd formal && lake exe cache get && lake build
 
 GIT_COMMIT=$(shell git rev-parse HEAD)
 GIT_BRANCH=$(shell git rev-parse --abbrev-ref HEAD)

README.md

@@ -6,10 +6,23 @@ Minimalist, fast and modular implementation of the Lean Ethereum client written
 
 ### Prerequisites
 
+**Using [Nix](https://github.com/DeterminateSystems/nix-installer?tab=readme-ov-file#install-determinate-nix) (recommended):**
+
+```sh
+nix develop                  # interactive shell (bash)
+nix develop -c zsh           # interactive shell (zsh)
+nix develop -c cargo build   # run a single command
+```
+
+This provides Rust, Lean 4, and all other dependencies. No manual installation needed.
+
+**Manual installation:**
+
 - [Rust](https://rust-lang.org/tools/install)
 - [Git](https://git-scm.com/install)
 - [Docker](https://www.docker.com/get-started)
 - [yq](https://github.com/mikefarah/yq#install)
+- [elan](https://github.com/leanprover/elan) (for formal verification / `--features lean-ffi`)
 
 ### Building and testing
 
@@ -28,6 +41,19 @@ make docker-build DOCKER_TAG=local
 
 Run `make help` or take a look at our [`Makefile`](./Makefile) for other useful commands.
 
+### Formal verification
+
+Key consensus functions have been [formally verified in Lean 4](./formal/README.md).
+The verified implementations can be compiled into the binary via FFI:
+
+```sh
+cargo build --features lean-ffi   # use verified Lean implementation
+cargo test --features lean-ffi    # run tests through Lean
+```
+
+This requires Lean 4 (provided by `nix develop` or [elan](https://github.com/leanprover/elan)).
+Without the feature flag, the native Rust implementation is used.
+
 ### Running in a devnet
 
 To run a local devnet with multiple clients using [lean-quickstart](https://github.com/blockblaz/lean-quickstart):

bin/ethlambda/Cargo.toml

@@ -34,3 +34,6 @@ tikv-jemallocator.workspace = true
 
 [build-dependencies]
 vergen-git2.workspace = true
+
+[features]
+lean-ffi = ["ethlambda-blockchain/lean-ffi"]

crates/blockchain/Cargo.toml

@@ -1,3 +1,6 @@
+[features]
+lean-ffi = ["ethlambda-state-transition/lean-ffi"]
+
 [package]
 name = "ethlambda-blockchain"
 authors.workspace = true

crates/blockchain/state_transition/Cargo.toml

@@ -9,9 +9,13 @@ repository.workspace = true
 rust-version.workspace = true
 version.workspace = true
 
+[features]
+lean-ffi = ["dep:ethlambda-lean-ffi"]
+
 [dependencies]
 ethlambda-types.workspace = true
 ethlambda-metrics.workspace = true
+ethlambda-lean-ffi = { workspace = true, optional = true }
 
 thiserror.workspace = true
 tracing.workspace = true