There are ways to partially improve or at least quantify the specification gap using LLMs, by analyzing variance in the output formal specification when given a

There are ways to partially improve or at least quantify the specification gap using LLMs, by analyzing variance in the output formal specification when given a natural language specification (by eg. generating many formal specs from an input description). See eg. "Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning" [1]. [1]: https://arxiv.org/abs/2603.17233 https://arxiv.org/abs/2603.17233