# Council Design Brief: Formal Verification

**Council ID:** `council-verify`  
**Mission:** Provide rigorous, machine-checked correctness guarantees for every DistOS subsystem specification. This council does not design subsystems — it proves them correct, identifies flaws in proposed designs, and returns actionable verification results with enough precision that authoring councils can fix their specifications without ambiguity.  
**UCXL Base Address:** `ucxl://council-verify:*@DistOS:verification/*`  
**Agent Count:** ~80  
**Status:** Design Brief — Constitution Phase

---

## 1. Scope and Responsibilities

`council-verify` owns the formal correctness layer of DistOS. Its scope covers:

- Accepting formal specifications (TLA+, Alloy, Coq, Lean) from all six core subsystem councils and from `council-api` and `council-fault`
- Writing model-checking harnesses for TLC and Alloy Analyzer against those specifications
- Specifying and checking safety properties: mutual exclusion, absence of deadlock, freedom from starvation, bounded wait times, and memory safety invariants
- Specifying and checking liveness properties: progress, termination, fairness under weak and strong fairness assumptions
- Constructing refinement mappings that relate abstract protocol specs to concrete implementation-level descriptions
- Verifying compositional properties: establishing that subsystem specs verified in isolation remain correct when composed
- Managing state-space explosion via symmetry reduction, partial-order reduction, abstraction, and bounded verification
- Producing structured verification reports that link every proved or falsified property back to the subsystem artifact that claimed it
- Maintaining a central registry of verified invariants so `council-synth` can detect when a cross-council design change invalidates a previously proved property

Responsibilities this council does **not** own: designing or modifying the subsystems themselves; producing human-readable narrative (that belongs to `council-docs` and `council-arch`); adversarial test case generation (owned by `council-qa`).

---

## 2. Research Domains

### 2.1 TLA+ Specification Language and TLC Model Checker

TLA+ (Temporal Logic of Actions, Lamport 1994) remains the most widely deployed formal specification language in industrial distributed systems. Agents must understand the full TLA+ grammar including action formulas, temporal operators (`[]`, `<>`, `~>`, `ENABLED`), refinement (`INSTANCE` with substitution), and the TLAPS proof system for machine-checked TLA+ proofs beyond TLC's exhaustive checking.

Key references:
- Lamport, L. *Specifying Systems* (2002). Addison-Wesley. The definitive text. Chapters 14–16 on liveness and fairness are mandatory reading.
- Lamport, L. *The TLA+ Toolbox* (2019). Formal Aspects of Computing 31(4).
- Newcombe, C. et al. "How Amazon Web Services Uses Formal Methods." *Communications of the ACM* 58(4), 2015. Documents TLA+ specs for DynamoDB (conditional writes, leader election), S3 (replication, bucket visibility), and EBS (volume attachment). Directly relevant because the DistOS storage layer shares fault-tolerance requirements with S3.
- Lebresne, S. and Bonnet, R. "A TLA+ specification for Raft." 2015. Reference implementation at `github.com/ongardie/raft.tla`. Agents should study how the spec handles log compaction and leader completeness.
- Helland, P. "Raft-TLA walk-through." AWS Builder's Library, 2023. Useful for understanding how abstract specs relate to actual implementations.

Agents must be fluent in the distinctions between safety (`[]P`) and liveness (`<>P`, `P ~> Q`) properties in the context of distributed system specs, and must understand that TLC can verify safety exhaustively for small models and liveness only under fairness assumptions.

### 2.2 Alloy Structural Modelling

Alloy (Jackson 2002) provides relational modelling with automatic satisfiability checking via the Alloy Analyzer (Kodkod back-end). It is better suited than TLA+ for verifying structural invariants: capability lattice consistency, access control policy completeness, and message schema constraints.

Key references:
- Jackson, D. *Software Abstractions: Logic, Language, and Analysis* (2nd ed., 2012). MIT Press. Chapters 5–7 on relational logic and the Alloy language.
- Jackson, D. "Alloy: A Lightweight Object Modelling Notation." *ACM Transactions on Software Engineering and Methodology* 11(2), 2002.
- Dennis, G. et al. "Modular Verification of Code with SAT." *ISSTA 2006*. Covers compositional use of Alloy for modular systems — directly applicable to per-council specs.

