Buterin stawia na formalną weryfikację. Fundacja Ethereum: wąskim gardłem nie jest znajdowanie błędów, lecz triaż

Vitalik Buterin odrzucił tezę, że hakerzy wspierani przez AI czynią cyberbezpieczeństwo praktycznie niewygrywalnym. W poście z 17 września przekonywał, że obrońcy mogą zyskać przewagę, jeśli wykorzystają formalną weryfikację — technikę, w której matematyczny dowód potwierdza, że program zachowuje się zgodnie ze specyfikacją. Swój argument zakotwiczył w deklaracji, że około 90 proc. jego majątku netto pozostaje w kryptowalutach. Jak napisał, zakłada więc, że bezpieczne systemy cyfrowe przetrwają silniejsze zautomatyzowane ataki.

„Coraz częściej słyszę, że hakerzy AI oznaczają zagładę cyberbezpieczeństwa. Nie zgadzam się. Uważam, że cyberbezpieczeństwo z natury sprzyja obronie, gdy ludzie w końcu się ogarną” — napisał Buterin. Formalną weryfikację porównuje do dowodzenia twierdzeń matematycznych: wystarczająco zdolna AI mogłaby pomóc udowodnić, że „ten program jest bezpieczny”, nawet gdy sam kod jest skomplikowany.

Zastrzeżenie jest jednak istotne. Dowód potwierdza zgodność z konkretną specyfikacją, a nie to, czy twórcy poprawnie zdefiniowali wszystkie właściwości bezpieczeństwa. Zbyt wąskie rozumienie bezpieczeństwa pomija ataki wymierzone w protokoły, serwery, bazy danych, warstwy sieciowe czy pamięci podręczne. Dlatego — argumentuje Buterin — weryfikować trzeba więcej elementów całego systemu, zamiast uznawać niewielką grupę modułów za krytyczne dla bezpieczeństwa.

Triaż, nie samo znajdowanie błędów

To nie jest wyłącznie teoria. W lipcu zespół Protocol Security Fundacji Ethereum poinformował, że skoordynowane agenty AI znalazły realny błąd w implementacji Gossipsub w Rust libp2p. Usterka — zdalnie osiągalne przepełnienie arytmetyczne wywoływane spreparowaną wiadomością PRUNE — została zarejestrowana jako CVE-2026-34219, a poprawka trafiła do wersji 0.49.4.

Ważniejsze od samego znaleziska jest to, co Fundacja powiedziała o procesie. Najtrudniejsze nie było wykrycie podatności, lecz odsianie fałszywych trafień. Agenty AI często generowały przekonujące raporty o nieosiągalnych ścieżkach wykonania, błędach widocznych tylko w trybie debugowania i dowodach formalnych, które technicznie przechodziły, ale dowodziły słabszej właściwości, niż zamierzano. Niezależna reprodukcja pozostawała warunkiem przyjęcia znaleziska, a badacze musieli ustalić, czy każdy kandydat jest osiągalny i istotny w produkcji. AI potrafi więc wygenerować podatności masowo, ale wąskim gardłem zostaje ludzki triaż.

Formalna weryfikacja w planie badań

Fundacja Ethereum włączyła formalną weryfikację do programu badań protokołu. W aktualizacji priorytetów z 7 września zapowiedziała, że będzie to narzędzie przekrojowe dla kilku obszarów badawczych, z horyzontem prac do 2029 r. — od prywatności i stanu po bezpieczeństwo postkwantowe. Osobny projekt, better.codes, uruchomiony w sierpniu, łączy agenty AI z dowodami sprawdzanymi maszynowo: badacze kierują systemy AI na problem poprawności kryptograficznej zapisany w Lean, a jądro Leana sprawdza, czy przesłany dowód spełnia ustalony teoremat.

AI po stronie atakujących

Anthropic w raporcie z września opisał z kolei, jak złośliwi aktorzy używają AI do automatyzacji badań nad podatnościami, tworzenia exploitów i prowadzenia kampanii przeciwko wielu celom. Część operatorów utrzymywała zautomatyzowane workflow zdolne do ciągłego badania podatności. Do 26 sierpnia, według danych samej firmy, ujawniono 2300 podatności znalezionych przez AI w 392 projektach open source, z czego 421 doczekało się poprawek.

Wpis Buterina nie zapowiada żadnego konkretnego EIP, daty wdrożenia ani obowiązku formalnej weryfikacji w Ethereum. To kontynuacja kierunku, który Fundacja już realizuje — i deklaracja, że obrona może wykorzystać AI skuteczniej niż atak. Buterin sam wskazuje przy tym, gdzie leży granica tego argumentu: dowód sprawdza zgodność ze specyfikacją, ale nie to, czy specyfikacja opisuje wszystko, co powinna.