# proposal/09-agent-system.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/fc26a6ca718d47c3c3d920dca6b2f8e4e71eb4e4/proposal/09-agent-system.md)

Repository: [versecafe/strata](https://git.cafe/versecafe/strata)

Visibility: public

Requested revision: fc26a6ca718d47c3c3d920dca6b2f8e4e71eb4e4

Requested commit: fc26a6ca718d47c3c3d920dca6b2f8e4e71eb4e4

Commit: fc26a6ca718d47c3c3d920dca6b2f8e4e71eb4e4

Blob: 7796f50373af9a9b821439db5132ecf71a853811

Size: 5991 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/fc26a6ca718d47c3c3d920dca6b2f8e4e71eb4e4/proposal/09-agent-system.md?format=markdown)

````
# 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](08-verification-platform.md)) 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](07-compiler-architecture.md)); vacuity + mutation scoring for properties ([08 §6](08-verification-platform.md)); 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:

```
architectural changes: none
schedule changes: +1 stage between priority levels 2–3
contract impact: latency +1; throughput unchanged;
                 CycleExact invalidated; TransactionEquivalent preserved
required 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](07-compiler-architecture.md)): 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](10-fpga-loop.md)'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](07-compiler-architecture.md)).
- 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](open-problems.md) 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.

````