Comment by andrewchambers

Often the spec can be simpler than the original.

The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations.

The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.