Certora首席科學家Mooly Sagiv認為，最大的加密安全風險並非複雜的程式碼漏洞，而是密鑰管理和人為錯誤等更簡單的問題。在Breakpoint 2025大會上，他強調審計並不能保證安全，並提倡將形式化驗證與人工審查相結合。Sagiv指出，集成到持續整合（CI）管道中的形式化驗證可以發現“未知的未知”，但他警告說，其有效性取決於屬性的正確定義。他還淡化了人工智慧作為生存威脅的重要性，認為它既是攻擊者的工具，也是防禦者的工具。