A Case Study in Firmware Verification:
Applying Formal Methods to Intel® TDX Module
The paper is accepted at TACAS 2026.
A preprint is available upon request.
Supplementary material is provided in the 
appendix.
This work is supported by a research gift from Intel.
Abstract
Firmware underpins system security but remains challenging to verify due to hardware dependency, specialized coding idioms, and limited open-source examples. Manual verification approaches, while common in industry, are labor-intensive and difficult to scale. This paper presents a detailed case study on applying automatic formal methods for software to a security-critical firmware component in Intel® Trust Domain Extensions (TDX), known as TDX Module. In this study, we employ six state-of-the-art C-program analyzers on the production TDX Module firmware, leveraging techniques ranging from bounded model checking and symbolic execution to abstract interpretation. Our empirical evaluation identifies obstacles unique to firmware, highlights harness-design decisions essential for verifying industry-scale code bases, and demonstrates opportunities in advanced slicing for more scalable verification. Although the case study focuses on TDX Module, the findings are broadly applicable to large-scale, low-level programs and have already influenced the software-verification community, such as standardizing nondeterministic object initialization. All verification tasks and proof harnesses are publicly released to foster reproducible research and future tool development.
Reproduction Information
The unmodified source code of TDX module (version 
1.5.05),
the developed proof harnesses, and the derived verification tasks are archived on
HarnessForge.
An artifact for reproducing the results presented in Sect. 5 of the paper is also available on
Verification Results
The table below reports, for each interface function, the number of verification tasks correctly solved under different havocking strategies (corresponding to Table 2 in the paper). In addition, we provide an interactive HTML table containing the verification results and logs for each task produced by each evaluated software analyzer.
| Interface function | Num. tasks | Mem. havoc | Obj. havoc | Tool-specific havoc |
|---|---|---|---|---|
| TDG.MR.REPORT | 10 | 0 | 0 | 5 |
| TDG.SERVTD.WR | 10 | 0 | 0 | 7 |
| TDG.SYS.RD | 10 | 0 | 0 | 8 |
| TDG.VM.WR | 17 | 0 | 0 | 14 |
| TDG.VP.ENTER | 18 | 0 | 0 | 12 |
| TDG.VP.VMCALL | 10 | 0 | 0 | 8 |
| TDH.EXPORT.RESTORE | 10 | 3 | 0 | 7 |
| TDH.IMPORT.ABORT | 9 | 2 | 0 | 7 |
| TDH.MNG.ADDCX | 33 | 5 | 2 | 11 |
| TDH.MNG.CREATE | 18 | 3 | 0 | 17 |
| TDH.MNG.INIT | 33 | 5 | 0 | 11 |
| TDH.MNG.KEY.CONFIG | 18 | 4 | 0 | 16 |
| TDH.MNG.KEY.FREEID | 17 | 2 | 0 | 16 |
| TDH.MNG.VPFLUSHDONE | 21 | 4 | 0 | 19 |
| TDH.MR.FINALIZE | 29 | 3 | 0 | 7 |
| TDH.PHYMEM.PAGE.RECLAIM | 25 | 0 | 0 | 5 |
| TDH.SYS.CONFIG | 29 | 0 | 0 | 8 |
| TDH.SYS.INIT | 17 | 0 | 0 | 13 |
| TDH.SYS.KEY.CONFIG | 13 | 10 | 0 | 13 |
| TDH.SYS.SHUTDOWN | 17 | 0 | 0 | 13 |
| TDH.SYS.UPDATE | 25 | 0 | 0 | 19 |
| TDH.VP.ENTER | 29 | 0 | 0 | 9 |
| Overall | 418 | 41 | 2 | 245 |
Identified Verifier Issues
| Verifier | Issue description | Issue links |
|---|---|---|
| CBMC | Incorrect handling of packed in struct members |
#8443 |
| CPAchecker | Anonymous struct/union in designated initializers not supported |
#1239 |
| Lack support for cast-to-union extension | #1289 | |
Lack support for compiler attributes such as packed and aligned |
#818 | |
| ESBMC | Error during encoding of verification conditions | #2850, #2851 |
| Error during program unrolling | #2852 | |
| Ultimate Automizer |
Anonymous struct/union not supported by C-to-Boogie translator | #272 |
| Lack padding model for unpacked data structures | #417 |