.md File is not a specification: Using formal analysis to find requirements gaps

Ok, so the proposed answer here is to define the spec in what is essentially code for another LLM to then interpret into different code?

I'm not sure if this does much more than a grillme skill and then poking an agent to do the work.

Today, most coding agents support spec-driven development (or plan mode).

They typically capture the requirements, design, and implementation plan in Markdown files. But is that Markdown file actually a specification?

This article explores how formal analysis can uncover requirements gaps that are easy to miss.