You can prove a TLS implementation correct up to defined assumptions (e.g. clock consistency). There are already some projects working on this, eg https://project-everest.github.io/