diff --git a/README.md b/README.md
index 15e3d390..4de97f34 100644
--- a/README.md
+++ b/README.md
@@ -87,7 +87,8 @@ Here is a list of specs included in this repository, with links to the relevant
 | [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                                      |          |             |         |           |          |
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |             |         |           |          |
-| [Yo-Yo Leader Election](specifications/YoYo)                                                 | Ludovic Yvoz, Stephan Merz           |          |             |         |      ✔    |          |
+| [Yo-Yo Leader Election](specifications/YoYo)                                                        | Ludovic Yvoz, Stephan Merz                          |          |             |         |      ✔    |          |
+| [TCP as defined in RFC 9293](specifications/tcp)                                                    | Markus Kuppe                                        |          |             |         |      ✔    |          |
 
 ## Examples Elsewhere
 Here is a list of specs stored in locations outside this repository, including submodules.
diff --git a/manifest.json b/manifest.json
index e24d082a..20967ccf 100644
--- a/manifest.json
+++ b/manifest.json
@@ -5128,6 +5128,50 @@
           ]
         }
       ]
+    },
+    {
+      "path": "specifications/tcp",
+      "title": "TCP as defined in RFC 9293",
+      "description": "Transmission Control Protocol (TCP)",
+      "sources": ["https://datatracker.ietf.org/doc/html/rfc9293"],
+      "authors": [
+        "Markus Kuppe"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/tcp/tcp.tla",
+          "communityDependencies": [
+            "SequencesExt"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/tcp/MCtcp.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "state constraint",
+            "symmetry"
+          ],
+          "models": [
+            {
+              "path": "specifications/tcp/MCtcp.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+              ],
+              "result": "success",
+              "distinctStates": 598,
+              "totalStates": 3196,
+              "stateDepth": 14
+            }
+          ]
+        }
+      ]
     }
   ]
 }
