Known-unsolved design problems, mostly interactions between individually-solved disciplines. Each entry states the problem, why it's hard, what the committed design does meanwhile, and what a resolution must deliver. The probing phase should try to (a) sharpen these, (b) find ones we missed, (c) kill or solve any it can.

OP-1 · Speculation squash × temporal capabilities

Problem. An epoch squash must revoke resource grants that in-flight speculative operations already hold: scheduled intervals on shared units, linear slot tokens, credits. Linear/temporal typing has no standard story for revocation — consumption is forever, but a flushed load's queue slot comes back. Why hard. Naively, every capability becomes epoch-indexed and every use site needs a squash-path proof; that destroys the "modest surface burden" promise. Iris-style resource algebras can express reclaim, but the wave-2 probe showed committed scope doesn't need them: conservation counters + generative epochs suffice once fragments cannot escape component boundaries; the RA machinery becomes load-bearing only in the phase-3 fragment-escaping regime. Committed stance. Phase-scoped under-claiming: speculative operations may only hold capabilities whose reclamation is structural (slots owned by a queue that itself handles squash; the type system checks the queue's squash contract once, at the component boundary, not per use). See 05-speculation-authority-effects.md. Research status (2026-07-17). Confirmed genuine gap: neither Filament nor Anvil has any notion of a revoked/truncated interval (verified against both papers). Existing precedents to reconcile: PDL's typed speculation contracts (spawn/verify/kill with statuses — proves the typestate side is checkable) and HazardFlow's discard-and-restart hazard interfaces. No system combines them with interval/event types. Resolution must deliver. A revocation rule sound w.r.t. the temporal-capability semantics, with errors expressible in the P-9 vocabulary. Probe result (wave 2, probes/squash-semantics/, RESOLVED-COMMITTED-SCOPE). Revocation semantics designed and executable: authority revokes synchronously (tag compare), capacity drains within a declared bound D keyed on death events; squash contract = five checkable invariants (conservation / occupancy-sum / no-stale-authority / bounded drain / generativity) verified once at the component boundary, Tier-1 lookup at use sites. Crux settled: claims are commitments — squash is not a guard; the evaporation alternative is machine-refuted (physical double-drive in 300/300 random traces) and would need temporal-guard discharge the OP-4 line forbids. Intervals never revoke; only consumable tokens do. Firewall relaxed: speculative raw interval claims on shared units are legal without contracts; the prohibition narrows to consumable tokens crossing component boundaries. Residue (not blocking committed scope): epoch trees, squash × CDC crossing, unbounded-latency drains, revocation-horizon claims. "Resolution must deliver" is met for flat epochs: the rule is sound w.r.t. temporal-capability semantics and ships with its P-9 vocabulary. Wave-3 update (probes/epoch-trees/): the epoch-tree residue is RESOLVED and the two ambient axes unify. Epochs form a tree rooted at the reset epoch; squash = one death event over a victim set; the five-invariant contract holds per-epoch and in aggregate with a single non-stacking drain bound; the chain-with-masks realization real OoO cores use provably implements the tree semantics (coordinate-liveness ≡ tree-liveness, property-checked). Reset is the root's subtree squash — same flush operation, no special case — and treating reset/speculation as independent ambient parameters is machine-refuted (150/150 witnesses: pre-reset speculative values retire under a dead generation). ResetWitness reset contracts are squash-contract instances: one mechanism. Remaining residue: multipath-fetch commit ordering (contract itself is fetch-shape-agnostic), squash × CDC (probe in flight), heterogeneous per-subtree drain bounds (shape obvious), finite mask width (an ordinary capacity obligation).

OP-2 · Reset epochs × everything

Problem. If reset creates a new system epoch invalidating old-epoch capabilities (05), then nearly every stateful type is epoch-indexed, and epoch parameters threaten to infect every signature. Why hard. The value is real (stale-token bugs across reset are nasty); the cost is pervasive indexing — precisely the failure mode that killed heavyweight region systems. Committed stance. Epochs are implicit ambient parameters within a reset domain; only values that cross domains or outlive a reset (retention registers, persistent handles) surface epoch indices. Whether this inference actually stays implicit under composition is the open question. Resolution must deliver. An elaboration rule showing epoch indices stay out of ≥95% of user-written signatures on realistic designs. Probe result (wave 2, probes/epoch-containment/, NARROWED — bare rule refuted, mechanisms pass). On a 52-signature boundary-heavy SoC corpus: the bare ambient rule yields 63.5% clean — FAIL, with transport infection the killer (the fabric domain went 0/6; an arbiter over heterogeneous epochs isn't even typeable without existentials). With five absorption mechanisms (now committed design in 05 §4: Stamped<T,D> existentials + bind epoch, opaque minting-component-validated IDs, no_reset unit epochs, CDC-below-epochs, linear ResetWitness): 96.2% — PASS, residue = the two signatures where a free epoch variable is load-bearing. Candidate general rule: single-occurrence absorption — a free epoch variable is forced iff a signature relates ≥2 epoch-bearing values. The probe also fixed the criterion's definition (surfacing = free epoch variable; opaque carriers don't count) — without it the criterion was unmeasurable. Remaining items all closed in wave 3: the pinning analysis is a real inference pass — local, principal, decidable (probes/pinning-inference/: monotone join on a finite lattice, per-SCC summary fixpoint, 52/52 corpus agreement, 96.2% reproduced; epoch elision is inferred, not written — 05 §4); the two ambient axes unify as one tree with reset at the root (probes/epoch-trees/ — independent axes machine-refuted); and ResetWitness is a squash-contract instance under ONE epoch-death contract (probes/squash-cdc/). OP-2 is RESOLVED for committed scope.

OP-3 · Subtyping decidability × summary-based composition

Problem. Incremental compilation composes components via summaries without reopening bodies (07); protocol refinement subtyping in full generality is undecidable, and "incomplete algorithm + solver" gives unpredictable results — poison for summary caching and for agents relying on definitive answers. Committed stance. Protocol catalog with decidable parametric compatibility (D-015); Tier-2 solver checks always produce one of three stable outcomes (proved / refuted / obligation), and obligation is a first-class summary entry, not a failure. Stakes raised by the package system. Contract-typed dependency slots (13 §2) make resolution itself summary subtyping at ecosystem scale: if Tier-2 outcomes drift across solver versions, dependency resolution becomes flaky — a strictly worse failure than a flaky build. Probe result (2026-07-17, probes/protocol-catalog/, SUPPORTS-SETTLED). The coverage probe ran: AXI4-Lite, credit NoC, WRAP/INCR bursts, and OOO same-ID matching all land in the catalog given four additions now specified in 04 §1 (bundle and layer operators, burst_dyn, and the comptime-monomorphization rule for multiplying parameters). Nothing needed phase-3 user protocols. Confirmations: ordering-as-separate-judgment is forced (per-key FIFO order is refinement-inexpressible), and keyed-schema trace refinement is exactly the undecidability zone the committed design already fences. Remaining coverage risk: CHI-lite — untried, and the likeliest first genuine phase-3 case; it is the designated re-probe. Resolution must deliver. Evidence that the catalog covers real designs (probe: take AXI4, CHI-lite, a credit NoC protocol, and try to express them), a user-defined-protocol story whose subtyping is decidable or honestly obligation-generating, and solver-version-stable outcomes for the resolution-facing subset.

OP-4 · Grades and capabilities under path conditions

Problem. Conditional resource use (if is_add { use adder } / if is_addr_calc { use adder }) requires path-sensitive disjointness to justify sharing. Making the type checker discharge these turns it into a scheduler — the exact trap P-5 warns about for comptime. Committed stance. The checker only generates disjointness obligations; a distinct, bounded solver tier discharges them or the user arbitrates/replicates. The line between "checker generates obligation" and "checker schedules" needs a crisp formal statement. Probe result (2026-07-17, probes/interval-caps/). The line held under implementation, with a candidate formal statement: the check is a pure function over the design (no mutation, no reordering); repairs are suggestion values the checker never selects among; and the checker and discharge tiers exchange exactly one artifact type (the cardinality-form disjointness obligation) in exactly one direction — no interval data enters discharge, no propositional reasoning enters the checker. Remaining for full resolution: the checker↔optimizer exchange (sharing decisions the optimizer makes under discharged obligations) wasn't in probe scope. Resolution must deliver. A characterization of which sharing decisions belong to typechecking, which to the optimizer, and how the two exchange facts without circularity — the probe's purity/one-artifact/one-direction statement is the candidate to formalize.

OP-5 · Multi-judgment diagnostics

Problem. With five-plus interacting judgments, a single bad connection can fail in several dimensions at once, some via solver timeouts. Explaining which judgment failed, why, and what repairs exist is an unsolved UX problem at this scale — and P-9 makes it load-bearing for the entire agent thesis. Committed stance. P-9 gating: a judgment doesn't ship without its diagnostic vocabulary. Errors are structured objects (violated judgment, facts, provenance, repairs) before they are English. Delivery vehicle. strata-ls is the designated harness (14 §21): multi-judgment failures render as one primary diagnostic naming its judgment with related facts attached; every repair acceptance/rejection is an experiment-DB event keyed by (judgment, repair, audience) — so "measure repair success given only the diagnostic" becomes standing telemetry, not a study. Resolution must deliver. A worked diagnostic taxonomy over the phase-2 judgment set, user-tested (or agent-tested: measure repair success rate given only the diagnostic); per-judgment repair-success dashboards from strata-ls telemetry by end of phase 2, cited by the P-9 ship-gate for new judgments.

OP-6 · Semantic ledger authoring burden

Problem. "Passes never silently drop facts" (P-3) implies every pass classifies its effect on every fact category. MLIR experience says analyses get invalidated wholesale in practice; the conservative default ("invalidates everything not mentioned", D-019) is sound but erodes toward useless if nobody annotates. Committed stance. Conservative default + ledger-coverage metrics reported per pass, so erosion is visible; the small set of core passes we own get full annotations. Probe result (2026-07-17, probes/ledger-passes/, SUPPORTS-SETTLED with riders). Erosion quantified on a 100-node/370-fact design over 12-pass pipelines: survival ≈ Π(1−touchᵢ) over the union of lazy touch-sets (order-independent — invalidation is absorbing); at 25% lazy passes, provenance and protocol facts drop below 50%; full-lazy ends near zero. The committed mitigation holds: with core passes annotated, all categories survive at 100% end-to-end and provenance/verification-generation inputs fully work. Two riders now part of the design: (a) touch-set tracking must be structural — one opaque pass with an unbounded touch set zeroes the ledger in a single step; (b) proof facts need finer-than-category invalidation — tag each proof with the equivalence it assumes and invalidate per-equivalence-break, else honest retiming annotations still gut the proof category. Metrics should report absolute counts alongside percentages (small categories are noisy). Resolution must deliver. Evidence after phase 2 that ledger precision on the hot path (elaborate → schedule → emit) stays high enough that downstream consumers (verification generation, provenance queries) actually work — now with the two riders as implementation requirements.

OP-7 · One semantic model

Problem. refine-1.md's closing requirement — the eight disciplines must form one semantic model with one metatheory — is asserted, not designed. Pairwise soundness is not composition soundness. Committed stance. The committed phases only combine disciplines whose pairwise interaction is understood (see 11-roadmap.md phase gates). A core-calculus document (to be promoted to 15-core-calculus.md) is the designated home for the real answer; mechanization of at least the phase-2 fragment is a north-star milestone. Probe result (wave 2, probes/core-calculus/, FRAGMENT-SOUND as amended — GAPS-FOUND(2), both repaired). λ-strata⁰ formalizes the phase-1/2 fragment (23 typing + 4 WF rules, Rust checker with 86 tests, one function per rule). The thesis was demonstrated concretely: two real cross-discipline unsoundnesses existed — (1) grades × later: the naive feedback rule accepts a 1-graded value spent once per cycle; neither QTT nor guarded recursion alone can express the bug; fixed by FIX-ω (ω-promotion of feedback-body usage), whose corollary — ω-graded periodic capabilities remain usable in feedback — is exactly how linearity reconciles with initiation intervals; (2) erasure × elaboration: "erasure commutes with elaboration" is false once reflect exists; fixed by an elaboration-closedness premise on T-REFLECT (D-037's clause 2 doing double duty). All other attempted breaks are blocked by named, tested rules — including the branch-join rule deriving D-039's errdefer discipline, and overlapping guards correctly deferring to discharge (the OP-4 line reproduced inside the calculus). Wave-1/2 amendments (positivity, cardinality obligations, modulo-II) turned out to be exactly the lemma premises, unreshaped — the probes were doing metatheory without knowing it. Lemma statuses: four PROVEN-SKETCH (one with proviso, one conditional), productivity PLAUSIBLE-STATED. Honest residue: term-level refinements × grades is the designated re-probe; symbolic event bases out of fragment; the D-037 production confluence argument is still owed. Resolution must deliver. A core calculus for the committed feature set with type-soundness proven or mechanized, before phase 3 features stack on it — now concretely staged: the checker stays green as a phase-2 gate with per-feature break-hunt reruns; full mechanization (est. 2–4 person-months, Lean/Coq) is the phase-3 entry gate, not the phase-2 exit.

OP-8 · Dynamic-latency temporal capabilities

Problem. Fixed-latency intervals (Filament-style) are well understood; dynamic latency (cache misses, arbitration) needs symbolic event constraints (response ≥ request + 1) and their interaction with capability non-overlap checking is much less mapped. Anvil points a direction; maturity unknown pending research brief. Research status (2026-07-17). Anvil (ASPLOS 2026) shows dynamic event patterns are typeable via event-graph interval containment, but it is a first-release prototype that currently loses ~2× in power to Filament on a static pipelined ALU — dynamic-event typing is not yet compatible with keeping static-pipeline quality. Promotion criterion recorded in 03. Committed stance. Phase 2 ships fixed-latency capabilities; dynamic latency enters via protocols (outstanding-count refinements) rather than via the interval checker. Resolution must deliver. A decidable (or obligation-generating) non-overlap story for symbolic intervals.

OP-9 · Fault-model completeness and health composition

Problem. The fault probe separates occurrence, detection, correction, containment, recovery, and invalidation for a bounded MSHR model. Real fault campaigns must cover spatially correlated faults, common-cause failures, latent multi-bit corruption, clock loss, memory-array behavior, and faults in the protection logic itself. Committed stance. Health contracts enumerate fault classes, injection sites, detection/containment bounds, trustworthy residue, and coverage. Unlisted classes remain residue; a campaign never implies environmental qualification. Resolution must deliver. An integrated MSHR/ECC/replay target, mutation adequacy against protection-logic faults, and a mapping from declared fault coverage to independent safety-tool/physical evidence without double-counting.

OP-10 · Compositional progress beyond finite summaries

Problem. Finite wait-for SCC/rank/escape checks catch practical deadlocks but do not prove arbitrary protocol liveness, and weak fairness does not provide finite response bounds. Abstraction can also erase the dependency that closes a cycle. Committed stance. Stable proved/refuted/obligation; explicit assumption ownership; only independently provisioned escape resources, well-founded ranks, or checked acyclicity discharge the decidable core. Resolution must deliver. CHI/NoC/reset-drain corpus results with seeded deadlocks, abstraction-sound summary rules, and a clear handoff from conditional progress summaries to model checking or theorem proving.

OP-11 · Full memory-model and translation composition

Problem. The probe proves protocol legality and architectural memory legality are distinct, but full RVWMO/Arm-style models include mixed-size/per-byte behavior, dependencies, translation, speculation, coherence, DMA, and interrupts. Partial summaries can become unsound if completeness is overstated. Committed stance. First-class events/relations plus explicit completeness; bounded litmus/model checks are evidence, not universal proofs. Resolution must deliver. Validation against a standard executable model, mixed-size and address-translation cases, component-summary composition theorems or conservative obligations, and an RTL-linking story.

OP-12 · Observer adequacy and physical leakage

Problem. Noninterference is only as meaningful as the observer projection. Cycle, contention, cache, debug, and power observers are incomparable in places; physical leakage is probabilistic and target-dependent, not fully represented by digital traces. Committed stance. Named observer projections in semantics; two-run relational verification; explicit declassification authority; physical power observations remain measured/model evidence. Resolution must deliver. Observer adequacy criteria, composition rules across hardware/software speculation contracts, and a calibrated path from digital leakage models to measurement without promoting correlation to proof.

OP-13 · Vendor-bound physical, power, and DFT semantics

Problem. Exact selector precedence, retiming/cloning lineage, setup/hold pairing, scan insertion, UPF power semantics, RDC, and reconfiguration behavior vary by backend and version. Source intent alone cannot prove what a vendor artifact means. Committed stance. Candidate certificates plus exact nonempty post-transform binding and validation; dependency manifests invalidate on relevant design/tool/target/mode changes; digital guarantees remain conditional on characterized electrical assumptions. Resolution must deliver. At least two vendor adapters and one open-flow adapter, seeded selector/precedence/lineage failures, DFT and power-aware translation validation, and measured false-positive/false-negative behavior.

OP-14 · Assurance-case scale, standards, and epistemic independence

Problem. A custody graph can become a large, circular dashboard that appears authoritative while merely restating correlated artifacts. Tool diversity, assumption ownership, evidence incompatibility, expiry, and release diffs must remain visible at SoC scale. Committed stance. Assurance cases are deterministic derived graphs and never evidence. Self-citation and circular ownership are rejected; uncovered residue is mandatory output. Resolution must deliver. Export/interchange with an established assurance metamodel (for example OMG SACM), incremental scaling measurements, diversity/correlation rules, and a seeded study showing that stale, circular, incompatible, and missing evidence cannot yield a green release.