We verify the security properties assertions cannot express.

The problem

The assurance gap

The tools that vet secure chips assume the cloud and charge per seat — a bad fit for classified work — and worse, they can quietly guess and still show a green checkmark. Mununu runs fully offline and never guesses.

Technical detail

Commercial formal tools are licensed by the seat and lean, more each year, on the cloud — an awkward guest in classified and air-gapped programs, where every tool must live wholly inside the enclave and answer for itself down to the byte.

Worse than the licensing is the epistemics. In security verification the nightmare is the silent wrong “pass” — a tool that quietly approximates, then reports “secure,” is a liability wearing a green checkmark.

Mununu is built for the opposite stance: on-prem, written in Rust, on an open-source toolchain, deployable with no network at all. Its verdicts are three-valued — True, False, or ⊥ (undecided) — and when abstraction cannot carry a definite answer, it abstains. It never bluffs.

The differentiated wedge

“Can it recover — or does it latch into the trap?”

A security chip has to do two opposite things perfectly: always recover under normal use, and never recover once it’s been attacked. Mununu proves both — on the same real chip.

Technical detail

For a security state machine, recoverability cuts both ways. In ordinary operation, with reset available, idle must stay within reach — a wedged security controller is a denial of service. But the instant the escalation input fires, the design must not recover: latching into the error trap is the whole point of the guard.

Both directions are branching-time. SystemVerilog Assertions and LTL bounded model checkers cannot say “a path back always exists,” so they can confirm neither the recovery nor the trap. Mununu decided both, definitively, on a production OpenTitan security FSM — the same real RTL, two environments, two sound verdicts.

Evidence

Demonstrated on real root-of-trust silicon

The proof points below are on real, production root-of-trust silicon — Google’s OpenTitan and the industry Caliptra — not lab toys.

aes_cipher_control · aes_ctr_fsm · otbn_start_stop→ SAFE PROVED

keymgr · edn_main_sm · rom_ctrl→ SAFE PROVED

mailbox black-box contract→ DISCHARGED PROVED

Weakness classes

The hardware-weakness classes you already track

Mununu speaks the same hardware-weakness vocabulary your assurance team already uses — and ships worked bug-and-fix examples for the classes that matter.

Assurance programs speak MITRE’s hardware-CWE language. So does Mununu. We ship bug/fix demonstration pairs for real weakness classes — each pair a constructed design in which the weakness is planted, detected, fixed, and re-verified. Every one is tagged DEMO: they demonstrate the property class, they are not findings in fielded silicon.

Deployment posture

Sound, embeddable, supply-chain-transparent

Built for the enclave: open, self-hosted, and accountable to the byte — no license servers, no calls home.

• Sound by construction. 3-valued verdicts; the core soundness theorems are machine-checked in Lean 4 and Isabelle/HOL.
• Open toolchain. The front end is auditable open source — slang, sv2v, yosys, Z3 — with Mununu itself in Rust. Every layer of the trust chain can be inspected.
• Self-hostable, air-gap-ready. Runs entirely on-prem as a CLI or a served HTTP API inside your enclave. No per-seat lock, no phone-home.
• Reproducible. Byte-deterministic transcripts and CI exit codes: the same input yields the same evidence, byte for byte.

Beyond checking

And synthesize the control kernel

Beyond checking someone’s work, Mununu can build the security control logic itself — so it’s correct by construction — and hands back machine-readable evidence when something fails.

Technical detail

For security-critical sequencing — lockstep steps, key-handling phases, escalation ladders — Mununu can synthesize the controller correct-by-construction instead of grading a hand-written one after the fact. What comes back is a control kernel that cannot violate its specification, because it was never shaped able to.

And when a property does fail, Mununu hands back structured JSON counterexamples — machine-readable traces made for triage tooling, not waveforms for a human to squint at.