CHERI-CVA6 Verification
Complete specification compliance of CHERI-CVA6 against the Sail specification for COSMIC.
A research group at the University of Oxford exploring applied hardware formal verification. We are a time-limited "pop up" lab that will be running May – August 2026, though we also do research in this field year round. We welcome academic and industrial visitors interested in exchanging ideas about formal proof and hardware.
Our public work can be found here: GitHub
Research Areas
Formal verification of RISC-V MUL and DIV
Verification of the MUL and DIV instructions for CHERI-CVA6 and CHERIoT-Ibex
Model Checking and Lean Logic
Bridges between model checked SVA and the richer Lean proof language.
Symbolic Simulation with Boolean Abstraction
Formal verification of floating point and vector operations in CVA6 and ARA using Symbolic Simulation and Symbolic Indexing.
Symbolic Indexing for Symmetry
Exploitation of symbolic indexing, a spohisticated partitioned abstraction mechanism in symbolic simulation with Boolean abstraction, for mircoarcitectural tables.
People
Professor Thomas Melham
Managing Director
Tom is a Professor of Computer Science at the University of Oxford and a Fellow and Tutor in Computation at Balliol College Oxford. He is a seasoned veteran of formal verification, and is the main organiser of OX-FV. He works on COSMIC, Symbolic Simulation, indexed abstractions, EDA, and more.
Louis-Emile Ploix
Technical Director / Researcher
Louis-Emile is a graduating 4th year at Oxford, and is working on end-to-end formal verification of the CHERI-CVA6 processor as a part of the COSMIC project. This will later become some kind of observational correctness, as we did for Ibex and CHERIoT-Ibex in an extension to our prior work.
Ashraf Alam
Research Assistant
Ashraf is a graduating 4th year mathematician at Oxford. With a background in mathematical logic, he will be taking this "pop-up lab" as an opportunity to learn about formal verification. His work will be on the formal verification of the bit manipulation extension and floating point operations of the CHERI-CVA6 processor.
Tita Rosemeyer
Research Assistant
Tita is a PhD Candidate at the AIMS CDT at Oxford. Her work in this group focuses on the formal verification fo the multiplication module of the CHERI-CVA6 processor. Previously, during her MSc thesis, she worked on the formal verification of binary code on the CHERIoT-Ibex microprocessor under Tom Melham's Supervision at Oxford.
Nathan Medros
Researcher
Nathan is an MSc student in Computer Science at the University of Oxford. His work focuses on applying symbolic simulation and symbolic indexing to the verification of the CHERI-CVA6 processor. Before coming to Oxford, he studied Mathematics and Computer Science at Occidental College.
Leo Stephan
Researcher
Maxwell Pettett
Researcher
Maxwell is an MSc student in Computer Science at the University of Oxford. His work focuses on the formal verification of CHERI safety properties in CHERI-CVA6 via ISA-oblivious proofs. His background from studying Computer Science at Cambridge includes architecture and GPU algorithms.
Visitors
We welcome visitors from both academia and industry who are interested in hardware formal verification. If you would like to visit, discuss a project, please get in touch with Tom at Tom.Melham@cs.ox.ac.uk.
Sponsors
