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.