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