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

[1] https://mitls.org/