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].