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

Cryptographic Primitive Code Generation by Fiat

Cryptol: The Language of Cryptography

Language for high-assurance and high-speed cryptography

APALACHE: symbolic model checker for TLA+ and Quint

A Proof-oriented Programming Language