CertiK has successfully completed the formal verification of HyperEnclave, an innovative open and cross-platform Trusted Execution Environment (TEE) from Ant Group’s Trust Native Technology team. This marks the first time in the industry that such an in-depth formal verification process has been completed for a TEE.

Ant Group’s Trust Native Technology team developed HyperEnclave as an open and cross-platform TEE to increase the efficiency and compatibility of its privacy-preserving computing workload. CertiK, using its exclusive world-class advanced formal verification technologies, successfully verified the security and technical correctness of HyperEnclave's core components.

CertiK's formal verification process involved applying machine-checked proofs to validate the correctness and security of HyperEnclave's code, including its most critical component: RustMonitor. CertiK applied its exclusive advanced systems code verification approach and developed a customized framework for verifying Rust code.

With extensive experience in formal verification and a number of innovative applications of the process, the CertiK team was able to accurately evaluate the security of HyperEnclave.

"CertiK is proud to work on this ground-breaking project," said Prof. Ronghui Gu, co-founder of CertiK and inventor of the exclusive approach to systems code verification. "Our work on this formal verification is a testament to our commitment to pushing the boundaries of security in the ever-evolving tech and Web3 landscapes."

CertiK looks forward to further auditing, testing, and formal verification of other confidential computing building blocks.