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

요약

본 연구는 Move bytecode에 대한 최약 전제 조건(WP) 분석과 Claude Code와 같은 에이전트 기반 코딩 CLI를 결합하여 Move Prover용 명세 추론 도구를 제안합니다. WP 분석을 기계적 기준점으로 삼아 AI가 루프 불변량이나 구조적 불변량 같은 고수준 명세를 자동으로 작성하며, Move Prover는 생성된 명세의 유효성을 검증하는 오라클 역할을 수행합니다.

핵심 포인트

• WP(Weakest-Precondition) 분석을 통해 AI 추론을 위한 건전하고 기계적인 기준점 제공
• Model Context Protocol(MCP)을 활용하여 WP 분석 및 Prover 기능을 코딩 에이전트에 노출
• AI가 루프 불변량, 단조성, 보존성 등 고수준의 관용적 명세를 작성하여 반복 작업 감소
• Move Prover를 오라클로 사용하여 에이전트가 검증 성공 시까지 명세를 반복 개선하는 루프 구축
• 고차 함수, 동적 디스패치, 전역 상태 등 복잡한 Move 코드 코퍼스에 대한 적용 가능성 확인