AFAIK Noise has end-to-end proofs of correctness using CryptoVerif, the work having mostly been done by the Prosecco team at INRIA. You can explore Noise protoc

AFAIK Noise has end-to-end proofs of correctness using CryptoVerif, the work having mostly been done by the Prosecco team at INRIA. You can explore Noise protocols on NoiseExplorer [0][1] Also I may be wrong again, but it is for TLS, that even with all the simplifications and major changes on TLS 1.3, that we only have proofs of correctness for certain subsets of the spec, and specific modes of operation (theres a version of the protocol targeting IoT for which this work has been done, but I can't remember the name) [0] https://noiseexplorer.com/ https://noiseexplorer.com/ [1] https://rwc.iacr.org/2019/slides/NoiseExplorer.pdf https://rwc.iacr.org/2019/slides/NoiseExplorer.pdf