비탈릭: AI 보조 형식 검증은 코드 효율성과 안전성을 동시에 향상시킬 것으로 기대된다

비탈릭 부테린은 블록체인 보안 분야에서 형식적 검증(Formal Verification)의 응용 전망에 대해 논의하는 글을 발표했습니다.

이 글에서는 이더리움 최전선 연구 개발에서 새로운 패러다임이 떠오르고 있으며, EVM 바이트코드, 어셈블리 또는 Lean을 사용하여 코드를 직접 작성하고 Lean에서 자동으로 검증 가능한 수학적 증명을 통해 그 정확성을 검증한다고 언급했습니다. 연구자 요이치 히라이는 이 패러다임을 "소프트웨어 개발의 궁극적인 형태"라고 부릅니다.

비탈릭은 AI 보조 형식적 검증이 코드의 효율성과 안전성을 동시에 향상시킬 것으로 기대하며, 특히 STARK, ZK-EVM, 양자 저항 서명 및 합의 알고리즘과 같은 안전 핵심 모듈에 적합하다고 생각합니다.

이 글은 또한 형식적 검증이 만능이 아니며, 증명 범위의 불완전성, 사양 오류, 하드웨어 측면 채널 등의 문제로 인해 실패할 수 있다고 강조합니다. 미래에는 소프트웨어가 "안전 핵심"과 "비안전 경계"로 분화될 수 있으며, 이더리움은 중요한 안전 핵심 중 하나가 될 것입니다.