Cryptographic Primitive Code Generation by Fiat

A work-in-progress language and compiler for verified low-level programming

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

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance …

Bounds on divsteps iterations in safegcd

Crellvm: Verified Credible Compilation for LLVM

Provably optimal low-level programs in Coq