feat: add formal verification — Lean 4 soundness proofs + proptest for permission lattice

.github/workflows/ci.yml

@@ -54,6 +54,20 @@ jobs:
           components: rustfmt
       - run: cargo fmt --check --all
 
+  lean-proofs:
+    name: Lean 4 Proofs
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install elan
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Regenerate Perm.lean from perms.toml
+        run: python3 proofs/scripts/gen_perm.py
+      - name: Build and verify proofs
+        run: cd proofs && lake build
+
   capsec-audit:
     name: Capability Audit
     runs-on: ubuntu-latest

Cargo.toml

@@ -8,6 +8,7 @@ members = [
     "crates/cargo-capsec",
     "crates/capsec-tokio",
     "crates/capsec-tests",
+    "crates/capsec-proof",
 ]
 exclude = [
     "crates/capsec-example-db",

crates/capsec-proof/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "capsec-proof"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+publish = false
+description = "Formal verification and property tests for capsec's permission lattice"
+
+[dependencies]
+toml = { workspace = true }
+
+[dev-dependencies]
+proptest = "1"
+toml = { workspace = true }