S2N is great, clean, actively maintained, and even has experimental support for post-quantum key exchange (compatible with BoringSSL and the Zig standard library).

Other very nice TLS implementations in C/C++:

- Facebook Fizz: https://github.com/facebookincubator/fizz

- PicoTLS: https://github.com/h2o/picotls

"Continuous formal verification of Amazon s2n" (2018) https://link.springer.com/chapter/10.1007/978-3-319-96142-2_...

https://scholar.google.com/scholar?cites=2686812922904040715...

But formal methods (and TLA+ for distributed computation) don't eliminate side channels.

> But formal methods (and TLA+ for distributed computation) don't eliminate side channels.

True, but they eliminate whole classes of attack. I'm normally aghast at people writing new code in plain C, but formally verified plain C counts as a whole other and better paradigm to me.

> I'm normally aghast at people writing new code in plain C,

Why?

There have been some attempts at formally verifying lack of timing attacks (to the extent allowed by hardware). This is the one I know the most about: https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 but there are likely others

Also in around side channel topic for example:

E. Prouff and M. Rivain, Masking against Side-Channel Attacks: A Formal Security Proof, EUROCRYPT 2013, LNCS 7881

S. Dziembowski and K. Pietrzak, "Leakage-Resilient Cryptography, 10.1109/FOCS.2008.56.

Side-channel: https://en.wikipedia.org/wiki/Side-channel_attack

Time complexity > Constant time: https://en.wikipedia.org/wiki/Time_complexity#Constant_time

"Masking against side-channel attacks: A formal security proof" (2013) https://link.springer.com/chapter/10.1007/978-3-642-38348-9_... https://scholar.google.com/scholar?cites=1479355492097437276...

"Leakage-Resilient Cryptography" (2008) https://ieeexplore.ieee.org/abstract/document/4690963 https://scholar.google.com/scholar?cites=5581902451405085906...

"FaCT: A DSL for Timing-Sensitive Computation" https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 citations in gscholar: https://scholar.google.com/scholar?cites=1570199926308101856...

Clarification: this still has dependencies. For example, it requires one of "OpenSSL (versions 1.0.2, 1.1.1 and 3.0.x), LibreSSL, BoringSSL, AWS-LC, and the Apple Common Crypto framework to perform the underlying cryptographic operations"

it says "it supports" but not "it requires" in README

It seems to support multiple options but requires you pick at least one of them. https://github.com/aws/s2n-tls/blob/main/docs/BUILD.md#build...

AWS-LC is the recommended option of the supported choices, there doesn't seem to be a "built-in" type choice.