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