Alloy is the preferred tool for `council-sec`'s capability model and `council-api`'s interface contracts.

### 2.3 Theorem Proving with Coq and Lean

For critical invariants where exhaustive model checking is infeasible (infinite state spaces, parameterised proofs over arbitrary numbers of nodes), mechanical theorem proving is required. The two target systems are:

- **Coq** (v8.18+): mature ecosystem, extensive libraries (Mathematical Components, Iris for concurrent separation logic). Used in seL4 verification (Klein et al., *SOSP 2009*, "seL4: Formal Verification of an OS Kernel" — the only OS kernel with a full functional correctness proof in Isabelle/HOL; agent teams should study the proof methodology even though DistOS does not target Isabelle).
- **Lean 4**: newer, strong dependent type theory, mathlib. Agents should be aware of Lean's advantages for mathematical specifications and its growing industrial use.

Key references:
- Klein, G. et al. "seL4: Formal Verification of an OS Kernel." *SOSP 2009*.
- Hawblitzel, C. et al. "IronFleet: Proving Practical Distributed Systems Correct." *SOSP 2015*. IronFleet verified a Paxos-based key-value store end-to-end in Dafny (a close relative of the Lean/Coq family). The methodology — writing code in a verifiable subset and discharging proof obligations automatically — is the architectural target for DistOS's critical paths.
- Hawblitzel, C. et al. "IronClad Apps: End-to-End Security via Automated Full-System Verification." *OSDI 2014*. Companion work on security verification.
- Jung, R. et al. "Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning." *POPL 2015*. Iris is the preferred logic for reasoning about concurrent OS code in Coq.

### 2.4 Safety Properties in Distributed Systems

Agents must be able to specify and check the following safety properties across all subsystems:

- **Mutual exclusion:** No two agents hold a critical resource simultaneously. Expressed as `[](~(hold(a) /\ hold(b)))` for agents a, b.
- **Deadlock freedom:** The system never reaches a state where no process can advance. In TLA+: `[][ENABLED(Next)]_vars`.
- **Starvation freedom:** Every process that repeatedly requests a resource eventually obtains it. A liveness property requiring a fairness assumption.
- **Memory safety invariants:** No node accesses memory beyond its allocated region. Requires coupling the memory council's allocation spec with an invariant expressed over the allocated-region relation.
- **Invariant stability under node failure:** Safety properties must hold even when `f` nodes fail for the declared failure threshold `f`.

Key references:
- Alpern, B. and Schneider, F. "Defining Liveness." *Information Processing Letters* 21(4), 1985. Foundational paper establishing the safety/liveness dichotomy.
- Lamport, L. "Proving the Correctness of Multiprocess Programs." *IEEE Transactions on Software Engineering* 3(2), 1977.

### 2.5 Liveness Properties: Progress, Termination, and Fairness

Liveness verification is harder than safety because it requires reasoning about infinite behaviours. Key concepts:

- **Weak Fairness (WF):** If an action is continuously enabled, it eventually fires.
- **Strong Fairness (SF):** If an action is repeatedly enabled, it eventually fires.
- **Progress:** Every submitted job eventually completes (relevant to `council-sched`).
- **Termination:** Every protocol run terminates (relevant to consensus in `council-fault`).
- **Wait-freedom:** Every operation completes in a bounded number of steps regardless of other processes. The strongest liveness property; not required everywhere but should be analysed for critical paths.

Fairness assumptions must be documented explicitly in every spec. Agents must flag any property that relies on strong fairness, as this is a non-trivial assumption in distributed systems with Byzantine participants.

### 2.6 Refinement Mappings

A refinement mapping demonstrates that a concrete spec `C` correctly implements an abstract spec `A`. In TLA+, this is expressed as `C ≡ A(f)` where `f` is a state function mapping `C`-variables to `A`-variables. Verification of refinement requires showing that every behaviour of `C` is a behaviour of `A(f)`.

Key references:
- Lamport, L. "The Temporal Logic of Actions." *ACM Transactions on Programming Languages and Systems* 16(3), 1994.
- Abadi, M. and Lamport, L. "The Existence of Refinement Mappings." *Theoretical Computer Science* 82(2), 1991. Establishes when refinement mappings exist.

