Currently, the IETF standardizes cryptographic primitives using pseudo-code. The correctness of an implementation of such a standard is safe-guarded by unit tests and reference implementations. Hacspec improves on this by replacing pseudo-code by a subset of rust with a precise operational semantics. Similarly, the Fiat Cryptogrphy library allows one to synthesize efficient correct-by-construction implementations. We contribute a Coq-backend for hacspec and connect the two projects using bedrock2, as well as a printer from the bedrock’s C-like language to Rust. Thus we provide a pipeline from hacspec to optimized, safe Rust. As a feasibility study, we apply the pipeline to the BLS elliptic curve, used for signatures.