비탈릭 부테린은 이더리움 소프트웨어 개발에 있어 형식 검증이 중요한 진전이라고 강조했습니다. 이 방법은 Lean과 같은 언어를 사용해 자동으로 검증 가능한 수학적 증명을 생성함으로써, 암호화 통신 프로토콜, ZK-STARKs, 합의 알고리즘과 같은 복잡한 기술의 보안을 강화합니다. AI의 통합은 이 과정을 더욱 간소화하여 검증 증명과 어셈블리 코드를 자동으로 생성할 수 있게 했습니다. 부테린은 형식 검증의 핵심 가치는 안전한 핵심 코드와 덜 안전한 구성 요소를 분리할 수 있다는 점에 있다고 강조하며, 이를 통해 사용자가 전체 코드베이스를 검토하지 않고도 보안 증명을 확인할 수 있다고 말합니다. 그러나 그는 형식 검증이 만병통치약은 아니며, 인간의 의도와 일치함을 보장할 수 없고 검증 실패 사례도 있었다고 경고합니다. 이러한 도전에도 불구하고, 형식 검증은 AI 생성 코드의 증가 속에서 네트워크 보안을 강화하는 유망한 길을 제시합니다.