You can do formal verification with tools like Coq using a laptop. The real issue is that writing a formal specification is hard even for small problems; writing a formal spec for something like TLS would be harder than actually implementing TLS.
https://en.wikipedia.org/wiki/Curry-Howard_Correspondence
Basically, checking a proof of correctness for software is equivalent to type checking (for a very fancy type system).