Toroid — an agent that writes and proves correctness properties for chips

If Congruent points formal methods at AI-written code, Toroid runs the same bridge in the other direction: AI, pointed at formal methods' home turf. An agent reads a hardware spec and a Verilog module, asks Claude to propose formal properties, discharges them with a real model checker (Yosys + SymbiYosys), and iterates on the counterexamples. The LLM proposes; the solver disposes — hallucination cannot pass verification.

The problem

A verification engineer's inner loop: read the spec and the RTL, decide what must always be true, write it as assertions, run the model checker, stare at the counterexample waveform, decide whether the bug is in the design or the property, fix, re-run. It's slow, senior, scarce work — and almost untouched by modern AI tooling, because a language model's opinion about a chip is worth nothing. Its opinion as a hypothesis a solver then settles is worth a lot.

Approach — every claim tied to a solver verdict

1. Extract the truth first. The module's real interface — ports, widths, clock, reset — comes from Yosys itself, never from the model's guess.
2. Synthesize, then gate. Claude proposes safety properties grounded in that interface and the spec, constrained to the assertion subset the open Yosys frontend actually accepts. A compile gate rejects anything that doesn't elaborate and feeds the diagnostics back for repair — bounded attempts, not retries forever.
3. Discharge. BMC, k-induction, and IC3/PDR via SymbiYosys — Bitwuzla for the SMT engines, ABC for PDR — with a lightweight pip install-only Yosys backend as the fallback. Each property returns PROVEN, BOUNDED-PASS, or FALSIFIED with a trace.
4. Iterate. A falsified property is parsed into a per-cycle trace, narrated deterministically, classified — RTL bug, over-strong property, or missing assumption — patched, and re-discharged: a guarded loop with bounded rounds.

Why it's trustworthy — the solver has the last word

• PROVEN is only awarded by an unbounded engine (k-induction / PDR). BMC alone reports BOUNDED-PASS with its depth stated.
• A vacuity guard. A property that passes only because its witness is unreachable is reported VACUOUS, never green — and the refine loop rejects patches that would weaken a red property into a vacuous pass.
• The verdict policy is property-tested. Hypothesis fuzzes decide_verdict over every raw solver outcome: unbounded-engine-only PROVEN, error/counterexample precedence, VACUOUS exactly when a pass's cover is unreachable.
• The AI path replays in CI with no API key. The live Claude run is captured as a fixture and re-driven through the real compile gate and solver — 12 integration tests run green in CI, including the full SymbiYosys backend.

The demo — one injected bug, caught end-to-end

A FIFO with an injected off-by-one: its full flag fires one slot early. Toroid checks the invariant full ⟺ count == DEPTH, proves it on the correct FIFO and falsifies it on the buggy one — the solver returns a state where count == 4 yet full == 0, exactly the dropped boundary. In the recorded live run (claude-opus-4-8) against a counter design, Claude synthesized 9 properties — 5 safety asserts plus 4 reachability covers — that compiled on the first attempt, and the checker proved all 5 asserts. There's also toroid equiv, a miter with shared symbolic inputs and the hardware sibling of Congruent: it proves two designs equivalent or hands back the distinguishing input (a=4, b=2 against a max-that-returns-min impostor).

Status & what's next

All five milestones built and confirmed live, plus a hardening pass: recorded-fixture CI, the property-tested verdict core, and the SymbiYosys + Bitwuzla backend green in CI. Deliberately out of scope for v1: full concurrent SVA (commercial-frontend territory), multi-clock and full-chip designs, liveness, and auto-fixing the RTL — Toroid diagnoses the design under test; it never rewrites it. Stated bounds: the multi-round refine loop is exercised with fakes (one live classification is captured as a fixture), and live synthesis is non-deterministic run to run — the pinned artifact is the recorded fixture.