Combining Mechanical and Agentic Specification Inference for Move

• URL: http://arxiv.org/abs/2605.10005v2
• Date: Wed, 13 May 2026 02:35:58 GMT
• Title: Combining Mechanical and Agentic Specification Inference for Move
• Abstract summary: We describe a specification inference tool for the Move Prover.<n>It combines a weakest-precondition analysis over Move bytecode with an agentic coding CLI such as Claude Code.<n>The tool has been applied to a corpus of canonical Move code.
• Score: 2.8693521708495684
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic coding CLI such as Claude Code. Specification inference reduces the boilerplate of writing specifications in Move: in order to verify a high-level property such as a global state invariant, pre- and post-conditions for the supporting functions typically have to be written by hand, which is tedious. In our setting, a Model Context Protocol (MCP) service exposes the WP analysis and the prover itself to the coding agent. The WP analysis provides a sound, mechanical baseline for inference; the AI is used precisely where WP is weakest -- for loop invariants and high-level idiomatic specifications such as monotonicity, conservation, and structural invariants. The Move Prover serves as the oracle that decides whether the generated specs are valid, and the agent is equipped to generate proof hints and to refine the inferred specification until verification succeeds. The tool has been applied to a corpus of canonical Move code, including code that uses higher-order functions, dynamic dispatch, global state, references, and various forms of loops.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
  We propose specification-grounded alignment, a new alignment paradigm that treats provider-authored model specifications as the primary alignment target.<n>We introduce SpecAlign, a framework that synthesizes alignment data directly from specification documents.
  arXiv  Detail & Related papers  (2026-06-15T06:30:52Z)
• Agentic Separation Logic Specification Synthesis [4.177196802192322]
  Spec-Agent is an agentic system for synthesizing expressive, well-validated specifications across large C++s.<n>For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language.<n>We evaluate Spec-Agent on open source C++s comprising millions of lines of code.
  arXiv  Detail & Related papers  (2026-05-26T18:05:42Z)
• Agentic Model Checking [12.832868209928039]
  We propose a paradigm that couples LLM agents with a bounded model checking backend.<n>We instantiate the approach in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in C and Rust.
  arXiv  Detail & Related papers  (2026-05-20T17:25:52Z)
• DocSync: Agentic Documentation Maintenance via Critic-Guided Reflexion [0.0]
  DocSync is an agentic workflow that frames documentation maintenance as a structurally grounded, iterative generation task.<n>We empirically evaluate a resource-constrained implementation of DocSync-using a LoRA-adapted small language model.<n>Our findings demonstrate that this AST-aware agentic approach substantially outperforms standard encoder-decoder baselines.
  arXiv  Detail & Related papers  (2026-05-04T02:41:33Z)
• VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
  We compare classical and prompt-based approaches for automated JML specification synthesis.<n>We investigate whether prompt optimization can push synthesis quality further by evolving prompts through structured verification feedback.<n>We propose VeriAct, a verification-guided agentic framework that iteratively synthesizes and repairs specifications.
  arXiv  Detail & Related papers  (2026-03-31T22:12:15Z)
• FMBench: Adaptive Large Language Model Output Formatting [49.52930069696333]
  We present FMBench, a benchmark for adaptive Markdown output formatting.<n>Experiments on two model families show that SFT consistently improves semantic alignment.<n>Results also reveal an inherent trade-off between semantic and structural objectives.
  arXiv  Detail & Related papers  (2026-02-06T04:42:06Z)
• AgenticTagger: Structured Item Representation for Recommendation with LLM Agents [58.12004213978182]
  AgenticTagger is a framework that queries LLMs for representing items with sequences of text descriptors.<n>To effectively and efficiently ground vocabulary in the item corpus of interest, we design a multi-agent reflection mechanism.<n>Experiments on public and private data show AgenticTagger brings consistent improvements across diverse recommendation scenarios.
  arXiv  Detail & Related papers  (2026-02-05T18:01:37Z)
• Finding the Translation Switch: Discovering and Exploiting the Task-Initiation Features in LLMs [69.28193153685893]
  Large Language Models (LLMs) frequently exhibit strong translation abilities, even without task-specific fine-tuning.<n>To demystify this process, we leverage Sparse Autoencoders (SAEs) and introduce a novel framework for identifying task-specific features.<n>Our work not only decodes a core component of the translation mechanism in LLMs but also provides a blueprint for using internal model mechanism to create more robust and efficient models.
  arXiv  Detail & Related papers  (2026-01-16T06:29:07Z)
• SeqPE: Transformer with Sequential Position Encoding [76.22159277300891]
  SeqPE represents each $n$-dimensional position index as a symbolic sequence and employs a lightweight sequential position encoder to learn their embeddings.<n> Experiments across language modeling, long-context question answering, and 2D image classification demonstrate that SeqPE not only surpasses strong baselines in perplexity, exact match (EM) and accuracy--but also enables seamless generalization to multi-dimensional inputs without requiring manual architectural redesign.
  arXiv  Detail & Related papers  (2025-06-16T09:16:40Z)
• AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL [6.062811197376495]
  We propose a novel approach that constructs a Knowledge Graph (KG) from both specifications and RTL.<n>We create an initial KG from the specification and then systematically fuse it with information extracted from the RTL code, resulting in a unified, comprehensive KG.<n> Experiments on four designs demonstrate that our method significantly enhances SVA quality over prior methods.
  arXiv  Detail & Related papers  (2025-03-24T21:53:37Z)
• Discourse Features Enhance Detection of Document-Level Machine-Generated Content [53.41994768824785]
  Machine-generated content poses challenges such as academic plagiarism and the spread of misinformation.<n>Existing MGC detectors often focus solely on surface-level information, overlooking implicit and structural features.<n>We introduce novel methodologies and datasets to overcome these challenges.
  arXiv  Detail & Related papers  (2024-12-17T08:47:41Z)
• Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
  We use TLA+ to model fine-grained behaviors of ZooKeeper and the TLC model checker to verify its correctness properties. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space.
  arXiv  Detail & Related papers  (2024-09-22T02:59:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.