mununu.

DO-254 formal verification · safety-critical FPGA / ASIC

Prove it can never wedge.

For safety-critical hardware — flight controls, avionics — the worst failure is a silent lockup no test happened to hit. Mununu proves a design can always recover, by checking every possible state, not just the ones you sampled.

Technical detail

The safety-critical questions that matter most are branching-time — no permanent lockup, graceful recovery from any fault state. Simulation only samples them; assertions cannot even phrase them. Mununu proves them — exhaustively, with machine-checked soundness — on real RTL.

Request an evaluation on your FPGA/ASIC See it on real RTL
OpenTitan · counters / timers / watchdogs · real RTL
AG EF (cnt == 0) HOLDS PROVED 48-bit · ranking certificates
From every reachable state of the 48-bit counter, the way back to zero is still open — proved, not sampled.

The core idea

Safety-critical is a branching-time question

“Can it always get back to a safe state?” sounds simple, but no amount of testing can truly answer it. Mununu can, because it reasons about every reachable state at once.

Technical detail

“Can it always get back to safe?” is no statement about a single run. It says: from every state the design can reach — every fault-induced state among them — at least one path home to safety still exists. That quantifies over the branching futures of every reachable state.

SystemVerilog Assertions and LTL speak of individual traces, so the property is inexpressible in them — not hard to check, but impossible to state. Plain bounded model checking and k-induction inherit the same blindness: they walk runs, and no collection of runs can witness “a path back always exists.” Simulation, for its part, only samples; for a lockup hiding in one corner of billions of states, sampling is hope, not evidence.

Mununu evaluates branching-time properties (μ-calculus, CTL-class) directly and soundly. A HOLDS verdict covers the whole reachable state space; a VIOLATED verdict arrives with a concrete trace showing exactly how the design wedges.

Evidence · recoverability

From any fault-induced state, can it recover?

We proved this on real production counter and timer logic from Google’s OpenTitan — and where a design can hang, we produce the exact failing sequence.

Technical detail

The recoverability class is shown on real OpenTitan counter, timer, and watchdog RTL — commit-pinned production silicon source, not a toy. Verdicts are settled by ranking certificates — nested and lexicographic where hierarchical timers demand it — at 48-bit width.

OpenTitan · counter / timer / watchdog family
AG EF (cnt == 0 ∨ cnt == MAX) HOLDS PROVED 48-bit · nested/lexicographic ranking
uart_tx · AG AF (bit_cnt == 0) VIOLATED PROVED concrete stall lasso
Both directions earn their keep: the proof certifies recovery; the violation hands you the exact stall to fix.

How to read our evidence

  • PROVEDSound, unbounded result on the stated RTL. 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.

Fault tolerance

Single-event upsets & fault tolerance DEMO

In space and at altitude, radiation flips bits. Mununu can check whether a chip’s redundancy really masks those upsets — the property radiation-hardened designs are built around.

Technical detail

Radiation flips bits. The classic answer is redundancy — dual- or triple-modular voting, as in LEON3-FT-class processors — and the classic question is whether the voting logic truly masks every single-event upset the design claims to tolerate.

Mununu’s dmr_commit_4bit gate demonstrates this property class on a dual-modular-redundancy commit stage, drawing its fault model from the radiation-effects literature and the LEON3-FT lineage.

Honest scope: this is a constructed demonstration — a tiny design, checked at the labeled-transition-system level only, and not yet reproduced in Verilator. It shows the property class; it is not a claim about fielded fault-tolerant silicon.

Correct by construction

Interlocks that cannot be violated DEMO

The safest interlock is one that physically cannot be broken. Mununu builds the control logic so that the unsafe action is impossible by construction — not merely checked for afterward.

Technical detail

The strongest interlock is the one the controller cannot break. Mununu synthesizes controllers as winning strategies against every move the environment can make, so the safety condition is structural — not a check bolted on afterward.

clock_gating DEMO

“Never actuate while unsafe”

A synthesized gating controller that structurally cannot enable the clock while the unsafe condition holds — proven by k-induction, with a negative control confirming the checker catches the broken variant.

door-motor interlock DEMO

Elevator door-motor interlock

A synthesized door/motor controller in which motion-while-open is unreachable by construction — the textbook interlock, delivered as a strategy rather than a hope.

Process fit

Evidence DO-254 rewards

Safety certification (DO-254) rewards evidence that is exhaustive, traceable, and repeatable. Formal proof is exactly that shape — and Mununu is honest about where its scale ends today.

DO-254 design assurance at DAL A/B asks for evidence that is exhaustive, traceable, and independently repeatable. Formal proof is its native shape, and Mununu is built to produce exactly that:

  • Exhaustive, not sampled. A definite verdict covers the entire reachable state space of the verified block.
  • Traceable. Every result is a property → verdict → engine record, tied to pinned source.
  • Reproducible. Byte-deterministic transcripts; verdicts map to CI exit codes, so the evidence regenerates identically on demand.
  • Sound — and the soundness itself is checked. The core soundness theorems are mechanized in Lean 4 and Isabelle/HOL.
Scope, plainly: Mununu produces DO-254-relevant evidence; it is Alpha software and not a qualified tool. Honest scale today is block and FSM level, with an exact cone of roughly 40 bits — above that it returns ⊥ rather than guessing. We consider the abstention a feature: for this audience, a tool that never bluffs is worth more than one that always answers.

Pick the block that must never wedge.

Send us the FSM or counter at the heart of your safety case; we’ll formalize its recoverability with you and hand back reproducible evidence. ALPHA

Request an evaluation Read the docs