Welcome to the Hafnium verification project. Hafnium is an open source project to build a secure hypervisor that allows system designers to achieve confidentiality and integrity of sensitive data with fine-grained security domains. One of the top priorities of Project Oak is to provide higher assurance of Hafnium's security using formal verification.
There are currently two projects going on in this repo.
- Formal verification: https://github.com/project-oak/hafnium-verification/tree/hfo2/coq-verification
- Rewriting in Rust: https://github.com/project-oak/hafnium-verification/tree/hfo2/hfo2
This is not an officially supported Google product.