This repository ties together machine-checked specifications (Lean 4), a Rust policy engine with a Wasmtime evaluation path, Python tooling for compliance bundles and linting, and optional Go, Node, and Python bindings. Continuous integration runs formatters, tests, and supply-chain gates so the default branch stays reproducible and reviewable.

These are the outcomes the codebase is organized around. All are active development areas—not a maturity matrix.

For a full component list and CI gate mapping, see docs/ARCHITECTURE.md.

flowchart TB
  subgraph spec["Formal layer — Lean"]
    RBAC["RBAC / ABAC"]
    TEN["Tenant FSM and isolation"]
    ATT["Attestation model"]
  end

  subgraph rt["Runtime — Rust"]
    PE["policyengine"]
    WASM["Wasmtime"]
  end

  subgraph tools["Tooling"]
    GEN["bundle/gen.py"]
    VAL["validate_manifest.py"]
    LINT["policy_lint.py"]
  end

  subgraph bind["Bindings"]
    B["Go · Node · Python"]
  end

  RBAC --> PE
  TEN --> PE
  ATT --> PE
  PE --> WASM
  PE --> GEN
  GEN --> VAL
  PE --> bind
  LINT -.-> PE

Pinned toolchains: lean-toolchain, rust-toolchain.toml.

git clone https://github.com/your-username/security-envelopes.git
cd security-envelopes

# Lean (one-time)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Rust (one-time)
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

pip install -e ".[dev]"

lake build
cargo build --release

Run the same categories of checks CI exercises:

# Lean smoke executables (see lakefile.lean)
lake exe test_rbac && lake exe test_tenant && lake exe test_attest

# Rust
cargo fmt --check
cargo clippy --workspace --all-targets -- -D warnings
cargo test --workspace

# Python
ruff check bundle scripts tests
pytest tests/ -v

# Optional locally; required in CI for Rust changes affecting deps
cargo deny check
cargo audit

Example policies — examples/ (e.g. examples/01_simple_rbac/policy.yaml):

python scripts/policy_lint.py examples/*/policy.yaml

CLI entry points (from repo root):

cargo run -p policyengine --bin rbac-gen -- --help
cargo run -p policyengine --bin attest-verify -- --help
python bundle/gen.py --help

There is no bundled examples/go/main.go; wire your own tests against the crates and bindings you need.

Contributing guidelines, pre-commit, and review expectations: CONTRIBUTING.md.

Vulnerability reporting and supply-chain notes: SECURITY.md.

Treat latency and scale figures as deployment-specific until you measure them in your environment and record results in benchmarks or release notes.

MIT.

Lean, the Rust project, Wasmtime, mathlib, and everyone building open, verifiable systems.