Виталик Бутерин считает, что ИИ+ формальная верификация - будущее разработки ПО

Виталик подробно описывает новую волну интереса к формальной верификации в Ethereum и шире в части разработки безопасного ПО.

Суть в том, чтобы писать математические доказательства корректности кода, которые можно автоматически проверить ИИ.

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

ИИ может сильно упростить и ускорить этот процесс. Вместо того, чтобы человек вручную писал сложные математические доказательства, ИИ будет помогать или даже почти полностью делать эту работу.

Есть уже примеры, тут мы писали и тут.

В итоге мы получим:

• Код, который математически проверен;
• Значительно более безопасное ПО;
• Намного более эффективный процесс разработки.

По мнению Виталика, это важно для:

1. Ethereum и блокчейн в целом;
2. ZK-системы (zero-knowledge proofs);
3. Консенсус (механизмы, по которым ноды договариваются);
4. Криптография.

Виталик говорит, что формальная верификация не даёт 100% гарантии. Она доказывает, что код соответствует спецификации, но сама спецификация может быть неверной, или могут быть проблемы на другом уровне, например, в аппаратном обеспечении.