← All repos

hacspec

Please see https://github.com/hacspec/hax

GitHubhacspec.org
cryptographyformal-verificationspecifications
Browse cluster: Lean4 Formal Verification & Cryptography →
1,416commits
32contributors
10languages

Tech stack & purpose

Hacspec is a specification language for cryptographic primitives written in Rust. The project provides a compiler and typechecker that validates Rust code against the hacspec language subset, along with code generation backends that translate specifications to F*, EasyCrypt, and Coq. Built on Rust nightly with dependencies on the Rust compiler infrastructure, the project includes a standard library (hacspec-lib), a cryptography provider implementing the RustCrypto API, and formal verification support through Coq libraries using CompCert and CoqPrime for arithmetic operations. Development on this repository has largely concluded in favor of the successor project hax.

Community & reference links

Languages

Coq
57.6%
Rust
35.7%
F*
3.6%
TeX
1.2%
Makefile
0.8%
eC
0.7%
Python
0.3%
Dockerfile
0.0%
Shell
0.0%
RPC
0.0%

Contributors (top 30 of 32)