ABSTRACT. We describe formal verification of the open source TLS implementation used in numerous Amazon services, ranging from the Amazon Simple Storage Service (S3) to the Amazon Web Services Software Development Kit (AWS SDK). A key aspect of this proof is continuous checking: to ensure that properties proved remain proved during the lifetime of the software, at each change to the code, proofs are automatically re-established with little to no interaction from the development community. Technical decisions made about the structure of the proof and tools employed were driven by this goal.