Even though model checking has dominated formal verification of hardware systems for decades, it still struggles to scale to modern hardware designs due to its inherent state-explosion issues. Alternatively, interactive theorem proving (ITP) has been used for a relatively short amount of time, where a user can manually state and prove theorems. ITP is known to be more expressive than model checking in the sense that any correctness criteria can be specified and proven using higher-order logic. It has another issue, though; a significant amount of human effort is required to prove large theorems. In this talk, I would like to introduce approaches to making hardware verification scalable with ITP, overcoming the human effort by applying well-established formal-methods theories. In particular, two techniques will be presented: modularity to break a proof into smaller pieces and serializability as domain knowledge to handle distributed execution. For the former, we introduce Kami, a framework embedded in the Coq proof assistant to realize modular verification. For the latter, we introduce Hemiola, another Coq-embedded framework to verify modern cachecoherence protocols much more efficiently.

Joonwon Choi is a Formal Verification Engineer at Apple, working on verifying hardware memory subsystems. He completed a PhD in computer science at MIT CSAIL in 2021, co-advised by Adam Chlipala and Arvind. He received his MS from MIT in 2016 and BS from Seoul National University in 2013. During his PhD, he worked on formal verification of hardware using the Coq interactive theorem prover. His research interests include various formal-methods techniques to scale up verification of computer systems. He is a recipient of Kwanjeong Educational Scholarship.