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.