Every subsystem spec must provide two levels: an abstract protocol-level spec (suitable for human understanding and compositional reasoning) and a concrete implementation-level spec (suitable for derivation of data structures and algorithms). `council-verify` is responsible for verifying that the refinement mapping holds.

### 2.7 Compositional Verification

Verifying subsystems independently and then proving the composed system correct is the only tractable approach at scale. Key techniques:

- **Assume-Guarantee reasoning (A-G):** Each module assumes a guarantee from its environment and guarantees a property to its users. The composition is correct if each module's guarantee satisfies the next module's assumption.
- **Interface specifications:** Every cross-council interface must have a formal spec of its pre/post conditions before compositional verification can proceed.

Key references:
- McMillan, K. "Circular Compositional Reasoning About Liveness." *CHARME 1999*.
- Henzinger, T. et al. "Assume-Guarantee Reasoning for Hierarchical Hybrid Automata." *HSCC 2001*.

`council-verify` will maintain an interface contract registry. Any subsystem change that violates an interface contract triggers an immediate verification task.

### 2.8 Distributed Systems Verification: Linearizability and Consistency Models

Subsystem specs must state their consistency model explicitly. `council-verify` verifies the stated model against the protocol spec:

- **Linearizability:** Each operation appears to take effect atomically at a single point between invocation and response (Herlihy and Wing, *JACM 1990*).
- **Sequential consistency:** Operations appear in a total order consistent with each process's program order.
- **Causal consistency:** Causally related operations appear in causal order.
- **Eventual consistency:** Replicas converge to the same value in the absence of updates.

Key references:
- Herlihy, M. and Wing, J. "Linearizability: A Correctness Condition for Concurrent Objects." *ACM Transactions on Programming Languages and Systems* 12(3), 1990.
- Burckhardt, S. *Principles of Eventual Consistency* (2014). Microsoft Research TR. Systematic treatment of consistency models using execution graphs.
- Attiya, H. and Welch, J. *Distributed Computing: Fundamentals, Simulations, and Advanced Topics* (2nd ed., 2004). Reference for correctness conditions.
- Viotti, P. and Vukolić, M. "Consistency in Non-Transactional Distributed Storage Systems." *ACM Computing Surveys* 49(1), 2016. Comprehensive taxonomy of 50+ consistency models.

### 2.9 State Space Explosion Management

Model checking hits combinatorial explosion rapidly for distributed systems. Agents must be competent in:

- **Symmetry reduction:** Exploiting permutation symmetry among identical nodes to collapse the state space. TLC's `Symmetry` clause.
- **Partial-order reduction:** Avoiding redundant interleavings of independent actions. Implemented in SPIN; partial support in TLC via action fairness.
- **Abstraction and data abstraction:** Replacing concrete data types with abstract types that preserve the relevant structure.
- **Bounded verification:** Verifying safety for small model sizes (e.g., 3 nodes, 5 messages) and using induction for the general case.
- **Counterexample-guided abstraction refinement (CEGAR):** Automatically refining abstractions when spurious counterexamples are found.

Key references:
- Clarke, E. et al. *Model Checking* (1999). MIT Press. The canonical textbook.
- Holzmann, G. *The SPIN Model Checker* (2003). Addison-Wesley.
- Clarke, E. et al. "Counterexample-Guided Abstraction Refinement." *CAV 2000*.

### 2.10 GPU Memory Model Formal Verification

NVIDIA has published formal verification work on the GPU memory model — a requirement given that DistOS targets Hopper, Grace, and Blackwell architectures:

- Alglave, J. et al. "GPU Concurrency: Weak Behaviours and Programming Assumptions." *ASPLOS 2015*. Establishes the formal framework for GPU memory models using axiomatic models.
- Lustig, D. et al. "Automated Synthesis of Comprehensive Memory Model Litmus Test Suites." *ASPLOS 2017*.
- NVIDIA. "NVIDIA Hopper Architecture In-Depth." 2022. Section on memory consistency model for NVLink and NVSwitch fabrics.
- Wickerson, J. et al. "Automatically Comparing Memory Consistency Models." *POPL 2017*.

`council-verify` must verify that the `council-mem` memory model specification is consistent with the Hopper/Blackwell hardware memory model documented by NVIDIA.

### 2.11 Industrial Case Studies

Agents must study these deployments to calibrate what is achievable in 14 days:

