proposal/09-agent-system.md

Agent System

The autonomous engineering layer above the deterministic substrate. Principles in force: P-8 (models outside the trusted base), P-9 (diagnostics are the product), P-11 (agents build Strata with Strata).

Why the substrate shape is right — 2026 evidence

The documented failure modes of LLM RTL generation map one-to-one onto what Strata's substrate eliminates or catches (D-028 research):

  • The bulk of benchmark failures are late syntax errors, non-synthesizable constructs, and undefined module references — all structurally impossible in a typed language with comptime elaboration (there is no unsynthesizable subset to wander into; references are resolved at typecheck).
  • The residual, deeper failure mode is semantic hallucination — syntactically valid, synthesizable, functionally wrong RTL — which is precisely what contract-generated verification, differential lockstep, and mutation-scored properties (08) exist to catch. The 2025–26 agentic literature (validation-first orchestration) is converging on this conclusion; Strata's bet is that the validation should be generated from the same types the agent writes against, not bolted on.

Committed design

1. Trust model

Trusted: parser, typechecker, comptime evaluator, IR verifier, lowering passes, contract compiler, reference-model interface. Untrusted: every model output — code, properties, rewrites, strategies, analyses. Admission paths: typechecking; translation validation / equivalence checking for rewrites (07 §4); vacuity + mutation scoring for properties (08 §6); simulation/formal/FPGA evidence for behavioral claims. An agent claim without evidence tags is not reportable (P-7).

2. Agents operate on semantic objects

Agents read and write: typed AST, architectural IR, contract IR, obligations, schedule witnesses, experiment definitions — not raw structural netlists. A proposed change is a structured claim:

1architectural changes: none
2schedule changes: +1 stage between priority levels 2–3
3contract impact: latency +1; throughput unchanged;
4 CycleExact invalidated; TransactionEquivalent preserved
5required validation: typecheck, schedule check, protocol refinement, local LEC

The compiler rejects inconsistent claims before expensive validation runs. Diagnostics close the loop: every rejection is a structured object (violated judgment, facts, provenance, candidate repairs — P-9), turning repair into targeted search over the repair candidates rather than regeneration.

3. Roles

As in rough-1.md §26, kept: research, specification, architecture, implementation, verification, formal, synthesis, debugging, and review agents — with the review agent holding rejection authority and the whole set sharing one workspace protocol: claims in, evidence-tagged results out, everything logged to the experiment database. Role boundaries follow the summary system (07 §6): an agent's blast radius is the components whose summaries its change invalidates, which is what makes parallel agent work safe.

4. Experiment database

Every attempt — successful or failed — is a structured record: design hash, diff, config, rationale, compiler results, properties checked, formal results, coverage delta, corpus, synthesis/FPGA measurements, fault model and injection sites, observer/model choice, assumption owners, artifact/tool/target pins, expiry events, failure traces, review verdict, retention decision, and uncovered residue. Serves three functions: agents don't repeat rejected work; discovered invariants and counterexamples are reusable assets; the FPGA loop's measurements land as Measured evidence attached to designs, not as prose in a report.

5. Verification improvement loop

The verification agent inspects semantic coverage → explains generator limitations (in terms of the typed strategies, which it can read) → proposes new rules/strategies → validates them (do they reach the gap?) → measures incremental value → retains only what pays. Property proposals go through the §1 admission path. This loop is the platform's compounding asset: the corpus and property set improve monotonically under mutation scoring.

6. Assumption and assurance interactions

Agents may propose assumptions, fault models, declassification policies, physical exceptions, or evidence links, but cannot self-approve them. Every assumption names an owning component or environment boundary; cycles in which A and B each assume the other's progress are rejected. Every artifact records invalidators—source/summary change, tool or target change, clock/mode/netlist change, calibration expiry, mapping/power/reconfiguration epoch death. The review agent sees a release diff over guarantees, assumptions, evidence axes, expiry, and residue, not a synthetic pass/fail score.

An assurance agent may assemble and explain the custody graph and identify missing links. It cannot cite that graph as proof, upgrade Tested to Proved, or hide incompatible evidence axes. Independent deterministic checkers, where available, supply diversity evidence; model consensus does not.

North star

  • Agents proposing optimizer rewrites admitted purely by translation validation (level-D passes, 07 §4).
  • Formal agents doing invariant search over Tier-3 obligations (proposal side only; solvers dispose).
  • Cross-design transfer: the experiment database as a retrieval substrate so agents working on design N+1 start from design N's invariants, counterexamples, and failed approaches.

Open problems touching this doc

Consumes OP-5 directly — the measurable success criterion proposed there (agent repair success rate given only the structured diagnostic) should be a tracked platform metric from phase 2 on.