# Formal Methods Plan

Goal: move from model checking to machine-checked proofs for the core lattice
and nucleus (`ν`) properties, while keeping the spec small and auditable.

## Scope (initial)
- Permission lattice order and join/meet.
- Nucleus `ν` (normalization) laws:
  - Idempotent: ν(ν(x)) = ν(x)
  - Monotone: x ≤ y ⇒ ν(x) ≤ ν(y)
  - Deflationary: ν(x) ≤ x
-  Uninhabitable state obligations as a derived constraint.

## Plan
1. **Lean 4 spec** of the lattice structure and ν (small, pure model).
2. **Proofs** of ν laws + meet/join compatibility (minimal theorem set).
3. **Traceability**: map each Rust field to the spec with a short “spec ↔ code”
   reference table.
4. **CI gate** for proof check (separate job; fails on proof regressions).

## What Kani Covers (and doesn’t)
- Kani is used for bounded model checking on Rust implementations.
- Kani runs as a nightly CI job; merge gating is planned once proofs stabilize.
- Kani **does not** replace theorem proving; it complements the proof layer.

## Non-goals (initial)
- Full refinement proofs from Rust to Lean.
- End-to-end OS isolation proofs.
