Files
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 probedPROBING— under adversarial reviewCONTESTED— probe found a real problem; decision being revisitedSETTLED— survived probingDEFERRED— 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.