Verify AI-generated RTL · LLM Verilog verification
AI writes the RTL. We verify it — and synthesize what it gets wrong.
AI can now write Verilog, but it quietly gets the tricky control logic wrong — the deadlocks and races that pass every test and then hang the chip. Mununu is the checker your AI loop calls to catch them, and it can build that control logic correctly in the first place.
Technical detail
You can’t sample your way to mutual exclusion, and you can’t unit-test a liveness property. Mununu is the embeddable oracle for the generate-verify-fix loop: it synthesizes the control kernel correct-by-construction, and verifies the whole system your model assembled — end to end.
mutex
HOLDS
DEMO
no_starvation(c0, c1)
HOLDS
DEMO
bad_mutex (negative control)
SAT
DEMO
The failure mode
Where GenAI RTL breaks: control logic
LLMs handle the easy, repetitive parts of a chip well. Where they slip is the coordination logic — and those bugs are exactly the kind no amount of testing can rule out.
Technical detail
LLMs are respectable at datapaths — pipelines, arithmetic, muxing. Where generated designs come apart is control: arbitration, handshakes, mutual exclusion, fairness, backpressure, interlocks. Control logic is order-sensitive and adversarial — the environment gets a move every cycle, and one missed corner is a hang or a race.
That kind of bug passes lint. It passes a handful of directed tests. And then it ships — because no finite sample of traces can witness “this deadlock is unreachable” or “every requester is eventually served.” External studies put roughly 60% of LLM-generated hardware designs as carrying weaknesses in MITRE’s hardware-CWE catalog; the control classes are exactly where sampling-based checks go blind.
The frame
The division of labor
Let the AI do what it’s good at, and let Mununu own the part it isn’t: the AI writes the bulk of the design, Mununu builds the control core and checks the whole thing.
Writes the datapath
What it’s good at: structure, arithmetic, plumbing, the bulk of the RTL — and the spec it means to meet.
Builds the control kernel
Correct-by-construction: a winning strategy that structurally cannot violate mutex or fairness. Synthesized — not generated, then checked.
Verifies the whole system
The integrated design — datapath plus kernel — is verified end to end, discharging the very assumptions the kernel was synthesized under.
The checker confirms; it does not rescue. Synthesize the control kernel instead of hallucinating it, and a whole class of LLM failure modes never enters the design at all.
The workflow
The generate-verify-fix loop
It slots into an automated loop: the AI proposes a design, Mununu synthesizes the control core and verifies the result, and on failure it hands back a machine-readable fix the model can act on.
Grounded in three runnable demonstrations: agentic_rtl_loop (GR(1) synthesis plus whole-system verification, oracle-proven, with a negative control), handshake_flow (backpressure), and compute_engine_faulty — the lockup a regression suite passes and Mununu doesn’t.
DEMO These loop demonstrations are constructed examples: the LLM leg is mocked — you bring the model — and some liveness results in the loop are BOUNDED rather than unbounded proofs.
The structural point
Embeddable — per run, not per seat
Here’s the commercial edge: the industrial verification tools can’t be embedded in a product because of how they’re licensed. Mununu is priced per run and built to live inside your pipeline.
Technical detail
Here is the constraint no roadmap fixes: a per-seat commercial formal license cannot live inside your SaaS or agent product. Every customer you have would need to bring their own license before your verify step could even run. The business model rules it out — not the engine.
Mununu is priced per run and made to embed: a Rust binary, a CLI, and a served HTTP API you call as one step in your loop, self-hosted or hosted. It takes the slot the incumbents structurally can’t — a complement to them, not a replacement. Industrial engines own scale; Mununu owns the branching-time, synthesis, and embeddable region of the map.
Evidence · real LLM artifacts
Tested against real LLM-generated assertions
We didn’t just test this on our own examples — we ran it against a public benchmark of real LLM-written assertions on real chips.
designs elaborated
82 / 83
REAL ARTIFACTS
How to read our evidence
- PROVEDSound, unbounded result on the stated input. Definite verdicts transfer to the real system.
- BOUNDEDBounded model checking — valid to the stated depth only.
- DEMOConstructed example. Illustrates the capability; not a real-chip finding.
Straight answers
FAQ
Can I embed it in my product?
Yes. Mununu is priced per run, not per seat, and is self-hostable: a Rust binary with a CLI and a served HTTP API you can call from your SaaS or agent loop. Your customers don’t need their own licenses for your verify step to run.
Does it replace JasperGold or VC Formal?
No — it’s a complement, and it can wrap industrial-scale engines rather than beat them. Those tools own scale; Mununu occupies a different region of the map: branching-time properties like AG EF good, reactive controller synthesis, and embeddability behind a per-run API.
How does it handle LLM hallucinations in the control logic?
By keeping them out of the control path. Mununu synthesizes the control kernel correct-by-construction — a winning strategy that structurally cannot violate its specification — rather than checking hallucinated control logic after the fact. The checker confirms; it doesn’t rescue.
What can’t it do yet?
Full-SoC sign-off. Honest scale is block and FSM level, with an exact cone of roughly 40 bits. Above that, it returns ⊥ (undecided) rather than guessing — and it’s Alpha software. We’d rather abstain than bluff.
Is the LLM part included?
No — you bring the model. Mununu is the synthesis-and-verification oracle your model calls: it takes RTL and a spec, and returns verdicts, synthesized control kernels, and structured JSON counterexamples your model can consume.
Is it fast at synthesis?
Dedicated synthesizers synthesize faster. Mununu’s claim is the integration: synthesis and whole-system verification behind one embeddable API, with the kernel’s assumptions discharged against the actual assembled design.
Put the oracle inside your loop.
One integration call: we’ll wire the API into your generate-verify-fix pipeline, against your own designs. ALPHA