- **Amazon Web Services TLA+ usage:** DynamoDB (conditional writes, leader election), S3 (replication), EBS, internal lock manager. Newcombe et al. 2015 (cited above) documents 14 specs found 10 bugs that other methods missed.
- **CockroachDB:** Published TLA+ specs for their Parallel Commits protocol at `github.com/cockroachdb/cockroach/tree/master/docs/tech-notes`. Model of their 2PC variant demonstrating absence of deadlock.
- **etcd/Raft:** Formal verification via TLC. Howard, H. "Flexible Paxos: Quorum Intersection Revisited." 2016. Extends Raft's quorum reasoning.
- **IronFleet** (Microsoft Research): End-to-end verified distributed system using Dafny. The most directly relevant existence proof that full-stack distributed system verification is feasible.

---

## 3. Agent Roles

| Role | Count | Responsibilities |
|------|-------|-----------------|
| Lead Verifier | 1 | Coordinates the council; assigns verification tasks; maintains the invariant registry; escalates to `council-synth` when a falsified property implicates another council |
| TLA+ Specialists | 20 | Write TLA+ specs and TLC harnesses for assigned subsystems; drive TLC jobs; interpret counterexamples; write refinement mappings |
| Alloy Modellers | 10 | Write Alloy models for structural invariants (capability lattices, interface schemas, access control); run Alloy Analyzer jobs |
| Theorem Prover Agents | 10 | Handle parameterised proofs in Coq or Lean where exhaustive checking is infeasible; prove inductive invariants for unbounded node counts |
| Liveness Specialists | 8 | Focus exclusively on liveness properties, fairness assumptions, and progress guarantees across all subsystems; track fairness debts |
| Refinement Analysts | 8 | Construct and verify refinement mappings between abstract and concrete specs; maintain the two-level spec contract for each subsystem |
| Compositional Integrators | 8 | Maintain the assume-guarantee decomposition across councils; track interface contract evolution; recheck composed properties when any component changes |
| GPU Memory Model Analysts | 6 | Verify the memory subsystem spec against Hopper/Blackwell hardware memory models; consult Alglave et al. axiomatic framework |
| Verification Report Writers | 9 | Produce structured verification reports in UCXL-addressed artifacts; translate counterexamples into prose that authoring councils can act on |

**Total:** 80 agents

---

## 4. Key Deliverables

All artifacts are addressed using the pattern `ucxl://council-verify:{role}@DistOS:verification/^^/{artifact-type}/{name}`.

### 4.1 Verified Property Registry

A central machine-readable registry mapping every claimed property (safety or liveness) to its verification status (proved, falsified with counterexample, in-progress, deferred), the spec artifact it was verified against, and the TLC/Coq/Alloy job that produced the result.

```
ucxl://council-verify:lead-verifier@DistOS:verification/^^/registries/verified-properties.json
```

### 4.2 Per-Subsystem TLA+ Verification Reports

One verification report per subsystem council. Each report covers: which properties were checked, the model parameters used, verification outcome, any counterexamples with step-by-step traces, and recommended spec fixes.

```
ucxl://council-verify:tla-specialist@DistOS:verification/^^/reports/sched-verification-report.md
ucxl://council-verify:tla-specialist@DistOS:verification/^^/reports/mem-verification-report.md
ucxl://council-verify:tla-specialist@DistOS:verification/^^/reports/net-verification-report.md
ucxl://council-verify:tla-specialist@DistOS:verification/^^/reports/fault-verification-report.md
ucxl://council-verify:tla-specialist@DistOS:verification/^^/reports/sec-verification-report.md
ucxl://council-verify:tla-specialist@DistOS:verification/^^/reports/telemetry-verification-report.md
```

### 4.3 Alloy Structural Models

```
ucxl://council-verify:alloy-modeller@DistOS:verification/^^/specs/capability-lattice.als
ucxl://council-verify:alloy-modeller@DistOS:verification/^^/specs/api-interface-contracts.als
ucxl://council-verify:alloy-modeller@DistOS:verification/^^/specs/memory-region-invariants.als
```

### 4.4 Coq/Lean Theorem Proofs

