I wrote this prompt/skill because of this LLM failure mode: when you ask an LLM to "write tests," it inevitably spits out feature-shaped, data-flow, happy-path assertions. It writes examples, not properties.
The solution is like this: prompt in a way that forces a formal decomposition workflow that activates more of the formal verification part of LLM "Brain".