# Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 10 of its 25 references that are in the map.
- First posted on arXiv 17 Mar 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

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

- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [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)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers](https://mlsanity.com/paper/2404.10362/) (2024)

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

- [Skill Drift Is Contract Violation: Proactive Maintenance for LLM Agent Skill Libraries](https://mlsanity.com/paper/2605.10990/) (2026)
- [Agentic Proving for Program Verification](https://mlsanity.com/paper/2605.23772/) (2026)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing](https://mlsanity.com/paper/2607.09072/) (2026)
- [Ceci n'est pas une pipe: AI systems as semantic abstractions](https://mlsanity.com/paper/2607.09489/) (2026)
- [Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning](https://mlsanity.com/paper/2608.21516/) (2026)
- [Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change](https://mlsanity.com/paper/2609.16302/) (2026)
- [SpecGuard: Proving a Task Is Broken Before the Agent Cheats](https://mlsanity.com/paper/2610.09159/) (2026)

## Abstract (arXiv)

Agentic AI systems can now generate code with remarkable fluency, but a fundamental question remains: does the generated code actually do what the user intended? The gap between informal natural language requirements and precise program behavior -- the intent gap -- has always plagued software engineering, but AI-generated code amplifies it to an unprecedented scale. This article argues that intent formalization -- the translation of informal user intent into a set of checkable formal specifications -- is the key challenge that will determine whether AI makes software more reliable or merely more abundant. Intent formalization offers a tradeoff spectrum suitable to the reliability needs of different contexts: from lightweight tests that disambiguate likely misinterpretations, through full functional specifications for formal verification, to domain-specific languages from which correct code is synthesized automatically. The central bottleneck is validating specifications: since there is no oracle for specification correctness other than the user, we need semi-automated metrics that can assess specification quality with or without code, through lightweight user interaction and proxy artifacts such as tests. We survey early research that demonstrates the potential of this approach: interactive test-driven formalization that improves program correctness, AI-generated postconditions that catch real-world bugs missed by prior methods, and end-to-end verified pipelines that produce provably correct code from informal specifications. We outline the open research challenges -- scaling beyond benchmarks, achieving compositionality over changes, metrics for validating specifications, handling rich logics, designing human-AI specification interactions -- that define a research agenda spanning AI, programming languages, formal methods, and human-computer interaction.