Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS"
From the abstract: "mplementations of the Transport Layer Security
(TLS) protocol must handle a variety of protocol versions and
extensions, authentication modes and key exchange methods,
where each combination may prescribe a different message
sequence between the client and the server. We address the
problem of designing a robust
composite
state machine that can
correctly multiplex between these different protocol modes. We
systematically test popular open-source TLS implementations
for state machine bugs and discover several critical security
vulnerabilities that have lain hidden in these libraries for years ..."
Based on this work you might say that there are formal state machines for TLS, but they aren't in the standard.
