비탈릭: AI 보조 형식 검증은 코드 효율성과 안전성을 동시에 향상시킬 것으로 기대된다
비탈릭 부테린은 블록체인 보안 분야에서 형식적 검증(Formal Verification)의 응용 전망에 대해 논의하는 글을 발표했습니다.이 글에서는 이더리움 최전선 연구 개발에서 새로운 패러다임이 떠오르고 있으며, EVM 바이트코드, 어셈블리 또는 Lean을 사용하여 코드를 직접 작성하고 Lean에서 자동으로 검증 가능한 수학적 증명을 통해 그 정확성을 검증한다고 언급했습니다. 연구자 요이치 히라이는 이 패러다임을 "소프트웨어 개발의 궁극적인 형태"라고 부릅니다.비탈릭은 AI 보조 형식적 검증이 코드의 효율성과 안전성을 동시에 향상시킬 것으로 기대하며, 특히 STARK, ZK-EVM, 양자 저항 서명 및 합의 알고리즘과 같은 안전 핵심 모듈에 적합하다고 생각합니다.이 글은 또한 형식적 검증이 만능이 아니며, 증명 범위의 불완전성, 사양 오류, 하드웨어 측면 채널 등의 문제로 인해 실패할 수 있다고 강조합니다. 미래에는 소프트웨어가 "안전 핵심"과 "비안전 경계"로 분화될 수 있으며, 이더리움은 중요한 안전 핵심 중 하나가 될 것입니다.