The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and pro

The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc. It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.