README.md

Strata — Proposal

Strata (working name) is a typed, comptime-elaborated hardware language and integrated verification platform, designed from the ground up as a substrate for agent-amplified hardware and systems-assurance engineering. It aims to preserve one chain from typed design intent through generated verification, transformation permissions, physical implementation evidence, fault/lifecycle contracts, and release assurance. This directory is the proposal: a build charter written cleanly enough to extract a whitepaper or grant proposal from later.

Every document is two-track:

Committed sections describe what we intend to build, mapped to a phase in the roadmap.
North star sections describe the full design the committed work must not preclude, including known open problems.

Anything contestable is logged in the decisions register and will be adversarially probed (see status legend below).

Scope after the systems-safety probe wave

The 2026-07-21 probe wave adds ten axes: fault/health, DMA memory safety, compositional progress, architectural memory consistency, observer-indexed information flow, physical-constraint custody, power/reconfiguration lifecycle, numeric error budgets, DFT/debug authority, and generated assurance cases. The result is not ten more core typing judgments. Strata uses a three-layer architecture:

a small semantic thin waist—identity/lineage, invalidation, memory events, observer projections, numeric denotation, and extensible authority;
opt-in contract families—fault recovery, leases, progress, memory models, power/reconfiguration, relational security, and assumption ownership; and
verification/evidence packages—fault campaigns, litmus/model checking, two-run checks, netlist-bound certificates, DFT translation validation, numeric certificates, and assurance graphs.

Ordinary FIFO or datapath code encounters none of those families unless it declares the corresponding contract. The executable probes establish the architecture and failure boundaries, not industrial-scale proof of RVWMO, analog leakage, electrical power behavior, unbounded liveness, or signoff-tool semantics. See the roadmap, decisions D-081–D-090, and the probe matrix.

Reading order

Doc	Contents
00-vision.md	Thesis, scope, thin-waist architecture, claims, and non-claims
01-design-principles.md	The rules every other doc must obey
02-type-system-core.md	Stratified judgments, phases, representation types, nominal identity, typestate
03-time-and-resources.md	Events, temporal capabilities, guarded feedback, the three notions of time
04-protocols-and-streams.md	Protocol types, stream combinators as protocol transformers, duality and refinement
05-speculation-authority-effects.md	Epochs, authority capabilities, effect rows, reset semantics
06-refinements-and-evidence.md	Tiered refinements, contracts, proof obligations, evidence lattice, and assurance custody
07-compiler-architecture.md	IR stack, semantic thin waist, CIRCT lowering, ledger custody, passes, and summaries
08-verification-platform.md	Contracts → tests, monitors, campaigns, relational/model-backed checks, and evidence
09-agent-system.md	Agent roles, trust model, diagnostics contract, experiment database
10-fpga-loop.md	Synthesis feedback, netlist certificate custody, HIL campaigns, and physical evidence
11-roadmap.md	Phases, what lands where, what is deferred and why
12-related-work.md	Academic and commercial prior art, nearest clusters, and defensible positioning
13-package-system.md	forge: manifest, mechanical semver, registry, modules, reproducible builds
14-toolchain.md	strata fmt, strata lint, strata-ls — one tree, one ledger, one diagnostic vocabulary
15-syntax-requirements.md	Syntax input: R1–R50 probe-evidenced requirements; R37–R50 await a surface-design wave
16-syntax.md	The committed core surface: charter, lexical rules, constructs, R1–R36 traceability, extension boundary
17-memory-model.md	`mem` storage class, read/write timing, port count, indexing safety, and pipeline ownership
18-grade-system.md	v0 usage grades: grade-0 erasure only, `ghost` wiring, and why grade-1/phases/typestate stay deferred
19-linearity.md	v0 grade-1 linearity: `linear let`, context-splitting exactly-once checking, and the OP-7 feedback disposition
20-guarded-feedback.md	v0 `delay`/`Later<Clock, T>`: the guarded-feedback typing judgment and the FIX-ω resolution (branch b)
decisions.md	Every contestable call: rationale, alternatives, confidence, probe status
open-problems.md	Known-unsolved interactions the design must eventually answer

Status legend

Used in decisions.md and inline in docs:

DRAFT — written, not yet probed
PROBING — under adversarial review
CONTESTED — probe found a real problem; decision being revisited
SETTLED — survived probing
DEFERRED — explicitly out of committed scope; north-star only

Context

This proposal consolidates and supersedes two working documents in the repo root: rough-1.md (the original platform proposal) and refine-1.md (a type-system deepening of it). Where they conflict, this directory is authoritative.