Foresight News 消息，據網易新聞消息，Web3 安全公司 CertiK 與螞蟻集團旗下的螞蟻密算聯合發佈最新研究工作，對下一代開源通用操作系統「星綻（Asterinas）」的核心組件進行了形式化驗證。星綻基於 Rust 開發，兼容 Linux 應用。此項工作展示了對 Rust 操作系統形式化驗證的重要進展，推動其安全性邁向「數學證明級」標準，併為提升下一代通用操作系統的安全性提供了新的思路。

此前，CertiK 已成功為螞蟻密算的 TEE 平臺 HyperEnclave 完成形式化驗證。