기술 요약: Move 를 위한 기계적 및 에이전트 기반 명세 추론의 결합

문제 제기

Move Prover(MVP) 를 사용한 Move 스마트 계약의 형식적 검증은 실용적인 병목 현상에 직면해 있습니다: 수동으로 명세를 작성하는 데 드는 높은 비용입니다. 개발자들은 고수준 속성 (예: 전역 상태 불변성, 자금 보존, 조건부 중단) 을 검증하고자 하지만, 검증 과정은 모든 지원 함수에 대한 명시적인 저수준 전조건 및 후조건을 요구합니다. 이러한 명세를 작성하는 것은 기계적이고 지루하며, 종종 검증기 사용 비용을 지배하여 더 넓은 채택을 방해합니다. 비록 MVP 가 명시되지 않은 호출 함수를 검증하기 위해 함수 본문을 인라인할 수는 있지만, 이 접근 방식은 모듈식 검증을 위해 확장되지 않습니다.

방법론

이 논문은 Move 바이트코드에 대한 명세를 추론하기 위해 기계적 약조건 (Weakest-Precondition, WP) 분석과 에이전트 코딩(특히 Claude Code 를 통해) 을 결합한 새로운 도구를 제시합니다. 이 시스템은 Move Prover 가 기계적 및 AI 생성 신호 모두에 대한 오라클로 작용하는 협력적 워크플로우를 통해 운영됩니다.

1. 기계적 구성 요소: 약조건 (WP) 분석

기계적 기준선은 Move 바이트코드에 대해 수행된 표준 WP 분석에 의존합니다. 주요 기술적 특징은 다음과 같습니다:

• 참조 제거: 분석 전에 Move Prover 의 변환 파이프라인이 Rust 스타일의 참조 (&T, &mut T) 를 바이트코드를 참조 없는 중간 형태로 다시 작성함으로써 제거합니다. 공유 참조는 인라인되고, 가변 참조는 인/아웃 매개변수로 변환됩니다. 이를 통해 고전적인 디스트라 (Dijkstra) 스타일의 추론이 직접 적용될 수 있습니다.
• 명세 계측: 바이트코드는 기존 사용자 명세에서 파생된 assume 및 assert 문으로 계측됩니다. 호출은 추상화된 호출자 계약을 위해 행동 술어 (예: result_of, aborts_of) 를 사용하여 계측됩니다.
• 출력: WP 엔진은 기계적으로 중단 조건, modifies 절, 그리고 결과 스타일의 후조건을 유도합니다. 그러나 이는 일반적으로 루프 본체만으로는 유도할 수 없는 루프 불변식에 어려움을 겪습니다; 이러한 것이 없으면 추론된 명세가 공허한 (vacuous) 것이 됩니다.

2. 에이전트 구성 요소: AI 주도 추론

모델 컨텍스트 프로토콜 (MCP) 서비스를 통해 통합된 AI 코딩 에이전트 (Claude Code) 가 WP 엔진의 한계를 해결합니다:

• 루프 불변식: 에이전트는 패턴 인식을 사용하여 WP 엔진이 유도할 수 없는 귀납적 불변식 (예: 단조성, 합의의 보존, 정렬된 접두사) 을 제안합니다.
• 고수준 관용구: 에이전트는 인간 개발자에게 익숙한 관용구로 고수준 명세 (예: 단조성, 구조적 불변식) 를 생성합니다.
• 단순화: 에이전트는 WP 엔진이 생성한 verbose 하거나 의미상 정확하지만 종종 다루기 힘든 명세를 더 간결하고 가독성 있는 형태로 정제합니다.
• 증명 힌트: 검증이 시간 초과될 때 (예: 비선형 산술로 인해), 에이전트는 검증기를 안내하기 위해 보조 정리 (lemmas) 와 증명 힌트를 생성합니다.

3. 워크플로우

이 프로세스는 "기술 (skills, Markdown 지시사항)", 편집 시간 후크, 그리고 MCP 서버를 활용하는 Claude Code 플러그인으로 제공됩니다. 워크플로우는 고정된 작업 순서를 따릅니다:

