Some spec based systems allow you to refine a high-level spec until it’s detailed enough to generate code from, where each refinement can be proved correct [1].

Some spec based systems allow you to refine a high-level spec until it’s detailed enough to generate code from, where each refinement can be proved correct [1]. I doubt this is done much, but it is possible. [1] eg https://en.m.wikipedia.org/wiki/B-Method https://en.m.wikipedia.org/wiki/B-Method