비탈릭 부테린은 최신 기사에서 이더리움의 최첨단 연구에서 새롭게 등장하는 패러다임에 대해 논의합니다. 이 접근법은 EVM 바이트코드, 어셈블리 또는 Lean으로 직접 코딩하고, Lean에서 자동으로 검증되는 수학적 증명을 통해 정확성을 확인하는 것을 포함합니다. AI 지원 형식 검증은 특히 STARK, ZK-EVM, 양자 저항 서명 및 합의 알고리즘과 같은 중요한 보안 모듈의 코드 효율성과 보안을 모두 향상시킬 것으로 기대됩니다. 그러나 부테린은 형식 검증이 완벽하지 않으며, 증명 범위의 불완전성, 명세 오류 또는 하드웨어 사이드 채널로 인해 실패할 수 있다고 경고합니다. 그는 미래 소프트웨어가 "보안 코어"와 "비보안 엣지"로 나뉘게 될 것이며, 이더리움이 주요 보안 코어가 될 것으로 전망합니다.