```
ucxl://council-verify:theorem-prover@DistOS:verification/^^/proofs/consensus-termination.v
ucxl://council-verify:theorem-prover@DistOS:verification/^^/proofs/scheduler-fairness.lean
ucxl://council-verify:theorem-prover@DistOS:verification/^^/proofs/memory-safety-invariant.v
```

### 4.5 Refinement Mapping Documents

```
ucxl://council-verify:refinement-analyst@DistOS:verification/^^/refinements/sched-abstract-to-concrete.md
ucxl://council-verify:refinement-analyst@DistOS:verification/^^/refinements/fault-paxos-to-implementation.md
```

### 4.6 Compositional Verification Summary

The master document proving that the composed DistOS spec (all subsystems together) satisfies the system-level properties enumerated in the Project Constitution.

```
ucxl://council-verify:compositional-integrator@DistOS:verification/^^/reports/compositional-correctness.md
```

### 4.7 GPU Memory Model Conformance Report

```
ucxl://council-verify:gpu-mem-analyst@DistOS:verification/^^/reports/gpu-memory-model-conformance.md
```

---

## 5. Decision Points

The following architectural questions must be resolved by this council in collaboration with the councils noted. Each decision must be recorded as a Decision Record (DR) at the UCXL address pattern `ucxl://council-verify:lead-verifier@DistOS:verification/^^/decisions/{dr-id}.md`.

### DP-V01: Primary Specification Language

Choose between TLA+ (dominant in industry, mature TLC checker), PlusCal (higher-level algorithmic notation that compiles to TLA+), or a hybrid approach. Decision criteria: agent familiarity, tool availability, expressiveness for GPU-specific memory model properties.  
**Deciding parties:** Lead Verifier, TLA+ Specialists, `council-synth`

### DP-V02: Verification Depth vs. Coverage Trade-off

Given 14 days, the council cannot exhaustively verify every subsystem at every level. Decide which subsystems require: (a) full TLC model checking with proved safety and liveness, (b) safety-only checking, (c) Alloy structural check only, (d) manual proof review. Scheduling and fault tolerance subsystems should be candidates for (a).  
**Deciding parties:** Lead Verifier, all specialists, `council-meta`

### DP-V03: Consistency Model for the Memory Subsystem

Must agree with `council-mem` on the stated consistency model before verification can begin. Options: linearizability (strongest, highest cost), sequential consistency, causal consistency, release-acquire (matching hardware), eventual consistency. The choice directly determines which properties are verifiable and which invariants are admissible.  
**Deciding parties:** `council-verify` Refinement Analysts, `council-mem`, `council-synth`

### DP-V04: Fairness Assumption Standard

Establish the minimum fairness assumption that all subsystem specs must satisfy. Options: no fairness (specs must be self-scheduling), weak fairness (WF) on all actions, strong fairness (SF) on specific actions. This decision affects what liveness properties can be claimed system-wide.  
**Deciding parties:** Liveness Specialists, `council-fault`, `council-sched`

### DP-V05: Parameterised Proof Strategy for Node Count

Determine how to handle proofs over arbitrary numbers of nodes (1024 in production) when TLC can only check small models. Options: inductive invariant proofs in Coq (high effort), boundary case analysis (check 3, 5, 7 nodes and argue by symmetry), or use of parameterised model checkers (IC3/PDR via aiger).  
**Deciding parties:** Theorem Prover Agents, `council-fault`

---

## 6. Dependencies on Other Councils

`council-verify` is a downstream consumer of specifications produced by all other councils. It is also an upstream dependency for any council that needs a correctness certificate before proceeding to integration.

| Council | Relationship | What council-verify consumes | What council-verify produces |
|---------|-------------|------------------------------|------------------------------|
| `council-sched` | Bidirectional | TLA+ scheduling protocol spec | Verification report; falsified properties with counterexamples |
| `council-mem` | Bidirectional | Memory model TLA+ spec; consistency model choice | Memory safety verification; GPU model conformance |
| `council-net` | Bidirectional | Network protocol TLA+ spec | Deadlock-freedom and progress reports |
| `council-fault` | Bidirectional | Consensus TLA+ spec (Raft/Paxos variant) | Termination proof; Byzantine resilience analysis |
| `council-sec` | Bidirectional | Capability lattice description; isolation invariants | Alloy structural model verification; capability safety report |
| `council-telemetry` | Consuming | Metering protocol description | Bounded-wait verification for accounting operations |
| `council-api` | Bidirectional | Interface contracts; system call semantics | API contract verification; pre/post condition checking |
| `council-qa` | Collaborative | Conformance test requirements | Verification results that inform test targets |
| `council-synth` | Reporting | Cross-council conflict notifications | Falsification results that trigger conflict resolution |
| `council-docs` | Providing | N/A | Verified invariant statements for inclusion in formal spec document |

