[todie]

Summary

• Lands SPEC-0002 detailing the formal Proof-Carrying Code (PCC) model for policy gates.
• Formalizes state transition invariant preservation: $(I(S) \wedge \text{Exec}(S, a, S')) \implies I(S')$.
• Defines the decoupling between out-of-band Gödel provers (e.g. Lean 4 / Z3) and the zero-I/O $O(1)$ AST proof-checking kernel in gs-domain.
• Enforces permissions immutability and fail-closed lattice semantics.
• Updates README to index SPEC-0002.

Verification

• cargo fmt --all -- --check passed.
• cargo clippy --workspace --all-targets -j 2 -- -D warnings passed.
• cargo test --workspace -j 2 passed (7 tests in gs-domain).

Co-authored-by: Kratos kratos@yx.unsigned.gg
Reviewed-by: Mimir mimir@unsigned.gg