diff --git a/manifest.json b/manifest.json
index fa336cc3..9459c587 100644
--- a/manifest.json
+++ b/manifest.json
@@ -1262,6 +1262,13 @@
             }
           ]
         },
+        {
+          "path": "specifications/Paxos/VotingApalache.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
         {
           "path": "specifications/Paxos/Paxos.tla",
           "communityDependencies": [],
diff --git a/specifications/Paxos/README b/specifications/Paxos/README
index c6022b6f..ab0fcc90 100644
--- a/specifications/Paxos/README
+++ b/specifications/Paxos/README
@@ -29,4 +29,8 @@ MCPaxos
   three specifications above.  The Toolbox makes it unnecessary
   for the user to write such specs, essentially producing them
   itself from the models defined by the user.
-   
\ No newline at end of file
+   
+VotingApalache
+  A version of the Voting specification that can be analyzed
+  the the Apalache model-checker. Also contains an inductive
+  invariant that Apalache can verify for small system sizes.