Semiconductor Engineering published a careful read on LLM-generated formal properties this week, and the finding most coverage will bury is the useful one: the binding constraint is not the LLM, it is the specification. Most hardware specs are written for human engineers, not for machines attempting to derive verifiable assertions from them. LLMs can generate more properties than a human team would write manually, but that gap inverts: the human cost of assessing whether those properties are complete and correct can exceed the cost of writing them from scratch.
The verification bottleneck is moving upstream. Formal property generation is maturing faster than formal property validation. The missing layer is machine-readable specification formats that constrain what a model can derive, so that completeness can be checked mechanically rather than by a senior verification engineer reading assertions one at a time. Until that layer exists, LLM-to-formal pipelines are a volume play, not a correctness play.
Teams that invest now in structured, machine-checkable spec formats will extract the most value from LLM-assisted formal flows. Teams that hand models their existing PDFs and Word documents will get more properties, more quickly, with no reliable way to know which ones matter. The EDA tools will keep improving. The specifications will not improve on their own.