[runeks]

Thanks for the response!

> The main contribution here is that only the data structures (which are reusable) need to be proven by hand; for a new NF, you only need a specification - which is, as you point out, not always easy to do.

I guess my main point is that not only is it not easy to do, but writing the spec is also an error-prone process (just like writing the implementation), and errors in the spec cannot be caught by any machinery.

Not to say that this makes the process meaningless — not at all — but simply to say that “formally verified” doesn’t mean “bug-free”, it means going from the challenge being writing a correct implementation to writing a correct specification.