Service · Anchor offering
Firmware & Silicon Verification
Bounded model checking at scale on the layer of code that ships once and runs everywhere — microcode, root-of-trust, TEE supervisors, secure boot, and platform firmware.
Why this offering
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.
This is the area where formal verification has the highest return per engineer-hour, and the area where Cyber-Reasoning Consultancy (CRC) has the deepest published track record.
Track record
Two published industrial collaborations
- Intel. In our published collaboration, interval analysis brought a 190,000-LOC Core Power Management firmware from a 3-day timeout to an 8-hour verdict; VO-GCSE delivered a 1,500% speedup on a representative firmware code pattern (arXiv 2406.15281; FSE Companion 2025).
- Arm. In our SAS 2024 collaboration with engineers from Arm, ESBMC identified 23 additional property violations in the Realm Management Monitor — the privileged firmware at the root of trust of the Armv9 Confidential Computing Architecture — on top of those already detected by CBMC, and contributed a confirmed memory-model fix upstream.
What we verify
Target firmware classes
How we deliver
The techniques behind the case studies
Spec-driven harness generation
Where machine-readable specifications exist (e.g. Arm RMM), we generate verification harnesses directly from the spec to evaluate pre/post-conditions on the implementation. Demonstrated in our SAS 2024 Arm CCA case study.
Interval analysis at the GOTO level
Abstract interpretation that tightens the bounds on program variables and supplies stronger invariants to k-induction. Took an Intel 190,000-LOC firmware codebase from a 3-day timeout to an 8-hour verdict (arXiv 2406.15281).
Verification-Oriented GCSE
A verification-targeted Global Common Subexpression Elimination pass that runs at ESBMC's GOTO IR, eliminating redundant pointer-dereference and subexpression computations before symbolic execution. Shipped in ESBMC 7.5+ (FSE Companion 2025).
Cross-tool integration
GOTO Transcoder lets ESBMC consume GOTO files produced by Kani / CBMC, so we can plug into existing CI workflows alongside an incumbent verifier and surface complementary findings (as we did for the model-checking/verify-rust-std project).
Sector fit
Where this lands
Semiconductor
Microcode CI integration, secure-element / TEE firmware verification, NIST SP 800-193 platform-firmware-resiliency support. Substantiated by our published Intel and Arm collaborations.
Automotive
Target capability for ASIL-rated firmware verification, ISO/SAE 21434 cybersecurity engineering for automotive SoCs, and AUTOSAR component verification — paired with our Tool Qualification & Certification Support service.
Aerospace
Target capability for DO-178C DAL A/B-class firmware verification (FMS, FADEC, and other airborne firmware) — paired with our Tool Qualification & Certification Support service for the DO-330 qualification evidence.
Verifying silicon firmware?
Tell us about the firmware family and the safety or security standard you're working toward. We'll scope a discovery engagement that maps cleanly onto our published Intel and Arm playbooks.