You could write those in Vale[0], but at that point, just use miTLS[1] to have a completely verified TLS implementation. [0] https://github.com/project-everest

You could write those in Vale[0], but at that point, just use miTLS[1] to have a completely verified TLS implementation. [0] https://github.com/project-everest/vale https://github.com/project-everest/vale [1] https://mitls.org/ https://mitls.org/