Головний науковець Certora Mooly Sagiv вважає, що найбільший ризик у сфері криптографічної безпеки полягає не у складних помилках у коді, а у простих проблемах, таких як управління ключами та людські помилки. На конференції Breakpoint 2025 він підкреслив, що аудит не може гарантувати безпеку, і виступив за поєднання формальної верифікації з людським оглядом. Sagiv зазначив, що формальна верифікація, інтегрована у конвеєр безперервної інтеграції (CI), може виявити «невідомі невідомі», але попередив, що її ефективність залежить від правильного визначення властивостей. Він також зменшив значення штучного інтелекту як загрози для виживання, вважаючи його одночасно інструментом для атакуючих і захисників.