TechFlow reports, according to an official WeChat public account announcement, that CertiK, a global blockchain and smart contract security company, has completed advanced formal verification of Ant Group's innovative open cross-platform Trusted Execution Environment (TEE) HyperEnclave.
HyperEnclave, an open cross-platform software TEE developed by Ant Group's Trusted Native Technology team, aims to enhance the efficiency and compatibility of Ant Group's privacy-preserving computing workloads.
CertiK's formal verification process involved applying machine-checked proofs to verify the correctness and security of HyperEnclave's code, including its most critical component: RustMonitor. Using its proprietary advanced system code verification methodology, CertiK developed a customized framework specifically for verifying Rust code.
