이더리움, 린 4로 3개 업그레이드 합의 검증

이더리움(ETH) 연구팀이 린 4(Lean 4)로 Fulu·Gloas·Heze 업그레이드의 합의 규격을 구현하고 수학적으로 검증하는 프로젝트를 추진하고 있다. 여러 클라이언트가 같은 규격을 다르게 해석해 체인이 갈라지는 위험을 줄이려는 작업이다.

이더리움 프로토콜 펠로십(EPF)과 인비저블 가든(Invisible Garden) 연구팀은 21일 이더리움 리서치 포럼 게시글을 통해 프로젝트 ‘Etheorem’의 진행 상황을 공개했다. Etheorem은 정리 증명 언어인 린 4로 이더리움 합의 규격을 실행 가능한 형태로 구현하고, 코드 테스트를 넘어 핵심 논리를 수학적으로 검증하는 것을 목표로 한다.

이더리움은 여러 개발팀이 만든 합의 클라이언트를 함께 사용하는 구조다. 각 클라이언트가 같은 규격을 구현하더라도 세부 로직을 다르게 이해하면 블록 유효성 판단이나 체인 선택 결과가 달라질 수 있다. Etheorem은 이런 해석 차이를 형식 검증으로 점검한다.

프로젝트는 Fulu·Gloas·Heze 업그레이드에 해당하는 합의 규격을 구현했다. 상태 전환과 포크 선택 로직을 실행할 수 있으며, 이더리움 공식 합의 테스트 벡터와 대조해 구현 결과를 확인하고 있다. Fulu에는 데이터 가용성 샘플링 관련 사양이, Gloas에는 실행 페이로드 경매 구조인 ePBS 관련 요소가 포함된다. Heze에는 검열 저항을 위한 포함 목록 구조가 반영돼 있다.

Etheorem의 기반에는 SSZ(Simple Serialize) 라이브러리인 SizzLean이 있다. 이 라이브러리는 합의 데이터의 직렬화·역직렬화와 머클 트리 계산에 필요한 일부 속성을 린 커널에서 검증한다. 검증 대상에는 직렬화된 데이터가 원래 값으로 되돌아오는지, 서로 다른 값이 같은 인코딩을 갖지 않는지, 인코딩 크기가 사전에 계산된 한도를 넘지 않는지가 포함된다.

프로젝트는 검증된 코드와 실제 실행 코드 사이의 차이를 줄이는 데도 초점을 맞췄다. 같은 규격 정의를 검증 환경과 실행 환경에서 함께 사용해 증명에 쓰인 로직과 실제 클라이언트의 로직이 달라지는 문제를 줄이겠다는 구상이다. 형식 검증이 적용 범위 안의 논리를 점검하는 방식인 만큼, 전체 이더리움 클라이언트를 대체하는 단계는 아니다. 블록체인 프로토콜의 린 4 형식 검증 사례도 핵심 로직을 모델로 재현해 검증 범위를 설정하는 방식으로 진행됐다.

테스트 벡터를 통과했다는 사실도 운영 환경의 안정성이나 정식 릴리스를 의미하지 않는다. 프로젝트는 향후 증명 범위를 확대할 계획을 제시했다.