arXiv preprint ·
Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification
- Published
- Source
- arXiv preprint, posted before peer review
- DOI
- 10.4204/EPTCS.452.8
- Original
- Read it at arXiv
- Topics
Abstract
LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)ânotoriously difficult to formalise for verificationâit becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Artificial Intelligence
Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization
DatalogBench: Evaluating Large Language Models on Text-to-Datalog Synthesis
Faultless: A Program Equivalence Technique for Validating and Evaluating Neural Decompilers
From Verification Failures to Reusable Guidance for Coding Agents
Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements
Get the few papers worth your time in Artificial Intelligence every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.