深潮 TechFlow 消息，據官方微信公眾號消息，全球區塊鏈和智能合約安全公司CertiK已經完成對螞蟻集團創新開放式跨平臺可信執行環境（TEE）HyperEnclave的先進形式化驗證。

據悉，螞蟻集團開放跨平臺軟件可信執行環境HyperEnclave由其可信原生技術團隊開發，旨在提高螞蟻集團隱私保護計算工作負載的效率和兼容性。

CertiK的形式化驗證過程涉及應用機器檢查證明來驗證HyperEnclave代碼的正確性和安全性，其中包括了最關鍵的組件部分：RustMonitor。CertiK應用了其獨有的先進系統代碼驗證方法，開發了一個用於驗證Rust代碼的定製框架。