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.
- π 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
Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.