# Architecture

Security Envelopes combines formal specifications, a Rust policy runtime, and tooling to produce audit-oriented artifacts.

## Data flow

```mermaid
flowchart LR
  subgraph spec [Formal layer]
    Lean[Lean specs in Spec]
  end
  subgraph runtime [Runtime]
    Engine[policyengine crate]
    Wasm[Wasmtime evaluation]
  end
  subgraph tools [Tooling]
    Bundle[bundle/gen.py]
    Manifest[manifest.json]
  end
  Lean --> Bundle
  Engine --> Wasm
  Engine --> Bundle
  Bundle --> Manifest
```

## Components

| Layer | Location | Responsibility |
|-------|----------|----------------|
| Specifications | `Spec/` | RBAC/ABAC, tenant FSM, attestation models in Lean (Mathlib) |
| Engine | `engine/` (`policyengine`) | Policy loading, WASM sandbox, crypto, attestation verification |
| Compliance bundle | `bundle/` | Zip layout, hashes, optional signing, PDF paths |
| Bindings | `bindings/{go,node,python}/` | Language shims; native builds are opt-in per platform |

## CI gates

Workflows live under [`.github/workflows/`](../.github/workflows/). Typical gates:

| Area | Checks | Workflow file |
|------|--------|----------------|
| Rust | `fmt`, `clippy` (`-D warnings`), `test`, `cargo audit`, `cargo deny`, release binaries, WASM smoke | [`ci-rust.yml`](../.github/workflows/ci-rust.yml) |
| Lean | `lake build`, `lake exe test_rbac`, `test_tenant`, `test_attest` | [`ci-lean.yml`](../.github/workflows/ci-lean.yml) |
| Python | `ruff`, `mypy` (scoped paths), `pytest` | [`ci-python.yml`](../.github/workflows/ci-python.yml) |
| Policy YAML | `scripts/policy_lint.py` on `examples/` | [`policy-lint.yml`](../.github/workflows/policy-lint.yml) |
| Security (scheduled) | `cargo audit`, `cargo deny` | [`ci-security.yml`](../.github/workflows/ci-security.yml) |
| SBOM | CycloneDX JSON artifact (Anchore action) | [`ci-sbom.yml`](../.github/workflows/ci-sbom.yml) |
| CodeQL | Rust analysis | [`codeql.yml`](../.github/workflows/codeql.yml) |
| Bindings | `go test`, `cargo check` for Node/Python crates | [`ci-bindings-go.yml`](../.github/workflows/ci-bindings-go.yml), [`ci-bindings-node.yml`](../.github/workflows/ci-bindings-node.yml), [`ci-bindings-python.yml`](../.github/workflows/ci-bindings-python.yml) |

For Lean-to-code traceability, see [TRACEABILITY.md](../TRACEABILITY.md).