I’ve read through the whole introduction PDF (without actually following the exercises, but I intend to go back and do it all now), and the whole system seems really nice. I’ve had a look at the Keccak/SHA-3 standard and it looks like implementing it in Cryptol with the same ability to parameterise the various sizes would be almost trivial. I think I’ll give it a go when I have some free time.
The build in ability to state properties and have them both quickly QuickChecked a la Haskell’s QuickCheck and also exhaustively proved using an SMT solver (I think that’s the right term?) is fantastic.
I highly recommend a read through of the book under their documentation. Makes me want to work for Galois even more; shame they don’t seem to want me.