diff --git a/specifications/tcp/MCtcp.cfg b/specifications/tcp/MCtcp.cfg
new file mode 100644
index 00000000..0b4b9c74
--- /dev/null
+++ b/specifications/tcp/MCtcp.cfg
@@ -0,0 +1,22 @@
+CONSTANTS
+    A = A
+    B = B
+
+CONSTANT
+    Peers <- peers
+
+SYMMETRY
+    Symmetry
+
+SPECIFICATION 
+    Spec
+
+INVARIANT 
+    TypeOK
+    Inv
+
+CONSTRAINT 
+    NoRetransmission
+
+ACTION_CONSTRAINT 
+    SingleActiveOpen
diff --git a/specifications/tcp/MCtcp.tla b/specifications/tcp/MCtcp.tla
new file mode 100644
index 00000000..4e7810e8
--- /dev/null
+++ b/specifications/tcp/MCtcp.tla
@@ -0,0 +1,24 @@
+---- MODULE MCtcp ----
+EXTENDS tcp, TLC
+
+CONSTANTS A, B
+peers == {A, B}
+Symmetry == Permutations(peers)
+
+NoRetransmission ==
+    \A p \in Peers :
+        \A i \in 1..Len(network[p]) - 1 :
+            network[p][i] # network[p][i + 1]
+
+SingleActiveOpen ==
+    \* A real system will allow infinitely many active opens of TCP connections. An
+    \* explicit state model checker like TLC cannot enumerate infinitely many states.
+    \* Thus, do not allow multiple active opens (the first active open is implicit in Init).
+    ~ \E local, remote \in Peers:
+        \/ ACTIVE_OPEN(local, remote)
+        \/ PASSIVE_OPEN(local, remote)
+        \/ SEND(local, remote)
+
+=============================================================================
+\* Modification History
+\* Created Tue Apr 02 10:38:50 PDT 2024 by markus
diff --git a/specifications/tcp/tcp.tla b/specifications/tcp/tcp.tla
new file mode 100644
index 00000000..7e01da22
--- /dev/null
+++ b/specifications/tcp/tcp.tla
@@ -0,0 +1,330 @@
+------------------------------- MODULE tcp ----------------------------------
+(* https://datatracker.ietf.org/doc/html/rfc9293 *)
+EXTENDS Integers, Sequences, SequencesExt, FiniteSets
+
+CONSTANT 
+    Peers
+
+ASSUME Cardinality(Peers) = 2
+
+States == {"LISTEN", "CLOSED", "SYN-SENT", "SYN-RECEIVED", "ESTABLISHED", 
+          "FIN-WAIT-1", "FIN-WAIT-2", "CLOSING", "CLOSE-WAIT", "LAST-ACK",
+          "TIME-WAIT"}
+
+(*
+Modeling siplifications:
+- No TCBs
+- User commands are not modeled directly, but may happen implicitly. However, active open is only allowed from the initial state.
+- No retransmissions (NoRetransmissions state constraint) or timeouts are modeled.
+*)
+
+VARIABLE
+    tcb,
+    connstate,
+    network
+
+vars == <<tcb, connstate, network>>
+
+TypeOK ==
+    /\ tcb \in [ Peers -> BOOLEAN ]
+    /\ connstate \in [ Peers -> States ]
+    /\ network \in [ Peers -> Seq({"SYN", "SYN,ACK", "ACK", "RST", "FIN"} \cup {"ACKofFIN"}) ]
+
+Init ==
+    \* One node starts in the SYN-SENT state, i.e., one node has already received the active open command. The other node
+    \* is in the listen state, i.e., it has received the passive open command.
+    \E node \in Peers:
+        /\ tcb = [p \in Peers |-> TRUE]
+        /\ connstate = [p \in Peers |-> IF p = node THEN "SYN-SENT" ELSE "LISTEN"]
+        /\ network = [p \in Peers |-> IF p = node THEN <<>> ELSE << "SYN" >>]
+
+\* Action triggered by user commands:
+
+PASSIVE_OPEN(local, remote) ==
+    \* User command: PASSIVE-OPEN
+    /\ local # remote
+    /\ connstate[local] = "CLOSED"
+    /\ UNCHANGED network
+    /\ connstate' = [connstate EXCEPT ![local] = "LISTEN"]
+    /\ tcb' = [tcb EXCEPT ![local] = TRUE]
+
+ACTIVE_OPEN(local, remote) ==
+    \* User command: ACTIVE-OPEN
+    /\ local # remote
+    /\ connstate[local] = "CLOSED"
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN")]
+    /\ connstate' = [connstate EXCEPT ![local] = "SYN-SENT"]
+    /\ tcb' = [tcb EXCEPT ![local] = TRUE]
+
+CLOSE_SYN_SENT(local, remote) ==
+    \* User command: CLOSE
+    /\ local # remote
+    /\ connstate[local] = "SYN-SENT"
+    /\ UNCHANGED network
+    /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"]
+    /\ tcb' = [tcb EXCEPT ![local] = FALSE]
+
+CLOSE_SYN_RECEIVED(local, remote) ==
+    \* User Command: CLOSE
+    /\ local # remote
+    /\ connstate[local] = "SYN-RECEIVED"
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "FIN")]
+    /\ connstate' = [connstate EXCEPT ![local] = "FIN-WAIT-1"]
+    /\ UNCHANGED tcb
+
+SEND(local, remote) ==
+    \* User command: SEND
+    /\ local # remote
+    /\ connstate[local] = "LISTEN"
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN")]
+    /\ connstate' = [connstate EXCEPT ![local] = "SYN-SENT"]
+    /\ UNCHANGED tcb
+
+CLOSE_LISTEN(local, remote) ==
+    \* User command: CLOSE
+    /\ local # remote
+    /\ connstate[local] = "LISTEN"
+    /\ UNCHANGED network
+    /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"]
+    /\ tcb' = [tcb EXCEPT ![local] = FALSE]
+
+CLOSE_ESTABLISHED(local, remote) ==
+    \* User command: CLOSE
+    /\ local # remote
+    /\ connstate[local] = "ESTABLISHED"
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "FIN")]
+    /\ connstate' = [connstate EXCEPT ![local] = "FIN-WAIT-1"]
+    /\ UNCHANGED tcb
+
+CLOSE_CLOSE_WAIT(local, remote) ==
+    \* User command: CLOSE
+    /\ local # remote
+    /\ connstate[local] = "CLOSE-WAIT"
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "FIN")]
+    /\ connstate' = [connstate EXCEPT ![local] = "LAST-ACK"]
+    /\ UNCHANGED tcb
+
+User ==
+    \E local, remote \in Peers :
+        \/ ACTIVE_OPEN(local, remote)
+        \/ PASSIVE_OPEN(local, remote)
+        \/ CLOSE_SYN_SENT(local, remote)
+        \/ CLOSE_SYN_RECEIVED(local, remote)
+        \/ CLOSE_LISTEN(local, remote)
+        \/ CLOSE_ESTABLISHED(local, remote)
+        \/ CLOSE_CLOSE_WAIT(local, remote)
+        \/ SEND(local, remote)
+
+-----------------------------------------------------------------------------
+       
+SynSent(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "SYN-SENT"
+    /\ UNCHANGED tcb
+    /\ \/ /\ IsPrefix(<<"SYN">>, network[local])
+          /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN,ACK"),
+                                         ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "SYN-RECEIVED"]
+       \/ /\ IsPrefix(<<"SYN,ACK">>, network[local])
+          /\ network' = [ network EXCEPT ![remote] = Append(@, "ACK"),
+                                         ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "ESTABLISHED"]
+
+SynReceived(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "SYN-RECEIVED"
+    /\ UNCHANGED tcb
+    /\ \/ /\ IsPrefix(<<"RST">>, network[local]) \* TODO: note 1 in RFC 9293 (must have gotten here from a *passive* OPEN, i.e., LISTEN)
+          /\ network' = [ network EXCEPT ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "LISTEN"]
+       \/ /\ IsPrefix(<<"ACK">>, network[local]) \* TODO: ACK of SYN
+          /\ network' = [ network EXCEPT ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "ESTABLISHED"]
+
+Listen(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "LISTEN"
+    /\ UNCHANGED tcb
+    /\ \/ /\ IsPrefix(<<"SYN">>, network[local])
+          /\ network' = [ network EXCEPT ![remote] = Append(@, "SYN,ACK"),
+                                         ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "SYN-RECEIVED"]
+
+Established(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "ESTABLISHED"
+    /\ UNCHANGED tcb
+    /\ IsPrefix(<<"FIN">>, network[local])
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"),
+                                   ![local] = Tail(network[local])]
+    /\ connstate' = [connstate EXCEPT ![local] = "CLOSE-WAIT"]
+
+-----------------------------------------------------------------------------
+
+FinWait1(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "FIN-WAIT-1"
+    /\ UNCHANGED tcb
+    /\ \/ /\ IsPrefix(<<"FIN">>, network[local])
+          /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"),
+                                         ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "CLOSING"]
+       \/ /\ IsPrefix(<<"ACKofFIN">>, network[local])
+          /\ network' = [ network EXCEPT ![local] = Tail(network[local])]
+          /\ connstate' = [connstate EXCEPT ![local] = "FIN-WAIT-2"]
+
+FinWait2(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "FIN-WAIT-2"
+    /\ UNCHANGED tcb
+    /\ IsPrefix(<<"FIN">>, network[local])
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"),
+                                   ![local] = Tail(network[local])]
+    /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"]
+
+Closing(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "CLOSING"
+    /\ UNCHANGED tcb
+    /\ IsPrefix(<<"ACKofFIN">>, network[local])
+    /\ network' = [ network EXCEPT ![local] = Tail(network[local])]
+    /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"]
+
+LastAck(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "LAST-ACK"
+    /\ UNCHANGED tcb
+    /\ IsPrefix(<<"ACKofFIN">>, network[local])
+    /\ network' = [ network EXCEPT ![local] = Tail(network[local])]
+    /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"]
+
+TimeWait(local, remote) ==
+    /\ local # remote
+    /\ connstate[local] = "TIME-WAIT"
+    /\ tcb[local]
+    /\ UNCHANGED network
+    /\ connstate' = [connstate EXCEPT ![local] = "CLOSED"]
+    /\ tcb' = [tcb EXCEPT ![local] = FALSE]
+    \* TODO: Timeout=2MSL
+
+Note2(local, remote) ==
+    (* Note 2: A transition from FIN-WAIT-1 to TIME-WAIT if a FIN is received
+       and the local FIN is also acknowledged. *)
+    /\ local # remote
+    /\ connstate[local] = "FIN-WAIT-1"
+    /\ UNCHANGED tcb
+    \* The local FIN is also acknowledged, i.e., skipping the CLOSING state.
+    /\ IsPrefix(<< "FIN", "ACKofFIN" >>, network[local])
+    \* ??? The RFC doesn't explictly mention this, but we send the ACKofFIN here.
+    /\ network' = [ network EXCEPT ![remote] = Append(@, "ACKofFIN"),
+                                   ![local] = SubSeq(network[local], 3, Len(network[local]))]
+    /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"]
+
+System ==
+    \E local, remote \in Peers :
+        \/ SynSent(local, remote)
+        \/ SynReceived(local, remote)
+        \/ Listen(local, remote)
+        \/ Established(local, remote)
+        \/ FinWait1(local, remote)
+        \/ FinWait2(local, remote)
+        \/ Closing(local, remote)
+        \/ LastAck(local, remote)
+        \/ TimeWait(local, remote)
+        \/ Note2(local, remote)
+
+Note3(local, remote) ==
+    (* Note 3: A RST can be sent from any state with a corresponding transition 
+       to TIME-WAIT (see [70] for rationale). Similarly, receipt of a RST from
+       any state results in a transition to LISTEN or CLOSED. *)
+    \* ??? "...can be sent from any state with a corresponding transition to TIME-WAIT"
+    \* ??? could also be interpreted as those states from where we can tranisiton to TIME-WAIT,
+    \* ??? i.e., FIN-WAIT-1, FIN-WAIT-2, CLOSING.
+    /\ local # remote
+    /\ UNCHANGED tcb
+    /\ \/ /\ tcb[local] \* ??? RFC 9293 doesn't mention this, but it seems impossible to send a RST without a TCB.
+          /\ network' = [ network EXCEPT ![remote] = Append(@, "RST")]
+          /\ connstate' = [connstate EXCEPT ![local] = "TIME-WAIT"]
+       \/ /\ IsPrefix(<<"RST">>, network[local])
+          /\ network' = [ network EXCEPT ![local] = Tail(network[local])]
+          /\ \/ connstate' = [connstate EXCEPT ![local] = "LISTEN"]
+             \/ connstate' = [connstate EXCEPT ![local] = "CLOSED"]
+
+Reset ==
+    \E local, remote \in Peers :
+        Note3(local, remote)
+
+Next ==
+    \/ System
+    \/ Reset
+    \/ User
+
+Spec ==
+    /\ Init
+    /\ [][Next]_vars
+    /\ WF_vars(System)
+    \* Would get stuck in SYN-SENT if we don't assert a user command.
+    /\ WF_vars(\E local, remote \in Peers: CLOSE_CLOSE_WAIT(local, remote))
+
+-----------------------------------------------------------------------------
+
+Inv ==
+    \* If there are no messages in flight and one node is in the ESTABLISHED
+    \* state, then the other node is also in the ESTABLISHED state. When
+    \* message are in flight, the state of the nodes can be different.
+    \A local, remote \in { p \in Peers : network[p] = <<>> } :
+        connstate[local] = "ESTABLISHED" <=> connstate[remote] = "ESTABLISHED"
+
+=============================================================================
+\* Modification History
+\* Created Tue Apr 02 10:38:50 PDT 2024 by markus
+
+
+
+From RFC 9293:
+
+                            +---------+ ---------\      active OPEN
+                            |  CLOSED |            \    -----------
+                            +---------+<---------\   \   create TCB
+                              |     ^              \   \  snd SYN
+                 passive OPEN |     |   CLOSE        \   \
+                 ------------ |     | ----------       \   \
+                  create TCB  |     | delete TCB         \   \
+                              V     |                      \   \
+          rcv RST (note 1)  +---------+            CLOSE    |    \
+       -------------------->|  LISTEN |          ---------- |     |
+      /                     +---------+          delete TCB |     |
+     /           rcv SYN      |     |     SEND              |     |
+    /           -----------   |     |    -------            |     V
++--------+      snd SYN,ACK  /       \   snd SYN          +--------+
+|        |<-----------------           ------------------>|        |
+|  SYN   |                    rcv SYN                     |  SYN   |
+|  RCVD  |<-----------------------------------------------|  SENT  |
+|        |                  snd SYN,ACK                   |        |
+|        |------------------           -------------------|        |
++--------+   rcv ACK of SYN  \       /  rcv SYN,ACK       +--------+
+   |         --------------   |     |   -----------
+   |                x         |     |     snd ACK
+   |                          V     V
+   |  CLOSE                 +---------+
+   | -------                |  ESTAB  |
+   | snd FIN                +---------+
+   |                 CLOSE    |     |    rcv FIN
+   V                -------   |     |    -------
++---------+         snd FIN  /       \   snd ACK         +---------+
+|  FIN    |<----------------          ------------------>|  CLOSE  |
+| WAIT-1  |------------------                            |   WAIT  |
++---------+          rcv FIN  \                          +---------+
+  | rcv ACK of FIN   -------   |                          CLOSE  |
+  | --------------   snd ACK   |                         ------- |
+  V        x                   V                         snd FIN V
++---------+               +---------+                    +---------+
+|FINWAIT-2|               | CLOSING |                    | LAST-ACK|
++---------+               +---------+                    +---------+
+  |              rcv ACK of FIN |                 rcv ACK of FIN |
+  |  rcv FIN     -------------- |    Timeout=2MSL -------------- |
+  |  -------            x       V    ------------        x       V
+   \ snd ACK              +---------+delete TCB          +---------+
+     -------------------->|TIME-WAIT|------------------->| CLOSED  |
+                          +---------+                    +---------+
+