This case study addresses a long-standing gap between the acknowledged benefits of formal software specification — early detection of design flaws, explicit assumptions, built-in invariants — and its limited industrial adoption, which the authors attribute to the overhead of writing and maintaining formal specifications and to the expertise that traditional specification languages demand. Their proposal is an intermediate representation sitting between informal natural-language requirements and fully formal languages: natural language enriched with lightweight mathematical notation and written in LaTeX, precise enough to support assertions that can be reasoned about and proved at the specification level, yet readable without deep formal-methods training.
The study compares two ways of developing the same program from a natural-language specification. In the first, the simulation is corrected iteratively from its execution results; in the second, AI reviews and refines the specification before any code is generated or run. The authors report that the second approach took roughly a sixth of the time the first did and produced a correct simulation on the first code-generation attempt. The case study is a simulation of knowledge growth within an organization, chosen as a domain rich enough to require nontrivial structure, invariants and parameterization while remaining interpretable; the specification is elaborated across several rounds in which the authors ask the model to identify ambiguities and inconsistencies, supply clarifications, and regenerate the specification before requesting an implementation.
A closing experiment runs the process in reverse to study what ambiguity costs. Starting from the refined, math-rich specification, the authors have the model restate it in plain language with no mathematical symbols, then condense that into three paragraphs, then — in a fresh context — asked it to reconstruct a rigorous specification from the condensed version. The reconstruction lost material: the authors report that the notion of organizations almost disappeared, that the graph structure contained mistakes such as a confusion between directed and undirected edges and in the definition of a clique, that the association of the facilitator to an organization went untouched, that the order of events was wrong because a clique was chosen before the temporary edges were introduced, that the facilitator’s budget was missing so that it appeared unbounded, and that the specificity of the scenarios was lost.
Key Points
- Proposes natural language augmented with lightweight mathematical notation, written in LaTeX, as an intermediate specification language, arguing it retains benefits of formal specification — early validation, explicit invariants, correctness by design — while reducing the notation overhead of heavyweight formal methods.
- Reports that reviewing and refining the specification with AI before generating any code took about a sixth of the time of iteratively correcting the implementation from its execution results, and produced a correct simulation on the first generation attempt. This rests on one case study by the authors, not a controlled comparison across projects or teams.
- Argues for an explicit distinction between the aspects a system analyst wants to control and those that need not be controlled: the authors hold that peripheral elements such as a GUI can be modified or expanded by the model without consulting the analyst, while anything pertaining to business logic should be returned to the analyst for refinement or confirmation, especially where the intention is ambiguous.
- Reports a division of labour on invariants: the human designer supplied high-level invariants while the model proposed lower-level ones that the authors judged correct and useful. The authors also note that the correctness invariant they had defined themselves was not among those the model suggested, and that some model-suggested invariants were stated in prose with no associated logical formula.
- Reports an attention limitation: as the specification grew beyond a few pages, the model occasionally omitted parts of it during generation, which the authors read as an argument for abstraction, modularization and decomposition when working with longer specifications.
- Reports that the model proposed extensions that had not been requested — Monte Carlo simulation to make the results statistically stable is the example given — which the authors accepted on the condition that they could be validated at the specification level.
- Reports that summarizing a precise specification into loose prose reintroduces ambiguity in ways that change the generated program, and presents this as evidence for what the authors call the primacy of precision: a first human-written description of business logic is typically imprecise, and the blurry line it leaves gives the model room to be creative in more of the program than was intended.
Notes
The authors position the work relative to spec-driven development, on which they say they build by using natural language augmented with mathematical notation as an intermediate representation, and relative to formal specification languages, against which they trade some rigor for readability and ease of use. In the ambiguity experiment they describe permitting the model to work in the manner of spec-driven development — formalizing the problem in intermediate files before implementing — and report that this gave transparency into the decisions the model took about elements surrounding the business logic. See Spec-driven development for the practice itself.
The authors state limitations of their own. The simulation used as the case study, while logically complex, is a small piece of software, and they encountered challenges of attention limits, specification decomposition and iterative refinement during development. The generated code was not manually reviewed at any point, the authors judging specification-level reasoning and invariant checking sufficient; the resulting programs are Python, distributed as linked notebooks. They also report that getting the model to state experimental conclusions explicitly required repeated prompting, which they suggest is an area for further refinement of agentic workflows.