My assumption would be that this formally verified implementation is not optimized, and therefore runs rather slowly compared to the C implementations. Plus it requires the .NET framework or Mono to run it. Am I off base?
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/ ) 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.
No, you're right on target. They are using non-optimized data structures, and rely on (Bouncy Castle's) managed code for encryption. From their paper, the throughput is around 10x slower than OpenSSL (but much closer to JSSE). My guess is that one could probably speed this up significantly, while still retaining the guarantees, but that's probably less interesting to these guys.
As for Mono or .NET, I assume so (AFAIK that's the only way to run F# applications).
