[touisteur]

Yes, there are actually implementations of most standard stuff in Ada and SPARK (so with some level of proof)

Interesting posts (and links):

* https://blog.adacore.com/avoiding-vulnerabilities-in-crypto-...

* https://blog.adacore.com/sparknacl-two-years-of-optimizing-c...

* https://github.com/Componolit/libsparkcrypto

Proof of constant-time execution is an interesting field, but as I understand very much less mature than the SPARK toolset. If anyone has a toolchain working over llvm to check and/or make code constant-time, I'm interested.

I mean, if the standards people want to keep writing C, they can probably use Frama-C for the standard implementation...