Synthesizing Correct-by-Construction Code for Cryptographic Primitives

Here's the abstract from their paper:

    We introduce a new approach for implementing cryptographic
    arithmetic in short high-level code with machine checked proofs
    of functional correctness.  We further demonstrate that simple
    partial evaluation is sufficient to transform such initial code
    into the fastest-known C code, breaking the decades old pattern
    that the only fast implementations are those whose
    instruction-level steps were written out by hand.  These
    techniques were used to build an elliptic-curve library that
    achieves competitive performance for 80 prime fields and
    multiple CPU architectures, showing that implementation and
    proof effort scales with the number and complexity of
    conceptually different algorithms, not their use cases. As one
    outcome, we present the first verified high-performance
    implementation of P-256, the most widely used elliptic curve.
    Implementations from our library were included in BoringSSL to
    replace existing specialized code, for inclusion in several
    large deployments for Chrome, Android, and CloudFlare.

A list of projects using the code generated by fiat-crypto: https://github.com/mit-plv/fiat-crypto/issues/902