# AEGIS — Formal Verification Candidates

- **Document ID:** ARCH-40
- **Phase:** E.2 — Verification Methodology
- **Status:** Draft for review (post four-reviewer discipline)
- **Version:** 0.1
- **Date:** 2026-07-10
- **Owner:** Chief Security Architect

---

## 1. Purpose

Identify which AEGIS subsystems benefit from formal methods and which methods apply. Formal verification is expensive; targeting is the entire game. Implements the assurance-level progression path (ARCH-27) toward L4/L5.

## 2. Selection Criteria

A subsystem is a formal-verification candidate when:
1. It sits on a critical path (compromise → platform-wide impact).
2. It has a small, well-defined state space that a formal model can capture.
3. It has properties that are hard to test exhaustively (concurrent state, invariants across distributed replicas).
4. Its interface is stable enough that a model's investment pays back over years.

## 3. Candidate Register

| Candidate | Method | Target Level | Priority | Debt Register |
|---|---|---|---|---|
| **Capability Directory** (Kernel) — attenuation + revocation semantics under concurrency | TLA+ | L4→L5 | 1 | D-S-01 |
| **Kernel Decision Loop** — atomic mediation + audit-first ordering | TLA+ | L4 | 2 | D-S-01 |
| **Layer-A hash-chain per-instance** — monotonicity + prev-hash correctness across restart | TLA+ + property tests | L4 | 3 | D-S-01 |
| **Watchdog Quorum** — decision protocol + alarm invariants | TLA+ | L4 | 4 | D-S-01 |
| **Ed25519 signing hot path** (Rust) — no unsafe UB; contract adherence | CBMC / Prusti | L4 | 5 | new |
| **Capability token encoding/decoding** (Rust) — no panic + length correctness | Prusti + fuzz | L4 | 6 | new |
| **Recovery Integrity Attestation** — five-question invariants + signature composition | TLA+ | L4 | 7 | D-S-01 |
| **Redaction pipeline invariants** — no-secret-in-output; canary property | Property tests + partial modelling | L3 | 8 | new |

## 4. Pilot Roadmap

- **v0-GA + Q1.** Set up TLA+ tooling; pilot on Capability Directory (candidate 1).
- **v0.2.** Extend to Kernel Decision Loop.
- **v1.** Watchdog Quorum + Layer-A hash-chain modeling.
- **v1.5.** Rust hot-path formal analysis (candidates 5-6).
- **v2.** Recovery Attestation modeling.

Each pilot produces: model, checked invariants, counterexamples (if any), and a report referenced by the Verification Matrix (ARCH-37).

## 5. What Formal Methods Do NOT Cover

- Implementation ≠ model. Even a checked model can be violated by an implementation bug. Formal analysis complements (not replaces) property tests and fuzz.
- Model boundaries capture designed invariants; environmental compromise (side channels, supply chain) is out of scope.

## 6. Skills and Sustainability

- Team upskilling: TLA+ workshop; Rust-Prusti training.
- External consultation for initial pilots.
- Documented model style guide to reduce reviewer burden.

## 7. Independent Architecture Review

- **F-1.** *Formal methods are expensive vs. ROI.* Prioritized to highest-impact candidates; other subsystems rely on property tests + red team.
- **F-2.** *Models drift from implementation.* Model diffs required per Kernel architecture change; ADR references model version.

## 8. Adversarial Architect Review

- **A-1.** *Attacker exploits a corner not modeled.* Model boundaries documented; residual risk owned; compensating controls named.
- **A-2.** *Insider approves a model with missing invariants.* Two-approver on model + external review.

## 9. Operational Reliability Review

- **O-1.** Sustainability: initial investment amortized over 15 years.
- **O-2.** Model runs incorporated into CI; regressions block.
- **O-3.** Onboarding covers model interpretation.

## 10. Self-Critique

- **S-1.** *8 candidates may be too ambitious; 3 is realistic for v0-v1.* Priority column reflects; over-scope moved to roadmap.
- **S-2.** *TLA+ has a learning curve.* Explicit training budget; external help until team ready.

## 11. First-Target Analysis and Redesign

**Target:** the model itself. A formal model that looks right but has a subtle omission gives false confidence. **Response:** model peer review + external review at first + intentional counterexample tests (verify the model can produce a counterexample when constraints relaxed).

## 12. Decisions

### D-40-1. Prioritized formal-methods candidate register with pilot roadmap

- **Reason.** Assurance L4→L5 path per ARCH-27 for Kernel-critical subsystems.

## 13. Change Log

- **0.1 (2026-07-10)** — Initial draft.