Ignoring for a moment the fact that this is an alpha release (and that as such, a handful of minor proofs, e.g. mundane facts related to endianness conversions, have yet to be completed), there are several limitations of our work.
- Our tools themselves are not verified, so there could be a bug in F, z3, the kremlin F-to-C compiler; or a bug about the C compiler itself (unless one uses a constant-time fork of CompCert). We consider most of these to be theoretically unpleasant, but still an acceptable tradeoff.
- Specifications are extremely hard to get right: one might introduce a typo when reading an RFC, or, say, state an endianness conversion wrong. So, even before implementing an optimized version of anything, we audit and test the spec first. This is usually a good sanity check, but certainly not bulletproof (note that this is a general problem of software verification, not specific to us).
- As noted near the end of the article, our models do not account for Spectre and Meltdown; and there might be new classes of attacks that we can't guard against, for the simple reason that they haven't been found yet.
As to whether this is an attempt to get free security audits, I guess we weren't intentionally thinking of it! But we certainly would love it if people could test the code and give us feedback on what to improve to make this an even more compelling choice for whoever needs a good cryptographic library. I've written a bit about this here: https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.ht...