Виталик Бутерин, сооснователь Ethereum, предложил использовать сочетание искусственного интеллекта и формальной верификации как основной метод разработки ПО. В публикации от 18 мая он отметил, что ИИ способен быстро генерировать код, но часто допускает ошибки. Формальная верификация позволяет математически доказать корректность работы программы, что критически важно для безопасности смарт-контрактов.
Бутерин выделил систему Lean как ключевой инструмент для создания проверяемых доказательств. По его мнению, этот подход необходим для внедрения постквантовой криптографии и работы со сложными доказательствами с нулевым разглашением. В качестве примеров практического применения он привел проекты Arklib для реализации STARKs и evm-asm, упрощающий формальный анализ виртуальной машины Ethereum.
Среди ограничений метода Бутерин назвал риск неверной спецификации и уязвимость аппаратного обеспечения, которую невозможно устранить программными методами. Тем не менее, он считает, что ИИ делает формальную верификацию экономически доступной, снижая затраты на написание доказательств. Ранее эта технология применялась в основном в аэрокосмической и оборонной отраслях.
