PANews reported on March 14 that according to NetEase News, Web3 security giant CertiK and Ant Group's Ant Computing jointly released the latest research work, which formally verified the core components of the next-generation open source general-purpose operating system, Asterinas. Asterinas is developed based on Rust and is compatible with Linux applications. This work demonstrates important progress in the formal verification of the Rust operating system, pushing its security towards the "mathematical proof level" standard, and provides new ideas for improving the security of the next generation of general-purpose operating systems. Previously, CertiK has successfully completed formal verification for Ant Computing's TEE platform HyperEnclave.