From a43a070ce788db8df61494aa3d871d457ff2d074 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sun, 14 Jun 2026 14:44:37 +0000
Subject: [PATCH] ci(lean): add Lean proof gate (lake build) guarding the
 metatheory

There was no Lean CI anywhere in the estate, so the mechanized proofs
(type safety, Sandbox Isolation Thm 1, Capability Soundness Thm 2,
Ethical Verdict Consistency, BFT quorum-intersection Thm 3) were
unguarded against regression. This gate runs `lake build` on every
push/PR via leanprover/lean-action (SHA-pinned v1.5.0), building
academic/formal-verification/lean4/ on core Lean (no Mathlib, no
test/lint targets). A broken proof now fails CI.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS
---
 .github/workflows/lean.yml | 46 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 .github/workflows/lean.yml

diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
new file mode 100644
index 0000000..17ee9f1
--- /dev/null
+++ b/.github/workflows/lean.yml
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: MPL-2.0
+# lean.yml — build + verify the Phronesis Lean 4 metatheory on every push/PR.
+#
+# Guards the mechanized proofs against regression. `lake build` typechecks the
+# whole development (a broken proof fails the build):
+#   * type safety       — progress / preservation / determinism
+#   * Sandbox Isolation  (safety_proofs.md Theorem 1)
+#   * Capability Soundness (Theorem 2) + Ethical Verdict Consistency
+#   * BFT quorum-intersection safety (Theorem 3)
+# Core Lean only (no Mathlib): the toolchain pinned in
+# academic/formal-verification/lean4/lean-toolchain is all CI needs.
+name: Lean Proofs
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+  workflow_dispatch:
+
+# Estate guardrail: cancel superseded runs (read-only check, safe to cancel).
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  lean:
+    name: Build Lean metatheory (lake build)
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      # Installs elan + the toolchain from lean-toolchain, then runs `lake build`.
+      # No test/lint targets and no Mathlib in this project, so those are off.
+      - name: Build + verify Lean proofs
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+        with:
+          lake-package-directory: academic/formal-verification/lean4
+          build: "true"
+          test: "false"
+          lint: "false"
+          use-mathlib-cache: "false"