Все о блокчейн/мозге/space/WEB 3.0 в России и мире

Виталик Бутерин считает, что ИИ+ формальная верификация - будущее разработки ПО Виталик подробно описывает новую волну интереса к формальной верификации в Ethereum и шире в части разработки безопасного ПО. Суть в том, чтобы писать математические доказательства корректности кода, которые можно автоматически проверить ИИ. Формальная верификация - это, когда ты не просто тестируешь программу, а доказываешь математически, что она ведёт себя именно так, как должна при любых входных данных. ИИ может сильно упростить и ускорить этот процесс. Вместо того, чтобы человек вручную писал сложные математические доказательства, ИИ будет помогать или даже почти полностью делать эту работу. Есть уже примеры, тут мы писали и тут. В итоге мы получим: • Код, который математически проверен; • Значительно более безопасное ПО; • Намного более эффективный процесс разработки. По мнению Виталика, это важно для: 1. Ethereum и блокчейн в целом; 2. ZK-системы (zero-knowledge proofs); 3. Консенсус (механизмы, по которым ноды договариваются); 4. Криптография. Виталик говорит, что формальная верификация не даёт 100% гарантии. Она доказывает, что код соответствует спецификации, но сама спецификация может быть неверной, или могут быть проблемы на другом уровне, например, в аппаратном обеспечении.