**Critical path constraint:** `council-verify` cannot begin checking a subsystem spec until that spec is at least 70% complete. The Phase 2 architecture documents from each council are the minimum viable input.

---

## 7. WHOOSH Configuration

### 7.1 Team Formation

```yaml
council_id: council-verify
display_name: "Formal Verification Council"
target_size: 80
formation_strategy: competency_weighted
required_roles:
  - role: lead-verifier
    count: 1
    persona: systems-analyst
    competencies: [tla-plus, model-checking, distributed-systems, proof-theory]
  - role: tla-specialist
    count: 20
    persona: technical-specialist
    competencies: [tla-plus, tlc, liveness-properties, refinement-mapping]
  - role: alloy-modeller
    count: 10
    persona: technical-specialist
    competencies: [alloy, relational-logic, structural-verification]
  - role: theorem-prover
    count: 10
    persona: technical-specialist
    competencies: [coq, lean4, dependent-types, inductive-proofs]
  - role: liveness-specialist
    count: 8
    persona: technical-specialist
    competencies: [fairness, liveness, progress-guarantees, temporal-logic]
  - role: refinement-analyst
    count: 8
    persona: systems-analyst
    competencies: [refinement-mappings, abstraction, abadi-lamport]
  - role: compositional-integrator
    count: 8
    persona: systems-analyst
    competencies: [assume-guarantee, compositional-reasoning, interface-contracts]
  - role: gpu-mem-analyst
    count: 6
    persona: technical-specialist
    competencies: [gpu-memory-models, hopper-architecture, axiomatic-models]
  - role: verification-report-writer
    count: 9
    persona: technical-writer
    competencies: [technical-writing, counterexample-analysis, verification-reports]
```

### 7.2 Quorum Rules

```yaml
quorum:
  decision_threshold: 0.6          # 60% of active agents must agree
  lead_verifier_veto: true         # Lead Verifier can block any property acceptance
  minimum_specialist_agreement: 3  # At least 3 domain specialists must agree on any claim of "proved"
  falsification_threshold: 1       # A single counterexample from any agent is sufficient to falsify
  cross_council_escalation:
    trigger: falsified_property
    target: council-synth
    response_sla_hours: 4
```

### 7.3 Subchannels

```yaml
subchannels:
  - id: verify-tlaplus-harnesses
    subscribers: [tla-specialist, lead-verifier]
    purpose: "TLC job coordination, model parameter negotiation, counterexample sharing"
    ucxl_feed: "ucxl://council-verify:tla-specialist@DistOS:verification/^^/specs/*.tla"

  - id: verify-alloy-sessions
    subscribers: [alloy-modeller, lead-verifier]
    purpose: "Alloy Analyzer session coordination and structural model review"
    ucxl_feed: "ucxl://council-verify:alloy-modeller@DistOS:verification/^^/specs/*.als"

  - id: verify-theorem-proving
    subscribers: [theorem-prover, liveness-specialist, lead-verifier]
    purpose: "Coq/Lean proof progress and tactic strategy discussion"
    ucxl_feed: "ucxl://council-verify:theorem-prover@DistOS:verification/^^/proofs/*"

  - id: verify-counterexamples
    subscribers: [all]
    purpose: "Broadcast falsification events; all agents subscribe to detect cross-cutting impact"
    ucxl_feed: "ucxl://council-verify:lead-verifier@DistOS:verification/^^/counterexamples/*"

  - id: verify-cross-council-inbound
    subscribers: [lead-verifier, refinement-analyst, compositional-integrator]
    purpose: "Receive spec updates from all subsystem councils; triage for re-verification"
    ucxl_feed: "ucxl://council-*:*@DistOS:*/^^/specs/*"

  - id: verify-reports-outbound
    subscribers: [verification-report-writer, lead-verifier]
    purpose: "Coordinate and publish final verification reports to BUBBLE"
    ucxl_feed: "ucxl://council-verify:verification-report-writer@DistOS:verification/^^/reports/*"
```

