I would imagine it is 'optimised for verification' rather than for speed, ie. the code will be written to follow the structure of the specification. However, t

I would imagine it is 'optimised for verification' rather than for speed, ie. the code will be written to follow the structure of the specification. However, the nice thing about having a verified implementation is that it can be used as the specification (reference implementation) for any other optimisations you want to make. Such a two-step process is usually much more tractable than trying to verify optimised code directly. This is used extensively by BedRock ( http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ ) which uses functional programs as specifications and an assembly-like language for the "real"/optimised implementation. The resulting verification problems are straightforward enough to be mostly automated.