I was aware of s2n-bignum which is a very cool project, but apparently there is a larger sister project, aws-lc, that aims for broader set of APIs including Ope

I was aware of s2n-bignum which is a very cool project, but apparently there is a larger sister project, aws-lc, that aims for broader set of APIs including OpenSSL compatibility, while retaining the general approach and vibe (lots of formal verification + performance work): https://github.com/aws/aws-lc https://github.com/aws/aws-lc That's pretty sweet. I'm currently using BoringSSL in a project as a supplement to OpenSSL (mostly because it is much easier to build for Windows users than requiring them to fiddle with msys2/vcpkg etc; the alternative is to rely on the Windows CNG API, but it lacks features like ed25519 support.) I wonder how much effort it would take to use aws-lc instead... Not that I'm that interested, BSSL is pretty good, but free performance and heavy automated verification is always nice :) Related: one of the authors of this post, John Harrison, wrote a really good book about automated theorm proving about 15 years ago while working on floating point verification at Intel -- there's still no other book quite like this one, I think https://www.cl.cam.ac.uk/~jrh13/ https://www.cl.cam.ac.uk/~jrh13/