---

## 8. Success Criteria

1. **Safety completeness:** Every subsystem spec has at least one mechanically checked safety property with a passing TLC run or Alloy check. Zero unverified safety claims in the final spec.
2. **Liveness coverage:** At least four of the six core subsystems have at least one mechanically checked liveness property under a documented fairness assumption.
3. **Refinement completeness:** At least three subsystems have a verified refinement mapping from abstract to concrete spec.
4. **No open counterexamples:** All TLC counterexamples discovered during the project are either resolved (spec corrected and re-verified) or explicitly deferred with a documented rationale and risk assessment.
5. **Compositional correctness:** The compositional verification report exists and demonstrates that system-level safety properties hold given the per-subsystem assume-guarantee decomposition.
6. **GPU model conformance:** The `council-mem` memory model spec is verified consistent with the Hopper/Blackwell hardware memory model specification.
7. **Invariant registry completeness:** The verified property registry contains an entry for every property claimed anywhere in the DistOS specification documents.
8. **Response SLA:** All counterexample reports are delivered to the originating council within 4 hours of falsification. All verification requests from `council-api` and `council-synth` are acknowledged within 2 hours.

---

## 9. Timeline

### Phase 1: Research (Days 1–3)

- All agents survey the reference systems and papers listed in Section 2
- TLA+ Specialists identify TLA+ idioms and patterns from Amazon, CockroachDB, and Raft specs that are directly applicable to DistOS
- Alloy Modellers establish the Alloy modelling vocabulary for capability lattices
- Theorem Prover Agents assess Coq/Lean library coverage for distributed systems reasoning
- GPU Memory Model Analysts study Hopper/Blackwell architecture documentation and Alglave et al. framework
- Lead Verifier drafts the verification scope matrix: which councils, which subsystems, which properties, which tools, in which order
- Deliverable: `ucxl://council-verify:lead-verifier@DistOS:verification/^^/research/verification-scope-matrix.md`

### Phase 2: Architecture (Days 3–6)

- Resolve Decision Points DP-V01 through DP-V05 with full DR records
- Establish interface contract templates and distribute to all subsystem councils
- Begin writing TLC harnesses for scheduling and fault tolerance specs (these arrive first from their councils)
- Establish the assume-guarantee decomposition for compositional verification
- Compositional Integrators begin mapping inter-council interface contracts
- Deliverable: `ucxl://council-verify:lead-verifier@DistOS:verification/^^/decisions/dp-v01-through-v05.md`

### Phase 3: Formal Specification (Days 6–10)

- Primary verification window: TLC, Alloy Analyzer, and Coq/Lean jobs run continuously
- TLA+ Specialists process all six core subsystem specs as they arrive from councils
- Alloy Modellers verify `council-sec` capability lattice and `council-api` interface contracts
- Theorem Prover Agents focus on consensus termination (Coq) and scheduler fairness (Lean)
- All counterexamples reported back to originating councils within 4 hours
- Liveness Specialists audit all specs for missing fairness assumptions
- Refinement Analysts begin mapping abstract to concrete for sched and fault subsystems
- Deliverable: All six per-subsystem verification reports (drafts) at verification report UCXL addresses

### Phase 4: Integration (Days 10–12)

- Compositional verification: compose all verified subsystem specs and check system-level properties
- Final resolution of any outstanding counterexamples
- GPU memory model conformance verification
- Verification Report Writers produce final reports for all subsystems
- Lead Verifier compiles the verified property registry
- Deliver compositional correctness report to `council-synth`
- Deliverable: `ucxl://council-verify:compositional-integrator@DistOS:verification/^^/reports/compositional-correctness.md`

### Phase 5: Documentation (Days 12–14)

- Verification Report Writers produce human-readable summaries of all verification results for inclusion in the main DistOS specification
- Lead Verifier produces a final verification audit trail navigable via UCXL temporal navigation
- All verification artifacts committed to BUBBLE decision record system
- Final verified property registry published
- Support `council-docs` in producing the Formal Verification appendix of the DistOS specification
- Deliverable: `ucxl://council-verify:lead-verifier@DistOS:verification/^^/reports/final-audit-trail.md`