This is an English version of an article first published, in French, on my blog: arcker.org. It's part of an educational series about Verbose — an experimental language whose compiler verifies proofs declared in source and emits small, readable x86-64 machine code.
When your browser shows a little padlock next to a URL, it has just held a cryptographic conversation with the server — the TLS handshake. That conversation is usually handled by enormous C libraries: OpenSSL, BoringSSL, hundreds of thousands of lines nobody ever reads in full.
This article is the capstone of the crypto arc of the series. It shows the payoff: a real browser opens an HTTPS page served by a binary whose every cryptographic transform — the key exchange, the identity signature, the bulk encryption, the hash — is machine code emitted by Verbose. Not one line of OpenSSL. And the browser, the most demanding TLS client there is, can't tell the difference: it completes the handshake and renders the page.
We build on SHA-256 (chapter 1 of the arc) — it shows up everywhere in TLS. The details of each brick (AES, Ed25519) get their own chapters; here we pull up and watch the whole thing work.
A handshake, in three ideas
