Semiconductor
Firmware Verification for Silicon
Formal verification for processor microcode, platform firmware, root-of-trust, and TEE components — the kind of low-level code where a single property violation can compromise an entire product line.
The challenge
Silicon firmware ships once and runs everywhere
Microcode, secure-boot ROM, TEE supervisors and similar firmware sit below the operating system and below the reach of most testing infrastructure. Once they ship in silicon, fixes are expensive — and a single property violation in a privileged component can undermine the security guarantees of every device built on the part.
Bounded model checking is the appropriate tool for this layer: it produces either a mathematical proof that a safety or security property holds, or a concrete counterexample showing exactly how it fails. ESBMC has been applied to firmware codebases at this scale in published industrial collaborations.
Target sectors
Compliance
Standards we address
Common Criteria (ISO/IEC 15408)
Formal verification supports the higher Evaluation Assurance Levels (EAL5+) typically required for secure-element, TEE, and root-of-trust firmware.
FIPS 140-3
Bounded model checking is a well-established technique for evidencing the absence of memory-safety and arithmetic errors in cryptographic-module firmware.
Arm PSA Certified / SESIP
Aligned with the security-by-design expectations placed on connected-device silicon and platform firmware.
ISO/SAE 21434
Cybersecurity engineering for road-vehicle electronics — relevant for automotive semiconductors and the firmware they ship with.
ISO 26262
Functional safety for automotive electronics — formal verification is highly recommended at the higher ASIL levels.
NIST SP 800-193
Platform Firmware Resiliency Guidelines — formal methods support the protection, detection, and recovery objectives.
Our role
How we help
Microcode and processor-IP firmware
Bounded model checking at scale on processor microcode and low-level firmware. Our published Intel collaboration showed how interval analysis brings a 190,000-LOC firmware codebase into reach in eight hours where it had previously timed out after three days.
Root-of-trust and TEE components
Verification of memory-isolation, world-switching, and authorisation properties on privileged firmware components. Our published Arm collaboration applied this to the Realm Management Monitor at the heart of the Armv9 Confidential Computing Architecture.
Pre-release / pre-tape-out verification
Formal verification of firmware before silicon ships, catching property violations on representative harnesses generated from machine-readable specifications.
Verification-tool integration into CI/CD
We help silicon teams embed ESBMC into existing CI pipelines alongside other model checkers — including reproducing prior CBMC findings and surfacing additional violations that survive existing toolchains.
Specification-driven harness generation
Where machine-readable specifications exist (for example, Arm's RMM specification), we generate verification harnesses directly from the spec to evaluate pre/post-conditions on the implementation.
Verification-time optimisation
Where redundant pointer-dereference patterns or large state spaces blow up verification cost, we apply ESBMC optimisations such as VO-GCSE and interval analysis — both shipped in production ESBMC builds.
Published collaborations
Where this has been done before
Intel · Firmware
Scalable firmware verification
VO-GCSE and interval analysis applied to Intel firmware code; 190,000-LOC firmware verified in eight hours versus a three-day timeout without interval analysis. Published in the interval-analysis paper (arXiv 2406.15281) and FSE Companion 2025.
Arm · Confidential Computing
Realm Management Monitor verification
ESBMC identified 23 additional property violations in Arm's RMM firmware on top of those already detected by CBMC, and contributed a confirmed memory-model fix upstream. Published at SAS 2024.
Verifying silicon firmware?
Let's discuss how ESBMC-based formal verification fits into your firmware assurance flow — from microcode to root-of-trust to TEE supervisors.