Yes, it's probably the most important trick in formal methods. Often surprisingly difficult to make it actually work, but when it does you can end up with a powerful tool.

In a past life I spent a lot of time on that sort of thing for control systems and RL. Spec says what not to do, reward says what to do, implementation can be arbitrarily complex wrt the spec.

There are many opportunities for an analogous move in LLM-assisted software engineering.