diff --git a/README.md b/README.md
index 2226976f..29d22400 100644
--- a/README.md
+++ b/README.md
@@ -65,7 +65,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Finitizing Monotonic Systems](specifications/FiniteMonotonic)                                      | Andrew Helwer                              |          |             |         |     ✔     |          |
 | [The Readers-Writers Problem](specifications/ReadersWriters)                                        | Isaac DeFrain                              |          |             |         |     ✔     |          |
 | [Einstein's Riddle](specifications/EinsteinRiddle)                                                  | Isaac DeFrain                              |          |             |         |     ✔     |          |
-| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz)                                     | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
+| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz)                                     | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
 | [Folklore Reliable Broadcast](specifications/bcastFolklore)                                         | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
 | [The Bosco Byzantine Consensus Algorithm](specifications/bosco)                                     | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
 | [Consensus in One Communication Step](specifications/c1cs)                                          | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
diff --git a/manifest.json b/manifest.json
index 35f4ca75..0f0d37c3 100644
--- a/manifest.json
+++ b/manifest.json
@@ -2712,7 +2712,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/aba-asyn-byz/aba_asyn_byz.cfg",
+              "runtime": "00:10:00",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },