Initial commit: Fresh implementation of CHORUS architecture (ResetData Mandate)

2026-03-03 13:38:56 +11:00
commit 68a489b64d
41 changed files with 17535 additions and 0 deletions
--- a/docs/distos/councils/07-formal-verification.md
+++ b/docs/distos/councils/07-formal-verification.md
@@ -0,0 +1,464 @@
+# 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`