После неоднозначного хардфорка Gnosis Chain, нацеленного на возврат $9,4 млн, похищенных в результате взлома Balancer, Бутерин заявил, что в 2030-х годах нельзя будет сказать, что «ошибки неизбежны, невозможно написать код без ошибок».

Соучредитель Ethereum предположил, что прорывным решением может стать многоуровневая избыточность, позволяющая отфильтровывать пробелы между замыслом и реализацией. Он указал на системы типов как на одну из форм избыточности, а на формальную проверку конкретных утверждений о коде как на другой уровень.

Формальная верификация позволяет выявить такие проблемы, как целочисленное усечение и переполнение, повторный вход и неэффективная оптимизация использования газа, которые могут ускользнуть от внимания аудиторов и тестировщиков. В то же время традиционное тестирование позволяет только проверить наличие ошибок, но не их отсутствие.

Бутерин также отметил, что в некоторых программах ошибки будут появляться и дальше, потому что в определённых случаях функциональность важнее совершенства. Но у разработчиков, которые уделяют приоритетное внимание безопасности, будут инструменты для создания действительно безошибочного кода.