형식 검증 자체는 새로운 개념이 아니다. 수십 년 전부터 존재했지만, 실제 개발에서 활용하기에는 너무 어렵고 시간이 많이 드는 방식이었다.
부테린은 AI가 이 장벽을 낮출 수 있다고 본다.
AI 기반 코딩 도구는 다음과 같은 작업을 도울 수 있다.
이 덕분에 과거에는 극도로 제한된 연구 프로젝트에서만 가능했던 형식 검증이 실제 블록체인 개발 과정에서도 사용 가능한 도구로 변하고 있다.
또 다른 변화는 개발 속도 자체다. 한 AI 기반 코딩 실험에서는 약 70만 줄 규모의 이더리움 클라이언트 프로토타입이 몇 주 만에 만들어졌으며, 이는 이더리움 로드맵의 여러 기능을 포함하고 메인넷과 동기화까지 가능했다.
부테린은 이런 생산성 향상이 단순히 개발 속도를 높이는 데만 쓰여서는 안 되며, 더 깊은 테스트와 형식 검증 같은 보안 강화 작업에 투자되어야 한다고 강조했다.
이더리움의 미래 업그레이드 중 일부는 매우 복잡하고 보안 중요도가 높기 때문에, 형식 검증의 이점을 특히 크게 얻을 수 있는 분야로 꼽힌다.
이더리움의 장기 로드맵에서 영지식 증명(Zero‑Knowledge) 기술은 핵심 요소다. ZK‑EVM은 향후 주요 검증 방식으로 자리 잡을 가능성이 있으며, 약 2028년경 주요 검증 방식이 될 수 있다는 전망도 나온다.
이 시스템은 암호학적 회로와 증명 구조가 매우 복잡하기 때문에, 형식 검증을 적용하면 치명적인 구현 버그 위험을 크게 줄일 수 있다.
부테린이 강조하는 이더리움의 핵심 목표는 보안, 탈중앙화, 사용자 통제권이다.
합의 알고리즘, 클라이언트 구현, 암호 알고리즘 같은 핵심 코드가 형식적으로 검증된다면, 네트워크가 설계 의도대로 정확히 동작한다는 보장을 더 강하게 만들 수 있다.
단기 로드맵에는 처리 용량 확대와 확장성 개선을 위한 여러 프로토콜 업그레이드가 포함되어 있다.
특히 성능에 민감한 저수준 최적화 코드는 작은 버그 하나로도 큰 문제를 일으킬 수 있기 때문에, 수학적으로 검증된 구현이 매우 유용할 수 있다.
이더리움은 스마트 계약 기반 지갑, 프라이버시 기능, 계정 추상화(account abstraction) 지원을 확대할 계획이다.
이 시스템들은 인증, 거래 검증, 암호학적 증명 등 복잡한 로직을 포함하므로 형식 검증이 오류를 줄이는 데 도움이 된다.
연구자들은 장기적으로 양자 컴퓨터에 대비한 암호 체계도 검토하고 있다.
암호 알고리즘 전환은 모든 블록체인에서 매우 위험한 단계이기 때문에, 형식적으로 검증된 구현은 새로운 알고리즘이 제대로 동작한다는 강력한 보증을 제공할 수 있다.
부테린은 AI 기반 형식 검증을 만능 해결책으로 보지는 않는다.
가장 큰 한계는 형식 검증이 개발자가 정의한 속성만 증명할 수 있다는 점이다. 만약 명세 자체가 잘못됐거나, 경제적 설계나 인센티브 구조에 문제가 있다면 검증 과정에서도 그 문제는 발견되지 않는다.
또한 몇 가지 현실적인 문제도 존재한다.
부테린 역시 AI로 빠르게 만들어진 구현에는 **“상당한 버그가 있을 수 있다”**며 실제 배포 전에는 충분한 테스트와 보안 검증이 필요하다고 강조했다.
AI가 발전할수록 공격자 역시 더 쉽게 취약점을 찾을 가능성이 있다. 복잡한 소프트웨어 시스템에서 보안 취약점을 자동으로 탐지하는 능력이 커질 수 있기 때문이다.
이 때문에 블록체인 같은 핵심 인프라는 단순한 테스트를 넘어 수학적으로 검증된 소프트웨어 수준의 보안을 필요로 하게 될 수 있다.
AI가 형식 검증의 어려운 부분을 자동화한다면, 미래의 암호화폐 인프라는 단순히 “잘 테스트된 코드”가 아니라 “수학적으로 올바름이 증명된 코드” 위에서 운영되는 방향으로 발전할 가능성이 있다.