These probabilistic guessing machines are pretty great for creating these formal models, e.g. TLA+, and then guessing if the implementation aligns with the spec.. In fact, it's my go-to tool for constructing soft guardrails for the model, so the design it's going to implement is logically sound. Same as for people: it's easier to make something working when you have a spec that is working.

Of course, it still allows the risk that you don't actually get to understand it.