leanCL 상태 전이 Lean 4, 증명으로 검증하는 합의 규칙
Strawmap J* (2028~29) · leanCL STF in Lean 4
차세대 합의 계층 leanCL의 핵심 규칙인 상태 전이 함수를 증명 도구 Lean 4로 작성합니다. 코드가 맞는지 테스트가 아니라 수학적 증명으로 확인하자는 작업입니다.
왜 필요한가
합의 계층은 블록이 들어올 때마다 체인의 상태를 다음 상태로 바꾸는 규칙을 따릅니다. 이 규칙을 상태 전이 함수(State Transition Function, STF)라고 부릅니다. 지금은 이 규칙을 파이썬 명세로 적고 각 클라이언트 팀이 자기 언어로 다시 구현한 뒤 테스트로 맞춰 봅니다. 테스트는 미리 떠올린 경우만 확인하므로, 명세에 숨은 모순이나 아무도 생각하지 못한 상황은 잡아내지 못합니다. leanCL은 이더리움 재단이 연구하는 차세대 합의 계층(lean consensus layer)입니다. 양자 내성 서명 같은 새 부품이 들어가 규칙을 처음부터 다시 쓰게 되는데, 이때 상태 전이 함수를 Lean 4로 작성하자는 것이 이 항목입니다. Lean 4는 프로그래밍 언어이자 정리 증명 도구(theorem prover)입니다. 코드와 함께 그 코드가 지켜야 할 성질을 명제로 적으면, 사람이 아니라 컴퓨터가 증명이 맞는지 검사합니다. leanCL의 lean과 Lean 4의 Lean은 우연히 같은 단어일 뿐 서로 다른 것입니다. 이렇게 하면 명세가 곧 검증된 참조 구현이 되고 클라이언트 구현의 어긋남을 찾기도 쉬워집니다. 프로토콜 규칙을 바꾸는 항목이 아니라 명세와 클라이언트를 만드는 방식에 관한 작업입니다. Strawmap의 2028~29년 칸은 예상일 뿐 확정된 일정이 아닙니다.
어떻게 동작하나
- 규칙을 Lean 4로 적습니다 블록을 받아 다음 상태를 내는 상태 전이 함수를 Lean 4 코드로 작성합니다. 이 코드가 leanCL 합의 규칙의 공식 명세 역할을 합니다.
- 지켜야 할 성질을 명제로 씁니다 예를 들어 확정된 블록은 뒤집히지 않는다, 잘못된 서명이 담긴 블록은 거부된다 같은 성질을 수학 명제로 적습니다.
- 컴퓨터가 증명을 검사합니다 Lean 4는 적어 둔 명제가 코드에서 실제로 성립하는지 증명을 검사합니다. 증명이 안 되는 자리는 명세에 빈틈이 있다는 신호입니다.