> The P521 curve implementation has been rewritten using code generated by the fiat-crypto project, which is based on a formally-verified model of the arithmeti

> The P521 curve implementation has been rewritten using code generated by the fiat-crypto project, which is based on a formally-verified model of the arithmetic operations. It is now constant-time and three times faster on amd64 and arm64. The observable behavior has not otherwise changed. This is exciting to see formally-verified Coq code being pulled into Go. https://github.com/mit-plv/fiat-crypto https://github.com/mit-plv/fiat-crypto