This table maps formal Lean modules to Rust code and automated checks. Extend it when you add or rename specs, crates, or CI steps.
| Lean module | Role | Rust / tooling | CI (representative) |
|---|---|---|---|
RBAC.Core, RBAC.Proofs, RBAC.ABAC |
RBAC/ABAC semantics | policyengine policy and WASM evaluation; cargo test |
ci-rust.yml |
Tenant.FSM, Tenant.Isolation, Tenant.Integration |
Tenant isolation model | engine integration tests; future conformance tests |
ci-rust.yml |
Attest.* |
Attestation model | engine attestation helpers; attest-verify binary |
ci-rust.yml |
Smoke executables (test_rbac, test_tenant, test_attest) |
Executable smoke coverage | lake exe … |
ci-lean.yml |