본 논문에서는 Move bytecode에 대한 최약 전제 조건 (Weakest-Precondition, WP) 분석과 Claude Code와 같은 에이전트 기반 코딩 CLI를 결합한 Move Prover용 명세 추론 (Specification Inference) 도구에 관한 초기 연구를 설명합니다. 명세 추론은 Move에서 명세를 작성할 때 발생하는 반복적인 작업 (Boilerplate)을 줄여줍니다. 전역 상태 불변량 (Global State Invariant)과 같은 고수준 속성을 검증하기 위해서는 일반적으로 지원 함수들에 대한 전제 조건 (Pre-condition) 및 사후 조건 (Post-condition)을 수동으로 작성해야 하는데, 이는 매우 지루한 작업입니다. 본 연구의 설정에서는 모델 컨텍스트 프로토콜 (Model Context Protocol, MCP) 서비스가 WP 분석과 프로버 (Prover) 자체를 코딩 에이전트에게 노출합니다. WP 분석은 추론을 위한 건전하고 기계적인 기준점 (Baseline)을 제공하며, AI는 WP가 가장 취약한 부분, 즉 루프 불변량 (Loop Invariants) 및 단조성 (Monotonicity), 보존 (Conservation), 구조적 불변량 (Structural Invariants)과 같은 고수준의 관용적 명세 (Idiomatic Specifications)를 작성하는 데 사용됩니다. Move Prover는 생성된 명세가 유효한지 결정하는 오라클 (Oracle) 역할을 수행하며, 에이전트는 검증이 성공할 때까지 증명 힌트 (Proof Hints)를 생성하고 추론된 명세를 개선할 수 있는 능력을 갖추고 있습니다. 이 도구는 고차 함수 (Higher-order Functions), 동적 디스패치 (Dynamic Dispatch), 전역 상태 (Global State), 참조 (References) 및 다양한 형태의 루프를 사용하는 코드를 포함하여, 표준적인 Move 코드 코퍼스 (Corpus)에 적용되었습니다.