PANews 3月14日消息，，據網易新聞消息，Web3安全巨頭CertiK與螞蟻集團旗下的螞蟻密算聯合發佈了最新研究工作，對下一代開源通用操作系統——星綻(Asterinas)——的核心組件進行了形式化驗證。星綻基於Rust開發，兼容Linux應用。此項工作展示了對Rust操作系統形式化驗證的重要進展，推動其安全性邁向“數學證明級”標準，併爲提升下一代通用操作系統的安全性提供了新的思路。此前，CertiK已成功爲螞蟻密算的TEE平臺HyperEnclave完成形式化驗證。