hacspec is a language and framework for writing succinct, executable, formally verifiable specifications for cryptographic components.
Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts. An application developer can use hacspec to specify and prototype cryptographic components in Rust, and then replace this specification with a verified implementation before deployment.
