PANews는 5월 18일 비탈릭 부테린이 이더리움 커뮤니티가 Lean과 같은 정형 도구를 사용하여 EVM 바이트코드 및 RISC-V 어셈블리와 같은 기본 언어로 직접 코드를 작성하고 기계 검증 가능한 수학적 증명을 통해 정확성과 보안을 보장하는 실험을 진행하고 있다고 밝힌 블로그 게시물을 보도했습니다. 비탈릭은 정형 검증을 통해 Signal, TLS, STARK, ZK-EVM과 같은 암호화 통신 프로토콜, 합의 알고리즘 및 EVM 구현의 엔드투엔드 보안과 동등성을 검증할 수 있으며, AI가 자동으로 버그를 찾아내는 새로운 환경에서 방어자의 이점을 크게 강화할 수 있다고 지적했습니다. 그러나 그는 정형 검증이 만능 해결책은 아니며 모델링되지 않은 가정, 사이드 채널, 노출되지 않은 모듈과 같은 위험을 쉽게 간과할 수 있다고 강조했습니다. 비탈릭은 미래의 소프트웨어는 소수의 "보안 코어"를 중심으로 구축될 것이며, AI가 대부분의 코드 생성을 처리하고 정형 검증이 핵심 인프라의 보안을 보장하는 역할을 담당할 것이라고 예상했습니다.