Introduction

hacspec is a specification language for crypto primitives, protocols, and more. It is a subset of the Rust programming language, focused on functional programming and it avoids the use of mutable state as much as possible.

This book gives an overview of:

• The hacspec language;
• The different parts of the project:
  • the standard library,
  • examples of hacspec programs;
• How to use hacspec to write specifications for standards and verification;
• How to use hacspec to generate test vectors;
• Work on the hacspec compiler and tooling itself.

For a quick introduction you can also check out these slides from April 2021. An in-depth technical report is also available, and serves as a reference for the language formalization.