Source-linked AI summary
Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
Shuvendu K. Lahiri
TL;DR
AI-generated code can look correct while deviating from user intent, making the intent gap a central reliability problem. The paper frames intent formalization as translating intent into checkable specifications across a spectrum, surveys evidence of its promise, and identifies specification validation and real-world scaling as major challenges.
Problem
The central problem is determining whether fluent AI-generated code actually matches user intent despite the persistent and AI-amplified intent gap.
Method
The paper defines intent formalization, surveys its spectrum from tests through full specifications and DSLs, and synthesizes early research and open challenges.
Results
Early research shows that interactive formalization improves developer correctness, automated specification metrics can reach expert-level quality, and end-to-end pipelines produce verified code.
Takeaways & Limitations
Intent formalization is presented as a promising direction for making AI-generated software explicit, checkable, and enforceable.
Takeaways & Limitations
Current results largely target self-contained algorithmic functions, leaving real-world side effects, mutable state, concurrency, and complex dependencies insufficiently addressed.
Abstract
from arXiv · showhide
Agentic AI systems can now generate code with remarkable fluency, but a fundamental question remains: \emph{does the generated code actually do what the user intended?} The gap between informal natural language requirements and precise program behavior -- the \emph{intent gap} -- has always plagued software engineering, but AI-generated code amplifies it to an unprecedented scale. This article argues that \textbf{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 \emph{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 \emph{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.
1 Introduction
Agentic coding intensifies the intent gap by producing plausible code at a scale that outpaces scrutiny, while silently preserving ambiguity in user requests. The article presents formal specifications as an intermediate layer ranging from tests to verified synthesis.
- Why Now?: Agentic coding tools now synthesize entire features autonomously, shifting developers from authors toward supervisors or passive consumers.This reduces direct human inspection of generated code.
- The Intent Gap: Ambiguous requests can yield plausible but divergent behavior, as “remove duplicates” may mean retaining one copy or eliminating every repeated element.The example shows why statistical pattern matching cannot reliably ground behavior in a user’s specific intent.
- The Intent Gap: The intent gap is the semantic distance between what users mean and what programs do, and AI amplifies it through scale without scrutiny.Generated code can exceed humans’ review capacity while traditional safeguards fail to keep pace.
- Intent Formalization: Formal specifications insert an intermediate “what” layer between informal intent and operational code, enabling enforcement through testing and verification.The article frames this as the central route toward reliable AI-generated software.
- Intent Formalization: Intent formalization spans lightweight tests, full functional specifications, and domain-specific languages that can synthesize provably correct code.These levels trade specification effort against correctness coverage and reliability needs.
- Research Agenda: The article surveys intent formalization as a research framework, connecting emerging AI coding workflows with verification infrastructure and an open research agenda.The motivating agenda includes bypassed human review, expanded deployment scale, and mature verification technology.
2 What Is Intent Formalization?
Intent formalization translates informal user intent into formal, checkable specifications across a spectrum of increasing expressiveness. These specifications support complementary verification approaches, while specification absence and validation remain central bottlenecks.
- What Is Intent Formalization?: Intent formalization automatically translates informal user intent into a set of formal, checkable program specifications.The resulting specifications span increasing levels of expressiveness.
- Specification Spectrum: Tests encode concrete input/output expectations, while code contracts express executable assertions, postconditions, and invariants.Both can apply across mainstream programming languages.
- Specification Spectrum: Logical contracts use richer constructs and program verifiers to check specifications statically for all possible inputs.Dafny, F*, and Verus exemplify verification-aware languages in this part of the spectrum.
- Specification Spectrum: Domain-specific languages provide complete formal specifications from which correct code is synthesized automatically through verified compilation.They occupy the far end of the expressiveness spectrum.
- Complementarity: The spectrum is complementary: tests can validate postconditions, postconditions can guide invariant discovery, and invariants can anchor full proofs.Progress at one level can therefore support progress at other levels.
- Related Distinctions: Intent formalization differs from autoformalization because it covers a cost-effective range from ambiguity-prone properties to complete DSL-based specifications.It is also distinct from informal spec-driven development because its outputs are mechanically checkable.
- Specifications vs. Verification: Specifications describe intended behavior, whereas verification checks whether code actually satisfies those specifications.Testing is lightweight but incomplete; runtime checks broaden coverage with overhead and trigger dependence.
- Specifications vs. Verification: The key bottleneck is the absence of formal specifications for verification, so teams can scale investment from targeted ambiguity checks to full functional specifications.Existing test runners, SMT solvers, and proof assistants can check specifications once they exist.
3 Early Research on Intent Formalization
Early research supports intent formalization across specification generation, specification validation, interactive clarification, and verified synthesis. The evidence spans benchmark studies and an end-to-end pipeline from informal prose to deployable verified code.
- 3 Early Research on Intent Formalization: Early studies organize intent-formalization evidence from individual specification capabilities through end-to-end systems.The surveyed evidence is primarily based on benchmark problems.
- 3 Early Research on Intent Formalization: A test oracle—the expected output for one input—is itself an instance of intent formalization.
- 3.1 LLMs Can Generate Meaningful Specifications: LLMs generate meaningful specifications: postconditions caught one in eight Defects4J bugs, while class invariants and module specifications extend coverage beyond individual functions.ClassInvGen outperformed direct prompting and Daikon, and VeriStruct verified nearly all functions across 11 data-structure modules.
- 3.2 Measuring Specification Quality: Specification validation remains fundamental because generated specifications have no independent ground truth beyond the user’s intent.Unlike code, specifications cannot be checked against a known oracle without addressing the user’s intended behavior.
- 3.2 Measuring Specification Quality: Soundness and completeness metrics evaluate specifications against tests, including rich logical contracts through symbolic techniques before implementation exists.Soundness checks valid behavior, while completeness measures rejection of incorrect or mutated outputs.
- 3.2 Measuring Specification Quality: Automated checks exposed an incomplete Dafny specification and found three mislabeled plus two inconsistent specifications missed by human labeling.The incomplete specification required replacing implication with bi-implication, and these metrics also supported Auto-Verus proof filtering.
- 3.3 Interactive Intent Formalization: TiCoder asks users to approve ambiguity-targeting tests, pruning candidate programs and roughly doubling correct evaluation in a study of 15 professional developers.The study also reported lower cognitive load, persistent regression tests, and majority participant preference for TiCoder.
- 3.4 End-to-End Verified Pipelines: 3DGen translates informal RFC prose into a 3D DSL, refines specifications with symbolic tests, and compiles them into provably correct parsers for 20 network protocol formats.The generated parsers are memory-safe C or Rust binaries produced through EverParse.
4 A Research Agenda
The research agenda targets seven challenges for making intent formalization useful beyond benchmark settings, including real-world systems, code changes, specification validation, rich logics, human interaction, and workflow integration.
- From benchmarks to real-world systems: Current results target self-contained algorithmic functions, leaving real-world systems with side effects, mutable state, concurrency, and complex dependencies underexplored.The agenda calls for benchmarks, metrics, and specification idioms for real-world intent formalization.
- Change intent and compositionality: Intent formalization must capture behavioral changes in existing code while composing with source code, tests, and specifications that define current behavior.This challenge also applies to code translation, such as migrating legacy C codebases to Rust.
- Identifying what to clarify cost-effectively: Specifications need metrics that rank expected bug-prevention value without exhaustively enumerating plausible implementations.TiCoder targets tests where diverse generated candidates disagree, but sampling candidate programs becomes expensive at scale.
- Automated metrics for spec validation: Specification validation requires complementary automated proxies, targeted user feedback, and cross-checking among code, docstrings, and formal annotations because users remain the only correctness oracle.Tests and mutation analysis provide automated signals, while human feedback resolves ambiguities that automation cannot settle.
- Rich logics and quantifiers: Rich verification logics remain difficult because LLMs struggle with quantifiers, recursive predicates, and ghost variables, while verifiers have limitations on complex concrete inputs.These limitations make automated soundness and completeness evaluation difficult.
- Human-AI interaction for specification: Approve/reject interaction improves benchmark correctness, but real-world specification needs explanations, calibrated confidence, and templates within an underexplored HCI space.The agenda therefore extends beyond simple approval loops toward richer human-AI specification interaction.
- Integration into developer workflows: Intent formalization should span issue creation, code review, and CI/CD so specifications remain connected to evolving requirements and agentic workflows.In vibe coding, specifications may become the primary interface between human intent and machine behavior.
5 Related Work
Intent formalization extends established specification mining and code-generation evaluation by shifting attention from observed behavior or generated-code correctness toward intended, checkable semantics.
- Specification mining: Classical specification mining infers invariants from execution traces, whereas LLM-based specification generation aims to reason about intended semantics beyond observed behavior.The distinction concerns whether specifications capture only executions or also user intent.
6 Conclusion
The paper argues that intent formalization is a promising route toward reliable AI-generated code, while emphasizing that major open challenges remain substantial research programs.
- Conclusion: Early research shows that LLMs can generate specifications across the formalism spectrum, evaluate specification quality, improve developer correctness interactively, and support verified code-generation pipelines.The paper also reports that specification quality enables proof automation.
- Conclusion: The central conclusion is that AI-generated code is already widespread, but reliable AI-generated code still requires making user intent explicit, checkable, and enforceable.The paper frames intent formalization as the mechanism connecting informal intent with formal verification.
- Conclusion: Scaling beyond benchmarks, formalizing changes, prioritizing clarifications, validating specifications, handling rich logics, designing human-AI interaction, and achieving compositionality remain substantial research programs.The paper calls for dedicated benchmarks, cross-disciplinary collaboration, and sustained investment.
- Conclusion: The paper concludes that closing the intent gap will determine whether AI makes software more reliable or merely more abundant.