Verification and synthesis. One system.
We prove your RTL. We build its controller.
One tool that both proves a chip design is correct and builds the control logic it’s missing — delivered as an API you can drop into a product or an AI coding loop.
Technical detail
Mununu is a Rust engine that listens to reactive systems — hardware RTL, protocols, the quiet choreography of agentic-AI workflows — and asks the temporal questions that decide whether they hold. In the grammar of μ-calculus and LTL, over Compositional Labeled Transition Systems, it proves what is true and builds, correct by construction, the controllers that keep it true. It meets you as a CLI, an HTTP API, and a web UI.
AG EF idle
HOLDS
PROVED
AG EF idle (escalation input free)
VIOLATED
PROVED
The reason this system exists
Two gaps in correctness. Both are closed.
Two problems hold hardware teams back today: the tool that verifies chips is expensive and can’t be embedded in a product, and the hardest correctness questions can’t even be written down. Mununu closes both.
The oracle gap
The instrument that judges whether RTL is correct costs a hundred to five hundred thousand dollars a seat, every year — and it will not live inside your product, nor ride along in an agent’s loop. If your system needs a conscience of correctness at its core, that price and that posture quietly close the door.
The expressiveness gap
Whole families of correctness — the power to recover, to survive a reset, to never deadlock, to always answer — cannot even be spoken in SVA or LTL. And synthesis, which builds a controller rather than merely grading one, is offered by no commercial or SaaS vendor at all.
We close both. Sound, expressive, embeddable — we verify and we build.
The defining property
“Can it always recover?”
The most valuable safety question is easy to ask and, until now, has been impossible to answer: from any state a design lands in, can it always get back to a safe one? Mununu answers it — proven, on real chips.
Technical detail
This asks after the shape of a design’s state space, not the fortunes of any single run. A trace-based assertion watches one path at a time; “recovery remains possible from everywhere” quantifies over the branching futures of every reachable state. That makes it branching-time — a thing SystemVerilog Assertions and LTL bounded model checkers cannot even utter, no matter how long they run.
Mununu decides it soundly, and has shown it on real OpenTitan silicon RTL — the same recoverability question answered, definitively, in both directions on a production security state machine.
One system, both directions
Verify and synthesize. One API.
Most tools either check a design or build one — never both. Mununu does both behind a single API, so you can prove what you have and generate what you’re missing in one place.
Technical detail
Verification tools only check; synthesis tools only build. Mununu is the only maintained tool that holds all three together — μ-calculus model checking, reactive controller synthesis, and sound 3-valued (KMTS) abstraction — behind a single served, embeddable API.
We prove your design
Safety, recoverability (AG EF good), liveness and response, GR(1) specifications. Every answer comes back definite — or honestly undecided. Never a guess.
We build the controller
Correct-by-construction synthesis — Ramadge–Wonham supervisory control and GR(1) — with export to SystemVerilog and XState. The controller cannot break its specification, because it was never built able to.
Surfaces: CLI · HTTP API · web UI. One set of engines. One set of verdicts. Wherever your work lives.
Soundness by design
Three verdicts. No bluffing.
When a verification tool says “pass,” can you trust it? Mununu gives one of three honest answers — yes, no, or “I can’t tell yet” — and never fakes confidence it doesn’t have.
Technical detail
Every question returns True, False, or ⊥ — undecided. When abstraction can no longer carry a definite answer, Mununu falls silent rather than guess. Honest scale today is block and FSM level, an exact cone of roughly 40 bits; beyond it, ⊥ — never a false “pass.”
Beneath it runs a portfolio that takes the first definite answer and raises an alarm the moment two sound engines disagree:
ROBDD | Exact symbolic — exact liveness on small FSMs, in-process |
KMTS + CEGAR | Predicate-cube 3-valued may/must abstraction for wide datapaths, auto-refined |
BMC + k-induction | Native bounded model checking and induction |
Interpolation | Native McMillan interpolation |
Ranking certificates | Termination-style certificates for recoverability and liveness |
Evidence
Demonstrated on real silicon. Not simulated.
This isn’t a lab demo. The results below come from real, production silicon — Google’s OpenTitan and the OCP Caliptra root-of-trust — not toy examples.
OpenTitan (lowRISC/Google open-source silicon root of trust, commit-pinned) and Caliptra (OCP datacenter root of trust) are verified subjects, not customers. These are property-class demonstrations on real RTL — not vulnerability findings.
AG EF (cnt == 0 ∨ cnt == MAX)
HOLDS
PROVED
ranking certificates, incl. nested/lexicographic
aes_cipher_control · aes_ctr_fsm · otbn_start_stop
SAFE
PROVED
keymgr · edn_main_sm · rom_ctrl
SAFE
PROVED
AG AF (bit_cnt == 0)
VIOLATED
PROVED
concrete stall lasso
How to read our evidence
- PROVEDSound, unbounded result. 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.
The science
Machine-checked. Reproducible.
The claims here aren’t marketing. The core guarantees are checked by machine, and every result ships with the evidence to reproduce it byte for byte.
Technical detail
The core soundness theorems are mechanized in Lean 4 and Isabelle/HOL. Definite verdicts carry to the real system at every alternation depth (Bruns–Godefroid, 3-valued KMTS); synthesis rests on memoryless winning strategies (Zielonka), ranking certificates (Podelski–Rybalchenko), GR(1) (Piterman–Pnueli–Sá’ar), and supervisory control (Ramadge–Wonham). Every verified example ships with a manifest, its source, and a byte-deterministic transcript, and every verdict maps to a CI exit code.
Where it lands
Choose your domain
Where does this land first? Start with the world closest to yours.
AI-generated RTL
The embeddable verify-and-build oracle for the generate-verify-fix loop — catching the control bugs LLMs quietly ship.
Explore the AI-RTL angle →
Defense & security
Air-gap-deployable proof of the security properties assertions can’t voice, shown on real root-of-trust RTL.
Explore the defense angle →
Aerospace & safety-critical
Exhaustive, machine-checked-sound proof that a design can never wedge — the kind of evidence a DO-254 process is built to reward.
Explore the aerospace angle →
Put a property to it.
Tell us what you’re verifying — a block, an FSM, a protocol, an agent loop — and we’ll run it with you, side by side. ALPHA