Виталик Бутерин в своей последней статье обсуждает новую парадигму, которая возникает в передовых исследованиях Ethereum. Этот подход предполагает прямое программирование с использованием байткода EVM, ассемблера или Lean и проверку корректности с помощью математических доказательств, автоматически проверяемых в Lean. Ожидается, что формальная верификация с поддержкой ИИ повысит как эффективность кода, так и безопасность, особенно для критически важных модулей безопасности, таких как STARK, ZK-EVM, квантово-устойчивые подписи и алгоритмы консенсуса. Однако Бутерин предупреждает, что формальная верификация не является безошибочной, так как она может потерпеть неудачу из-за неполного охвата доказательств, ошибок в спецификациях или побочных каналов аппаратного обеспечения. Он предполагает, что в будущем программное обеспечение разделится на «ядра безопасности» и «небезопасные периферии», при этом Ethereum готов стать ключевым ядром безопасности.