이더리움, Lean 4로 합의 검증 진전

프로젝트 개요

이더리움의 연구팀은 Lean 4 증명 보조 도구를 사용하여 Fulu, Gloas, Heze 업그레이드의 합의 사양을 구현하고 수학적으로 검증하는 'Etheorem'이라는 중요한 프로젝트를 진행하고 있다. 이 노력은 여러 클라이언트가 동일한 사양을 다르게 해석할 때 발생할 수 있는 체인 분할의 위험을 줄이는 것을 목표로 한다.

Etheorem의 목표

Etheorem의 주요 목표는 Lean 4에서 이더리움 합의 사양의 기능적 구현을 만드는 것으로, 단순한 코드 테스트를 넘어 핵심 논리를 수학적으로 검증하는 것이다. 이 프로젝트는 이더리움 프로토콜 펠로우십(EPF)과 인비저블 가든 연구팀이 이더리움 연구 포럼에 게시한 글을 통해 진행 상황을 공개했다.

기술적 구현

Etheorem은 세 가지 업그레이드에 대한 합의 사양을 성공적으로 구현했다. 상태 전환 및 포크 선택 논리를 실행할 수 있으며, 그 결과를 공식 이더리움 합의 테스트 벡터와 비교한다. 업그레이드의 주요 특징은 다음과 같다:

• Fulu: 데이터 가용성 샘플링과 관련된 사양.
• Gloas: 실행 페이로드 경매 구조(ePBS)와 관련된 요소.
• Heze: 포함 목록 구조를 통한 검열 저항 기능.

검증 기술

이 프로젝트는 합의 데이터 직렬화, 비직렬화 및 머클 트리 계산에 필요한 중요한 속성을 검증하기 위해 SSZ(Simple Serialize) 라이브러리인 SizzLean을 활용한다. 검증 과정에서는 직렬화된 데이터가 원래 값으로 되돌아가는지, 서로 다른 값이 동일한 인코딩을 공유하지 않는지, 인코딩 크기가 미리 정의된 한계를 초과하지 않는지를 확인한다.

이 이니셔티브는 검증 환경과 실행 환경 모두에서 동일한 사양 정의를 사용하여 검증된 코드와 실제 실행 코드 간의 불일치를 줄이는 데에도 중점을 두고 있다. 그러나 이 공식 검증이 전체 이더리움 클라이언트 생태계를 대체하는 것은 아니며, 테스트 벡터를 통과한다고 해서 운영 안정성이나 공식 출시 준비가 보장되는 것은 아니다. 이 프로젝트는 향후 증명의 범위를 확장할 계획이다.