This bit is an aside but it's interesting to me: "Earlier this year, with Galois, we completed a proof of our implementation of AES_CTR_DRBG, and formally verified that our code in s2n is equivalent to the written specification." That's amazing! I think it may be the first bit of provably correct code that I'm likely to actually use in practice.