Movement는 aptos-core 저장소에 대규모 형식 검증 인프라를 병합했습니다. 완전한 Lean 4 바이트코드 모델과 정제 증명 프레임워크가 도입되어 수학적 사양과 Move VM의 자동 차분 테스팅을 실현합니다.
새로운 시스템은 Lean 4에서 Move 추상화를 정의합니다. `Value`, `Instr`, `State`, `Step`, `Native`, `Programs`가 포함되며, 실제 역어셈블리 프로그램을 기반으로 한 바이트코드 레벨 의미론에 특히 초점을 맞춥니다. 정제 증명은 형식 모델과 실제 VM 구현 간의 정확성 관계를 수립하며, 표준 라이브러리에 대해 검증된 `vector::contains` 연산의 커널 검증 정리를 포함합니다.
차분 테스트 하네스(`move-lean-difftest`)는 벡터 연산, 이진 표준 직렬화(BCS), 해시 함수에 걸쳐 공유 테스트 오라클에서 실제 Move VM과 Lean 평가기를 자동으로 비교합니다. 이 Rust와 Lean 구현을 직접 비교하는 양방향 검증 접근 방식은 시맨틱 차이의 조기 감지를 가능하게 하고 프로토콜 정확성에 대한 신뢰를 강화합니다.
프레임워크는 포괄적인 문서와 도구를 포함합니다. `lake build`는 Lean 증명을 컴파일하고, `difftest.sh` 스크립트는 모든 검증 스위트를 실행하며, 보조 Move 골든 테스트는 바이트 레벨 일관성을 검증합니다. 저장소는 또한 Ristretto 및 SHA3-512와 같은 암호화 프리미티브를 위한 `AptosStd` 레이아웃을 등록하여 형식 사양이 프로덕션 구현과 일치하도록 보장합니다.
개발자는 `elan`을 통해 Lean 4(4.24.0)를 설치하고 Lake 빌드 시스템을 실행하여 증명을 로컬에서 검증할 수 있습니다. 완전한 실행 가이드와 바이트코드 모델 로드맵은 저장소의 형식 검증 README 파일에 문서화되어 있으며, 진행 중인 프로토콜 개발과 제3자 감사를 위해 이 인프라를 접근 가능하게 합니다.