Looks neat. We need more simple and verifiably correct cryptographic primitive frameworks that people can build upon to help secure the world. It'll take another 10-15 years before industry catches up.
The DSL allowed me to find a (trivial) error in the SHA-1 spec -- the description says 0 <= t < 79, but below they allow for 0 <= t <= 79 (which is also the cryptol implementation).
Nice catch! We noticed that error as well but didn't want to poke the NIST folks in the eye on the web page -- we're hoping to win them over with Cryptol, not put them on the defense. We're planning to submit an errata report on their website next week.
The DSL allowed me to find a (trivial) error in the SHA-1 spec -- the description says 0 <= t < 79, but below they allow for 0 <= t <= 79 (which is also the cryptol implementation).