hacspec is the functional subset of Rust that can be used, together with a hacspec standard library, to write succinct, executable, and verifiable specifications in Rust. These specifications can be translated into formal languages with hax.
There is a wealth of specifications of cryptographic algorithms and protocols to get you started.
Publications & Other material
Secondary literature, using hacspec:
- 📕 Last yard
- 📕 A Verified Pipeline from a Specification Language to Optimized, Safe Rust at CoqPL'22
- 📕 Hax - Enabling High Assurance Cryptographic Software at RustVerify24
- 📕 A formal security analysis of Blockchain voting at CoqPL'24
- 📕 Specifying Smart Contract with Hax and ConCert at CoqPL'24
Contributing
Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.