TechFlow 보도에 따르면, 5월 19일 비탈릭 부테린(Vitalik Buterin)이 개인 블로그를 통해 ‘형식적 검증(Formal Verification)’ 기술이 이더리움 연구 커뮤니티 및 더 광범위한 컴퓨팅 분야에서 급속히 부상하고 있다고 밝혔다. 이 기술은 리안(Lean) 등의 수학적 증명 도구를 사용해 자동으로 검증 가능한 수학적 증명을 작성함으로써 코드의 정확성을 검증하는 것으로, 연구자들은 이를 ‘소프트웨어 개발의 궁극적 형태’라고 부른다. 글에서는 형식적 검증이 특히 목표는 단순하지만 구현은 복잡한 분야—예컨대 양자 내성 서명(quantum-resistant signatures), STARKs, 합의 알고리즘, ZK-EVM 등 이더리움의 핵심 기술—에 매우 적합하다고 지적했다. 또한 비탈릭 부테린은 형식적 검증이 만능은 아니라고 강조하며, 인간의 의도를 완전히 포착하지 못한다는 한계와 사양 누락(specification omissions), 일부 코드가 검증 범위에 포함되지 않는 것과 같은 위험 요소가 존재한다고 설명했다.
이에 대해 그는 낙관적인 전망을 제시했다. 즉, 인공지능(AI)과 형식적 검증의 결합은 상호 보완적인 관계를 형성할 것이며, AI는 대량의 코드를 효율적으로 생성하는 역할을 담당하고, 형식적 검증은 그 정확성을 보장하는 역할을 맡게 될 것이라고 예측했다. 향후 소프트웨어 보안 아키텍처는 ‘보안 코어(security core) + 비보안 엣지 샌드박스(unsecure edge sandbox)’ 모델로 진화할 것이며, 이더리움은 그 중 하나의 주요 보안 코어가 될 것이라고 전망했다.
