Intent Formalization: Assessing the Quality of AI-Generated Formal Program Specifications (Keynote)

Agentic AI systems can now produce fluent code, but the core question persists: does the code reflect the user's actual intent? The long-standing gap between informal natural-language requirements and precise program behavior—the intent gap—is magnified by AI-generated code. The path to reliability runs through intent formalization: automatically translating informal intent into checkable specifications, ranging from lightweight tests to symbolic specs and domain-specific languages. As AI systems become creative at generating such specifications, the bottleneck shifts from writing specs to evaluating them. Since specifications lack an independent oracle, verifying that they truly capture user intent is difficult and user-dependent. We will discuss how this evaluation can be rigorous and largely automated. Using tests as a proxy oracle, we define metrics—soundness, completeness, and preciseness—to quantify how well a specification matches intent across both mainstream and verification-aware languages. Research prototypes demonstrate feasibility: tests to resolve intent ambiguities (TiCoder), quality assessment of symbolic specs (nl2postcond, Dafny spec validation), training a formal specification model (AutoVerus), and automated specification repair via agentic proof automation (F*). This work defines a research agenda spanning AI, programming languages, formal methods, and HCI.