# Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages

arXiv: https://arxiv.org/abs/2406.09757 · HTML: https://mlsanity.com/paper/2406.09757/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 23 references that are in the map.
- First posted on arXiv 14 Jun 2024.

## Builds on (most cited first, 8 of 8)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [TOGA: A Neural Method for Test Oracle Generation](https://mlsanity.com/paper/2109.09262/) (2021)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Verified Low-Level Programming Embedded in F*](https://mlsanity.com/paper/1703.00053/) (2017)

## Built on by (most cited first, 16 of 16)

- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning](https://mlsanity.com/paper/2604.11556/) (2026)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [Assured Automatic Programming via Large Language Models](https://mlsanity.com/paper/2410.18494/) (2024)
- [Perish or Flourish? A Holistic Evaluation of Large Language Models for Code Generation in Functional Programming](https://mlsanity.com/paper/2601.02060/) (2026)
- [VeriBound: PAC-Bayesian Generalization Bounds for Process Reward Models Trained with Formal Verification Tools](https://mlsanity.com/paper/2606.20740/) (2026)
- [Code-Augur: Agentic Vulnerability Detection via Specification Inference](https://mlsanity.com/paper/2606.18619/) (2026)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)
- [Ceci n'est pas une pipe: AI systems as semantic abstractions](https://mlsanity.com/paper/2607.09489/) (2026)
- [Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler](https://mlsanity.com/paper/2609.23954/) (2026)

## Abstract (arXiv)

Verification-aware programming languages such as Dafny and F* provide means to formally specify and prove properties of a program. Although the problem of checking an implementation against a specification can be defined mechanically, there is no algorithmic way of ensuring the correctness of the it user-intent formalization for programs, expressed as a formal specification. This is because intent or requirement is expressed it informally in natural language and the specification is a formal artefact. Despite, the advent of large language models (LLMs) has made tremendous strides bridging the gap between informal intent and formal program implementations recently, driven in large parts by benchmarks and automated metrics for evaluation. Recent work has proposed a framework for evaluating the it user-intent formalization problem for mainstream programming languages~citeendres-fse24. However, such an approach does not readily extend to verification-aware languages that support rich specifications (using quantifiers and ghost variables) that cannot be evaluated through dynamic execution. Previous work also required generating program mutants using LLMs to create the benchmark. We advocate an alternate, perhaps simpler approach of it symbolically testing specifications to provide an intuitive metric for evaluating the quality of specifications for verification-aware languages. We demonstrate that our automated metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark, yet demonstrates cases where the human labeling is not perfect. We also outline formal verification challenges that need to be addressed to apply the technique more widely. We believe our work provides a stepping stone to enable the establishment of a benchmark and research agenda for the problem of user-intent formalization for programs.