저수준 실행 코드(low-level executable code)를 그 동작에 대한 고수준 설명(high-level account)과 연결하는 것은 수십 년 동안 프로그래밍 언어 연구의 핵심 관심사였습니다. 형식적으로 검증된 컴파일러(formally verified compilers)부터 번역 검증기(translation validators), 인증 컴파일러(certifying compilers), 그리고 증명 탑재 코드(proof-carrying code)에 이르기까지, 각 접근 방식은 노동 집약적이지만 근본적인 기계적 증명(mechanized proofs)과, 완전성(completeness), 일반성(generality), 그리고 증가된 신뢰 기반(trusted base)을 대가로 자동화를 선택하는 것 사이에서 결정해 왔습니다. 최근 대규모 언어 모델(Large Language Models, LLMs)은 형식 검증(formal verification)의 경제성을 변화시키기 시작했습니다. 에이전트 기반의 증명 개발(Agentic proof development)은 이제 이전에는 도달할 수 없었던 규모와 속도로 기계가 확인하는 증명(machine-checked proofs)을 생성할 수 있습니다. 본 논문에서 우리는 실행 코드와 그 고수준 명세(high-level specification) 사이의 정제(refinement)에 대한 근본적이고 기계가 확인하는 증명을 사후적(post hoc)인 개별 아티팩트 인증서(per-artifact certificates)로서 생성하는 LLM의 능력을 평가합니다. 우리는 이를 Ethereum 블록체인 위에서 스마트 컨트랙트를 실행하는 저수준 가상 머신인 Ethereum Virtual Machine (EVM)의 맥락에서 연구합니다. 우리는 Lean으로 구성된 근본적인 프레임워크인 EquiVM을 구축합니다. EquiVM은 실행 가능한 EVM 의미론(semantics)과 스마트 컨트랙트의 의도된 동작을 특징짓는 명세 언어(specification language)로 구성되지만, 특정 소스 언어나 컴파일 툴체인(compilation toolchain)에 종속되지 않습니다. EquiVM에서 정제(refinement)는 임의의 출처를 가진 배포된 바이트코드(deployed bytecode)에 대해 기술되며, 알 수 없는 코드와의 상호작용은 의미론의 일부이며, 각 증명은 재현 가능한 기계 확인 인증서입니다. 이전의 어떤 기술도 이러한 조합을 달성하지 못했습니다. 최첨단 상용 LLM을 사용하여, MakerDAO 스테이블코인 시스템의 대부분을 포함하여 23개의 실제 컨트랙트가 최소한의 인간 가이드로 엔드 투 엔드(end to end) 증명되었습니다. 이 과정에서 컨트랙트당 최대 1억 개의 토큰과 100시간의 증명 시간이 소요되었습니다. 우리는 이제 근본적인 기계적 증명을 토큰 비용으로 구매할 수 있으며, 이러한 변화가 검증 프레임워크가 설계되는 방식을 재편할 수 있다고 결론짓습니다.