From 6734750497eea969e0e6b1a08844c53db6e5ded8 Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Mon, 8 Jan 2024 16:12:41 +0000
Subject: [PATCH] Only send AEs to known servers (#5896)

---
 tla/consensus/ccfraft.tla | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index a69382e809f2..6b03b3a76e21 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -553,6 +553,7 @@ AppendEntries(i, j) ==
     \* No messages to itself and sender is primary
     /\ state[i] = Leader
     /\ i /= j
+    /\ j \in GetServerSet(i)
     \* AppendEntries must be sent for historical entries, unless
     \* snapshots are used. Whether the node is in configuration at
     \* that index makes no difference.