Some projects make it possible for you to generate verified code from the specification.

There is usefulness to these tools even if the implementation is a separate beast. At a minimum, they allow you to test drive your ideas in particularly thorny areas such as concurrency and security. Forcing you to think hard about a secure kernel or a library of data structures is a good thing in and of itself. You only have to give such core libraries this kind of anal attention, not to the layers built atop.

I'm guessing it's the same way you ensure that your code implements a specification written in English.

But at least you know the specification is consistent.

Some model checkers like CBMC annotate C code directly. Others can generate piles of tests. But usually just knowing your requirements are consistent and exactly how the algorithm has to behave to work as intended goes a long way!

If you have a specification that resembles your implementation well enough (which is not naturally the case, as keeping specifications on a higher level is almost always better, but can be done), you can use Model-Based Testing (MBT) techniques to increase confidence that your implementation matches the specification.

For example, you can ask Quint to generate a bunch of traces (executions) for you in JSON and then parse those to run tests in the implementation. If your trace is [{action: deposit(10), result: ok}, {action: withdraw(20), result: Error}], you can have an sort of integration test for your implementation that asserts that calling deposit(10) should result in ok and then calling withdraw(20) subsequently should result in an error.

There is one example for this as a Rust test: https://github.com/informalsystems/quint-sandbox/blob/main/S...

In addition to what everybody else is saying about the value of having a spec at all, there's a lot of exciting developments now in using a spec to generate a test suite, which is way simpler than using a spec to generate production code. Example: https://arxiv.org/abs/2006.00915