1. 루프 불변식 합성: 에이전트가 불변식이 부족한 루프를 식별하고 이를 제안합니다.
2. 약조건 추론: 에이전트가 기계적 기준선 명세를 생성하기 위해 MCP 를 통해 MVP 를 호출합니다.
3. 단순화: 에이전트가 가독성과 간결성을 위해 결합된 명세를 다시 작성합니다.
4. 검증 및 정제: 전체 범위의 검증 실행이 수행됩니다. 논리적 오류가 발견되면 에이전트가 이를 수정합니다. 시간 초과가 발생하면 에이전트가 보조 정리나 증명 힌트를 도입합니다.
5. 반복: 검증기로부터의 반례가 에이전트로 피드백되어 정제됩니다. 사용자는 언제든지 개입할 수 있습니다.

주요 기여

논문은 세 가지 주요 기여를 식별합니다:

1. 하이브리드 추론 아키텍처: 저자들의 지식에 따르면, 이는 sound 한 기계적 기준선 (WP) 과 에이전트 구성 요소를 결합한 최초의 LLM 기반 명세 추론 시스템입니다. WP 엔진은 기계적 유도 (중단, 수정, 후조건) 를 처리하는 반면, AI 는 WP 의 "가장 약한" 부분 (루프 불변식 및 고수준 관용구) 을 처리합니다.
2. 상호작용형 코딩 에이전트 통합: 이전의 독립형 스크립트로 작동하던 추론 도구들과 달리, 이 시스템은 상호작용형 코딩 에이전트 (Claude Code) 에 플러그인으로 통합됩니다. 이는 사용자가 추론 과정을 모니터링하거나, 재정의하거나, 기여할 수 있는 협력적 루프를 가능하게 합니다.
3. WP 를 위한 참조 제거: 논문은 고전적 WP 분석을 가능하게 하기 위해 Move 바이트코드에 적용된 참조 제거 (이전에 Rust 용 Aeneas 에서 사용됨) 에 대해 상세히 설명합니다. 참조 없는 중간 형태와 WP 추론의 이러한 결합은 이전에 설명된 바가 없습니다.

결과 및 평가

이 도구는 다음과 같은 표준 Move 코드 코퍼스에 적용되었습니다:

• 고차 함수: 특히 술어를 사용하는 벡터 검색 함수.
• 산술: 비선형 산술 및 오버플로우 검사가 포함된 지수 함수.
• 상태 의존 알고리즘: 여러 주소에 걸쳐 전역 저장소를 수정하는 함수.

관찰:

• 하이브리드 접근 방식은 루프, 동적 디스패치, 전역 상태를 포함하는 복잡한 시나리오에 대한 명세를 성공적으로 생성했습니다.
• 지수 함수 예시에서 WP 엔진은 정확성 조건을 제공한 반면, 에이전트는 검증 시간 초과를 해결하기 위해 단조성 보조 정리를 성공적으로 도입했습니다.
• 에이전트는 WP 엔진 자체의 항 단순화 이후에도 WP 생성 명세를 더 간결한 형태로 자주 다시 작성했습니다.
• 시스템은 에이전트가 단순화 단계에서 이러한 조건을 폐기함으로써 "공허한" 조건을 처리합니다.

중요성 및 주장

이 논문은 이 작업을 초기 연구이자 예비 결과를 가진 도구 논문으로 규정합니다. 저자들은 중요성에 대해 겸손한 주장을 합니다:

• 상호 보완적 강점: 이 시스템은 보일러플레이트를 위한 기계적 추론의 신뢰성과 귀납적 추론을 위한 LLM 의 패턴 인식 능력을 활용합니다. WP 기준선은 에이전트가 완전히 잘못된 명세를 제안하는 것을 방지하는 반면, 에이전트는 WP 가 실패하는 부분을 채웁니다.
• 워크플로우 혁신: 기술과 MCP 를 통한 대화형 코딩 루프에 검증의 통합은 정적 분석 도구에서 동적 협력 워크플로우로의 전환을 나타냅니다.
• 미래 방향: 저자들은 "기술 (skills, 지시사항)"의 정의가 진화하는 영역임을 인정합니다. 그들은 확장성과 수동 작성 명세 대비 토큰 비용을 평가하기 위해 이 도구를 Aptos Framework 와 복잡한 영구 거래 엔진에 역으로 적용할 계획입니다. 그들은 하이브리드 접근 방식이 순수 LLM 추론과 비교하여 얼마나 효과적인지에 대한 체계적인 연구가 더 필요하다고 명시적으로 언급합니다.

이 논문은 이 방법론이 Move 에서 형식적 검증의 보일러플레이트 비용을 줄이는 실현 가능한 경로를 보여주며, AI, 기계적 추론, 인간 개발자 간의 협력을 가능하게 한다고 결론지었습니다.