Galois s2n is a formal verification project that proves the correctness of Amazon's s2n TLS library implementations. The project uses Galois' Software Analysis Workbench (SAW) to demonstrate equivalence between specifications written in the Cryptol language and the C code of s2n. The verification covers the implementation of the keyed-Hash Message Authentication Code (HMAC) algorithm and the Deterministic Random Bit Generator (DRBG). The project reduces reasoning about 103 lines of HMAC code to 3 lines of Cryptol by proving equivalence between the Cryptol implementation and C program, then performing further reasoning using the mathematical Cryptol program. The verification process is automated and integrated into Amazon's continuous integration system, running automatically with each code change. The proofs often remain intact despite changes to the software. The tools are integrated into the s2n build environment, allowing anyone with prerequisites to run the same proofs on their own version of the s2n code. The project includes automated reporting of statistics from verification runs, making the formal methods work understandable to those without a formal methods background. A tool scrapes the continuous integration system to compile useful statistics that can be viewed live.