diff --git a/.github/scripts/check_markdown_table.py b/.github/scripts/check_markdown_table.py
index 0b6bfd37..f689517e 100644
--- a/.github/scripts/check_markdown_table.py
+++ b/.github/scripts/check_markdown_table.py
@@ -180,6 +180,7 @@ def from_json(spec):
     for path, json, md in different_tlc_flag:
         print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a TLC Model flag in README.md table')
 
+'''
 # Ensure Apalache flag is correct
 different_apalache_flag = [
     (manifest_spec.path, manifest_spec.apalache, table_spec.apalache)
@@ -191,6 +192,7 @@ def from_json(spec):
     print('ERROR: Apalache Model flags in README.md table differ from model records in manifest.json:')
     for path, json, md in different_tlc_flag:
         print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' an Apalache Model flag in README.md table')
+'''
 
 if success:
     print('SUCCESS: manifest.json concords with README.md table')
diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py
index e1fd4c31..79f87273 100644
--- a/.github/scripts/check_small_models.py
+++ b/.github/scripts/check_small_models.py
@@ -17,6 +17,7 @@
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True)
 parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
 parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[])
+parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
 args = parser.parse_args()
 
 logging.basicConfig(level=logging.INFO)
@@ -27,6 +28,7 @@
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
 skip_models = [normpath(path) for path in args.skip]
+only_models = [normpath(path) for path in args.only]
 
 def check_model(module_path, model, expected_runtime):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -72,6 +74,7 @@ def check_model(module_path, model, expected_runtime):
         for model in module['models']
             if model['size'] == 'small'
             and normpath(model['path']) not in skip_models
+            and (only_models == [] or normpath(model['path']) in only_models)
     ],
     key = lambda m: m[2],
     reverse=True
diff --git a/.github/scripts/format_markdown_table.py b/.github/scripts/format_markdown_table.py
index 2b1bb41d..c1c7ab88 100644
--- a/.github/scripts/format_markdown_table.py
+++ b/.github/scripts/format_markdown_table.py
@@ -16,10 +16,6 @@
 parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
 args = parser.parse_args()
 
-readme = None
-with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
-    readme = mistletoe.Document(readme_file)
-
 columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']
 
 def get_column(row, index):
@@ -64,11 +60,21 @@ def format_table(table):
     '''
     return
 
-table = next((child for child in readme.children if isinstance(child, Table)))
-format_table(table)
+def format_document(document):
+    '''
+    All document transformations should go here.
+    '''
+    # Gets table of local specs
+    table = next((child for child in document.children if isinstance(child, Table)))
+    format_table(table)
 
-# Write formatted markdown to README.md
-with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file:
-    with MarkdownRenderer() as renderer:
+# Read, format, write
+# Need to both parse & render within same MarkdownRenderer context to preserve other formatting
+with MarkdownRenderer() as renderer:
+    readme = None
+    with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
+        readme = mistletoe.Document(readme_file)
+    format_document(readme)
+    with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file:
         readme_file.write(renderer.render(readme))
 
diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py
index 3c55f388..b8c6fe60 100644
--- a/.github/scripts/generate_manifest.py
+++ b/.github/scripts/generate_manifest.py
@@ -52,15 +52,20 @@ def get_cfg_files(examples_root, tla_path):
     Assume a .cfg file in the same directory as the .tla file and with the
     same name is a model of that .tla file; also assume this of any .cfg
     files where the .tla file name is only a prefix of the .cfg file name,
-    unless there are other .tla file names in the directory that exactly
-    match the .cfg file name.
+    unless there are other .tla file names in the directory that are longer
+    prefixes of the .cfg file name.
     """
     parent_dir = dirname(tla_path)
     module_name, _ = splitext(basename(tla_path))
     other_module_names = [other for other in get_module_names_in_dir(examples_root, parent_dir) if other != module_name]
     return [
-        path for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg', root_dir=examples_root)
-        if splitext(basename(path))[0] not in other_module_names
+        path
+        for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg', root_dir=examples_root)
+        if not any([
+            splitext(basename(path))[0].startswith(other_module_name)
+            for other_module_name in other_module_names
+            if len(other_module_name) > len(module_name)
+        ])
     ]
 
 def generate_new_manifest(examples_root, ignored_dirs, parser, queries):
diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py
index f10b765f..85ea568a 100644
--- a/.github/scripts/tla_utils.py
+++ b/.github/scripts/tla_utils.py
@@ -108,6 +108,7 @@ def resolve_tlc_exit_code(code):
     """
     tlc_exit_codes = {
         0   : 'success',
+        10  : 'assumption failure',
         11  : 'deadlock failure',
         12  : 'safety failure',
         13  : 'liveness failure'
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index df6bfab4..c6b491f2 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -28,13 +28,13 @@ jobs:
         shell: bash
     steps:
       - name: Clone repo
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Install python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: '3.11'
       - name: Install Java
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           distribution: adopt
           java-version: 17
diff --git a/.gitignore b/.gitignore
index 296e2e33..dd480ffd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -38,9 +38,11 @@ pyvenv.cfg
 
 ## Ignore directories used for local CI testing
 deps/
+tree-sitter-tlaplus/
 
 # Ignore TTrace specs
 *_TTrace_*.tla
 
 ## Blacklist tools/ folder created by .devcontainer.json
 tools/
+
diff --git a/README.md b/README.md
index b9beacc7..7ba62fe8 100644
--- a/README.md
+++ b/README.md
@@ -18,10 +18,11 @@ All specs in this repository are subject to CI validation to ensure quality.
 Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
 | Name                                                                                                | Author(s)                                  | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
 | --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: |
+| [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |     ✔     |          |
+| [Loop Invariance](specifications/LoopInvariance)                                                    | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |     ✔     |          |
 | [Learn TLA⁺ Proofs](specifications/LearnProofs)                                                     | Andrew Helwer                              |    ✔     |      ✔      |    ✔    |     ✔     |          |
-| [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |           |          |
 | [Boyer-Moore Majority Vote](specifications/Majority)                                                | Stephan Merz                               |    ✔     |      ✔      |         |     ✔     |          |
-| [Proof x+x is Even](specifications/sums_even)                                                       | Stephan Merz                               |    ✔     |      ✔      |         |           |          |
+| [Proof x+x is Even](specifications/sums_even)                                                       | Stephan Merz                               |    ✔     |      ✔      |         |     ✔     |          |
 | [The N-Queens Puzzle](specifications/N-Queens)                                                      | Stephan Merz                               |    ✔     |             |    ✔    |     ✔     |          |
 | [The Dining Philosophers Problem](specifications/DiningPhilosophers)                                | Jeff Hemphill                              |    ✔     |             |    ✔    |     ✔     |          |
 | [The Car Talk Puzzle](specifications/CarTalkPuzzle)                                                 | Leslie Lamport                             |    ✔     |             |         |     ✔     |          |
@@ -31,17 +32,16 @@ Here is a list of specs included in this repository, with links to the relevant
 | [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi)                                          | Markus Kuppe, Alexander Niederbühl         |    ✔     |             |         |     ✔     |          |
 | [Missionaries and Cannibals](specifications/MissionariesAndCannibals)                               | Leslie Lamport                             |    ✔     |             |         |     ✔     |          |
 | [The Coffee Can Bean Problem](specifications/CoffeeCan)                                             | Andrew Helwer                              |    ✔     |             |         |     ✔     |          |
-| [Stone Scale Puzzle](specifications/Stones)                                                         | Leslie Lamport                             |    ✔     |             |         |           |          |
-| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz               |          |      ✔      |    ✔    |           |          |
-| [Misra Reachability Algorithm](specifications/MisraReachability)                                    | Leslie Lamport                             |          |      ✔      |    ✔    |           |          |
-| [Loop Invariance](specifications/LoopInvariance)                                                    | Leslie Lamport                             |          |      ✔      |    ✔    |           |          |
+| [Stone Scale Puzzle](specifications/Stones)                                                         | Leslie Lamport                             |    ✔     |             |         |     ✔     |          |
+| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz               |          |      ✔      |    ✔    |     ✔     |          |
+| [Misra Reachability Algorithm](specifications/MisraReachability)                                    | Leslie Lamport                             |          |      ✔      |    ✔    |     ✔     |          |
 | [EWD840: Termination Detection in a Ring](specifications/ewd840)                                    | Stephan Merz                               |          |      ✔      |         |     ✔     |          |
 | [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe                 |          |      ✔      |         |     ✔     |          |
 | [The Paxos Protocol](specifications/Paxos)                                                          | Leslie Lamport                             |          |      ✔      |         |     ✔     |          |
-| [Asynchronous Reliable Broadcast](specifications/bcastByz)                                          | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |      ✔      |         |           |          |
-| [Distributed Mutual Exclusion](specifications/lamport_mutex)                                        | Stephan Merz                               |          |      ✔      |         |           |          |
-| [Two-Phase Handshaking](specifications/TwoPhase)                                                    | Leslie Lamport, Stephan Merz               |          |      ✔      |         |           |          |
-| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward)                       | Leslie Lamport                             |          |      ✔      |         |           |          |
+| [Asynchronous Reliable Broadcast](specifications/bcastByz)                                          | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |      ✔      |         |     ✔     |          |
+| [Distributed Mutual Exclusion](specifications/lamport_mutex)                                        | Stephan Merz                               |          |      ✔      |         |     ✔     |          |
+| [Two-Phase Handshaking](specifications/TwoPhase)                                                    | Leslie Lamport, Stephan Merz               |          |      ✔      |         |     ✔     |          |
+| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward)                       | Leslie Lamport                             |          |      ✔      |         |     ✔     |          |
 | [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex)                              | Leslie Lamport                             |          |             |    ✔    |     ✔     |          |
 | [The Echo Algorithm](specifications/echo)                                                           | Stephan Merz                               |          |             |    ✔    |     ✔     |          |
 | [The TLC Safety Checking Algorithm](specifications/TLC)                                             | Markus Kuppe                               |          |             |    ✔    |     ✔     |          |
@@ -49,7 +49,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [The Slush Protocol](specifications/SlushProtocol)                                                  | Andrew Helwer                              |          |             |    ✔    |     ✔     |          |
 | [Minimal Circular Substring](specifications/LeastCircularSubstring)                                 | Andrew Helwer                              |          |             |    ✔    |     ✔     |          |
 | [Snapshot Key-Value Store](specifications/KeyValueStore)                                            | Andrew Helwer, Murat Demirbas              |          |             |    ✔    |     ✔     |          |
-| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts)               | Stephan Merz                               |          |             |    ✔    |           |          |
+| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts)               | Stephan Merz                               |          |             |    ✔    |     ✔     |          |
 | [Resource Allocator](specifications/allocator)                                                      | Stephan Merz                               |          |             |         |     ✔     |          |
 | [Transitive Closure](specifications/TransitiveClosure)                                              | Stephan Merz                               |          |             |         |     ✔     |          |
 | [Sliding Block Puzzle](specifications/SlidingPuzzles)                                               | Mariusz Ryndzionek                         |          |             |         |     ✔     |          |
@@ -65,24 +65,24 @@ 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  |          |             |         |           |          |
-| [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  |          |             |         |           |          |
-| [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore)                            | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [Failure Detector](specifications/detector_chan96)                                                  | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos)                                           | Leslie Lamport, Giuliano Losa              |          |             |         |           |          |
-| [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97)                               | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01)   | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [Spanning Tree Broadcast Algorithm](specifications/spanning)                                        | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [Transaction Commit Models](specifications/transaction_commit)                                      | Leslie Lamport, Jim Gray                   |          |             |         |           |          |
-| [Span Tree Exercise](specifications/SpanningTree)                                                   | Leslie Lamport                             |          |             |         |           |          |
-| [The Cigarette Smokers Problem](specifications/CigaretteSmokers)                                    | Mariusz Ryndzionek                         |          |             |         |           |          |
-| [Conway's Game of Life](specifications/GameOfLife)                                                  | Mariusz Ryndzionek                         |          |             |         |           |          |
-| [Chameneos, a Concurrency Game](specifications/Chameneos)                                           | Mariusz Ryndzionek                         |          |             |         |           |          |
+| [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  |          |             |         |     ✔     |          |
+| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore)                            | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
+| [Failure Detector](specifications/detector_chan96)                                                  | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
+| [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97)                               | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
+| [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01)   | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
+| [Spanning Tree Broadcast Algorithm](specifications/spanning)                                        | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
+| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos)                                           | Leslie Lamport, Giuliano Losa              |          |             |         |     ✔     |          |
+| [Transaction Commit Models](specifications/transaction_commit)                                      | Leslie Lamport, Jim Gray                   |          |             |         |     ✔     |          |
+| [Span Tree Exercise](specifications/SpanningTree)                                                   | Leslie Lamport                             |          |             |         |     ✔     |          |
+| [The Cigarette Smokers Problem](specifications/CigaretteSmokers)                                    | Mariusz Ryndzionek                         |          |             |         |     ✔     |          |
+| [Conway's Game of Life](specifications/GameOfLife)                                                  | Mariusz Ryndzionek                         |          |             |         |     ✔     |          |
+| [Chameneos, a Concurrency Game](specifications/Chameneos)                                           | Mariusz Ryndzionek                         |          |             |         |     ✔     |          |
+| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon)                                    | Martin Harrison                            |          |             |         |     ✔     |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                             |          |             |         |           |          |
-| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon)                                    | Martin Harrison                            |          |             |         |           |          |
+| [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
 
 ## Examples Elsewhere
 Here is a list of specs stored in locations outside this repository, including submodules.
@@ -137,7 +137,7 @@ Ideally these will be moved into this repo over time.
 
 ## License
 The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license.
-However, your spec can be included in this repo along with you own license if you wish.
+However, your spec can be included in this repo along with your own license if you wish.
 
 ## Support or Contact
 Do you have any questions or comments?
diff --git a/manifest-schema.json b/manifest-schema.json
index 7570d518..611f72d3 100644
--- a/manifest-schema.json
+++ b/manifest-schema.json
@@ -78,7 +78,7 @@
                         "type": "array",
                         "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}
                       },
-                      "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]}
+                      "result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]}
                     }
                   }
                 }
diff --git a/manifest.json b/manifest.json
index fa336cc3..26d75f6c 100644
--- a/manifest.json
+++ b/manifest.json
@@ -30,6 +30,42 @@
             "proof"
           ],
           "models": []
+        },
+        {
+          "path": "specifications/Bakery-Boulangerie/MCBakery.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/Bakery-Boulangerie/MCBakery.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/Bakery-Boulangerie/MCBoulanger.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/Bakery-Boulangerie/MCBoulanger.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "state constraint"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -138,7 +174,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/Chameneos/Chameneos.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -206,7 +253,16 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/CigaretteSmokers/CigaretteSmokers.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -475,7 +531,16 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/GameOfLife/GameOfLife.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -800,7 +865,9 @@
       "authors": [
         "Leslie Lamport"
       ],
-      "tags": [],
+      "tags": [
+        "beginner"
+      ],
       "modules": [
         {
           "path": "specifications/LoopInvariance/BinarySearch.tla",
@@ -812,6 +879,42 @@
           ],
           "models": []
         },
+        {
+          "path": "specifications/LoopInvariance/MCBinarySearch.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/LoopInvariance/MCBinarySearch.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/LoopInvariance/MCQuicksort.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/LoopInvariance/MCQuicksort.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/LoopInvariance/Quicksort.tla",
           "communityDependencies": [],
@@ -892,6 +995,66 @@
       ],
       "tags": [],
       "modules": [
+        {
+          "path": "specifications/MisraReachability/MCParReach.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/MisraReachability/MCParReach.cfg",
+              "runtime": "00:00:30",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/MisraReachability/MCReachabilityTest.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg",
+              "runtime": "00:00:20",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            },
+            {
+              "path": "specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/MisraReachability/MCReachable.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/MisraReachability/MCReachable.cfg",
+              "runtime": "00:01:30",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/MisraReachability/ParReach.tla",
           "communityDependencies": [],
@@ -1299,6 +1462,71 @@
           ],
           "models": []
         },
+        {
+          "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/PaxosHowToWinATuringAward/MCPaxos.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            },
+            {
+              "path": "specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/PaxosHowToWinATuringAward/MCVoting.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/PaxosHowToWinATuringAward/MCVoting.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla",
           "communityDependencies": [],
@@ -1641,41 +1869,87 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/SpanningTree/SpanTree.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/SpanningTree/SpanTreeRandom.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/SpanningTree/SpanTreeRandom.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock"
+              ],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/SpanningTree/SpanTreeTest.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
-        }
-      ]
-    },
-    {
-      "path": "specifications/SpecifyingSystems",
-      "title": "Specs from Specifying Systems",
-      "description": "All specs seen in the textbook Specifying Systems by Leslie Lamport",
-      "source": "http://lamport.azurewebsites.net/tla/book.html",
-      "authors": [
-        "Leslie Lamport"
-      ],
-      "tags": [
-        "beginner"
-      ],
-      "modules": [
-        {
-          "path": "specifications/SpecifyingSystems/AdvancedExamples/BNFGrammars.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
+          "models": [
+            {
+              "path": "specifications/SpanningTree/SpanTreeTest4Nodes.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            },
+            {
+              "path": "specifications/SpanningTree/SpanTreeTest5Nodes.cfg",
+              "runtime": "unknown",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "unknown"
+            }
+          ]
+        }
+      ]
+    },
+    {
+      "path": "specifications/SpecifyingSystems",
+      "title": "Specs from Specifying Systems",
+      "description": "All specs seen in the textbook Specifying Systems by Leslie Lamport",
+      "source": "http://lamport.azurewebsites.net/tla/book.html",
+      "authors": [
+        "Leslie Lamport"
+      ],
+      "tags": [
+        "beginner"
+      ],
+      "modules": [
+        {
+          "path": "specifications/SpecifyingSystems/AdvancedExamples/BNFGrammars.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
           "models": []
         },
         {
@@ -2370,7 +2644,16 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/Stones/Stones.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2433,7 +2716,16 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/TeachingConcurrency/Simple.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/TeachingConcurrency/SimpleRegular.tla",
@@ -2443,7 +2735,16 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/TeachingConcurrency/SimpleRegular.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2493,6 +2794,22 @@
           "features": [],
           "models": []
         },
+        {
+          "path": "specifications/TwoPhase/MCTwoPhase.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/TwoPhase/MCTwoPhase.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/TwoPhase/TLAPS.tla",
           "communityDependencies": [],
@@ -2530,7 +2847,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"
+            }
+          ]
         }
       ]
     },
@@ -2637,7 +2965,28 @@
           "features": [
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/bcastByz/bcastByz.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            },
+            {
+              "path": "specifications/bcastByz/bcastByzNoBcast.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2658,7 +3007,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/bcastFolklore/bcastFolklore.cfg",
+              "runtime": "00:30:00",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2679,7 +3039,16 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/bosco/bosco.cfg",
+              "runtime": "00:03:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2700,7 +3069,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/c1cs/c1cs.cfg",
+              "runtime": "unknown",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "unknown"
+            }
+          ]
         }
       ]
     },
@@ -2742,7 +3122,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/cf1s-folklore/cf1s_folklore.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2764,6 +3155,25 @@
             "pluscal"
           ],
           "models": []
+        },
+        {
+          "path": "specifications/chang_roberts/MCChangRoberts.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/chang_roberts/MCChangRoberts.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2798,7 +3208,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/detector_chan96/EnvironmentController.cfg",
+              "runtime": "02:00:00",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2902,6 +3323,22 @@
           "features": [],
           "models": []
         },
+        {
+          "path": "specifications/diskpaxos/MC_HDiskSynod.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/diskpaxos/MC_HDiskSynod.cfg",
+              "runtime": "unknown",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "unknown"
+            }
+          ]
+        },
         {
           "path": "specifications/diskpaxos/Synod.tla",
           "communityDependencies": [],
@@ -3480,21 +3917,56 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/glowingRaccoon/clean.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/glowingRaccoon/product.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/glowingRaccoon/product.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/glowingRaccoon/stages.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/glowingRaccoon/stages.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -3531,6 +4003,24 @@
           ],
           "models": []
         },
+        {
+          "path": "specifications/lamport_mutex/MCLamportMutex.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/lamport_mutex/MCLamportMutex.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "state constraint"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/lamport_mutex/NaturalsInduction.tla",
           "communityDependencies": [],
@@ -3580,7 +4070,16 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/nbacc_ray97/nbacc_ray97.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -3601,7 +4100,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/nbacg_guer01/nbacg_guer01.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -3617,6 +4127,22 @@
       ],
       "tags": [],
       "modules": [
+        {
+          "path": "specifications/spanning/MC_spanning.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/spanning/MC_spanning.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "safety failure"
+            }
+          ]
+        },
         {
           "path": "specifications/spanning/spanning.tla",
           "communityDependencies": [],
@@ -3638,6 +4164,22 @@
         "beginner"
       ],
       "modules": [
+        {
+          "path": "specifications/sums_even/MC_sums_even.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/sums_even/MC_sums_even.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/sums_even/TLAPS.tla",
           "communityDependencies": [],
@@ -3740,21 +4282,50 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/transaction_commit/PaxosCommit.cfg",
+              "runtime": "00:00:30",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/transaction_commit/TCommit.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/transaction_commit/TCommit.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock"
+              ],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/transaction_commit/TwoPhase.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/transaction_commit/TwoPhase.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     }
diff --git a/specifications/Bakery-Boulangerie/MCBakery.cfg b/specifications/Bakery-Boulangerie/MCBakery.cfg
new file mode 100644
index 00000000..b0af6112
--- /dev/null
+++ b/specifications/Bakery-Boulangerie/MCBakery.cfg
@@ -0,0 +1,10 @@
+CONSTANT
+  N = 2
+  MaxNat = 2
+  Nat <- NatOverride
+INVARIANTS MutualExclusion TypeOK Inv
+\* https://github.com/tlaplus/Examples/issues/109
+\*PROPERTIES DeadlockFree StarvationFree
+SPECIFICATION ISpec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/Bakery-Boulangerie/MCBakery.tla b/specifications/Bakery-Boulangerie/MCBakery.tla
new file mode 100644
index 00000000..d9f40ecf
--- /dev/null
+++ b/specifications/Bakery-Boulangerie/MCBakery.tla
@@ -0,0 +1,7 @@
+---------------------------- MODULE MCBakery --------------------------------
+EXTENDS Bakery
+CONSTANT MaxNat
+ASSUME MaxNat \in Nat
+NatOverride == 0 .. MaxNat
+=============================================================================
+
diff --git a/specifications/Bakery-Boulangerie/MCBoulanger.cfg b/specifications/Bakery-Boulangerie/MCBoulanger.cfg
new file mode 100644
index 00000000..5aae39a3
--- /dev/null
+++ b/specifications/Bakery-Boulangerie/MCBoulanger.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 3
+  MaxNat = 3
+  Nat <- NatOverride
+INVARIANTS MutualExclusion TypeOK Inv
+SPECIFICATION Spec
+CONSTRAINT StateConstraint
+
diff --git a/specifications/Bakery-Boulangerie/MCBoulanger.tla b/specifications/Bakery-Boulangerie/MCBoulanger.tla
new file mode 100644
index 00000000..a3c6142d
--- /dev/null
+++ b/specifications/Bakery-Boulangerie/MCBoulanger.tla
@@ -0,0 +1,8 @@
+--------------------------- MODULE MCBoulanger ------------------------------
+EXTENDS Boulanger
+CONSTANT MaxNat
+ASSUME MaxNat \in Nat
+NatOverride == 0 .. MaxNat
+StateConstraint == \A process \in Procs : num[process] < MaxNat
+=============================================================================
+
diff --git a/specifications/Chameneos/Chameneos.cfg b/specifications/Chameneos/Chameneos.cfg
new file mode 100644
index 00000000..82980ea0
--- /dev/null
+++ b/specifications/Chameneos/Chameneos.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  N = 4
+  M = 4
+  Faded = Faded
+  MeetingPlaceEmpty = MeetingPlaceEmpty
+INVARIANTS TypeOK SumMet
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/CigaretteSmokers/CigaretteSmokers.cfg b/specifications/CigaretteSmokers/CigaretteSmokers.cfg
new file mode 100644
index 00000000..b568ea64
--- /dev/null
+++ b/specifications/CigaretteSmokers/CigaretteSmokers.cfg
@@ -0,0 +1,6 @@
+CONSTANTS
+  Ingredients = {matches, paper, tobacco}
+  Offers = {{matches, paper}, {matches, tobacco}, {paper, tobacco}}
+INVARIANTS TypeOK AtMostOne
+SPECIFICATION Spec
+
diff --git a/specifications/CigaretteSmokers/CigaretteSmokers.tla b/specifications/CigaretteSmokers/CigaretteSmokers.tla
index ef52e04d..e4794de8 100644
--- a/specifications/CigaretteSmokers/CigaretteSmokers.tla
+++ b/specifications/CigaretteSmokers/CigaretteSmokers.tla
@@ -12,7 +12,7 @@ VARIABLE smokers, dealer
 (***************************************************************************)
 (* 'Ingredients' is a set of ingredients, originally                       *)
 (* {matches, paper, tobacco}. 'Offers' is a subset of subsets of           *)
-(* ingredients, each missing just one ingriedent                           *)
+(* ingredients, each missing just one ingredient                           *)
 (***************************************************************************)
 ASSUME /\ Offers \subseteq (SUBSET Ingredients)
        /\ \A n \in Offers : Cardinality(n) = Cardinality(Ingredients) - 1
diff --git a/specifications/GameOfLife/GameOfLife.cfg b/specifications/GameOfLife/GameOfLife.cfg
new file mode 100644
index 00000000..521c6e6a
--- /dev/null
+++ b/specifications/GameOfLife/GameOfLife.cfg
@@ -0,0 +1,4 @@
+CONSTANT N = 4
+INVARIANT TypeOK
+SPECIFICATION Spec
+
diff --git a/specifications/LoopInvariance/MCBinarySearch.cfg b/specifications/LoopInvariance/MCBinarySearch.cfg
new file mode 100644
index 00000000..5b46fac3
--- /dev/null
+++ b/specifications/LoopInvariance/MCBinarySearch.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  Values = {1,2,3,4,5}
+  MaxSeqLen = 8
+  Seq <- LimitedSeq
+INVARIANTS resultCorrect TypeOK Inv
+PROPERTY Termination
+SPECIFICATION Spec
+
diff --git a/specifications/LoopInvariance/MCBinarySearch.tla b/specifications/LoopInvariance/MCBinarySearch.tla
new file mode 100644
index 00000000..1a1b63dd
--- /dev/null
+++ b/specifications/LoopInvariance/MCBinarySearch.tla
@@ -0,0 +1,7 @@
+--------------------------- MODULE MCBinarySearch ---------------------------
+EXTENDS BinarySearch
+CONSTANT MaxSeqLen
+ASSUME MaxSeqLen \in Nat
+LimitedSeq(S) == UNION {[1 .. n -> S] : n \in 1 .. MaxSeqLen}
+=============================================================================
+
diff --git a/specifications/LoopInvariance/MCQuicksort.cfg b/specifications/LoopInvariance/MCQuicksort.cfg
new file mode 100644
index 00000000..bd23c2be
--- /dev/null
+++ b/specifications/LoopInvariance/MCQuicksort.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  Values = {1,2,3}
+  MaxSeqLen = 4
+  Seq <- LimitedSeq
+INVARIANTS PCorrect TypeOK Inv
+PROPERTY Termination
+SPECIFICATION Spec
+
diff --git a/specifications/LoopInvariance/MCQuicksort.tla b/specifications/LoopInvariance/MCQuicksort.tla
new file mode 100644
index 00000000..e3f5d31f
--- /dev/null
+++ b/specifications/LoopInvariance/MCQuicksort.tla
@@ -0,0 +1,7 @@
+---------------------------- MODULE MCQuicksort -----------------------------
+EXTENDS Quicksort
+CONSTANT MaxSeqLen
+ASSUME MaxSeqLen \in Nat
+LimitedSeq(S) == UNION {[1 .. n -> S] : n \in 1 .. MaxSeqLen}
+=============================================================================
+
diff --git a/specifications/MisraReachability/MCParReach.cfg b/specifications/MisraReachability/MCParReach.cfg
new file mode 100644
index 00000000..7c58b89e
--- /dev/null
+++ b/specifications/MisraReachability/MCParReach.cfg
@@ -0,0 +1,10 @@
+CONSTANTS
+  Nodes = {n1, n2, n3, n4}
+  Root = n1
+  Procs = {p1, p2}
+  Succ <- ConnectedToSomeButNotAll
+  Seq <- LimitedSeq
+INVARIANT Inv
+PROPERTY Refines
+SPECIFICATION Spec
+
diff --git a/specifications/MisraReachability/MCParReach.tla b/specifications/MisraReachability/MCParReach.tla
new file mode 100644
index 00000000..a519a154
--- /dev/null
+++ b/specifications/MisraReachability/MCParReach.tla
@@ -0,0 +1,14 @@
+---- MODULE MCParReach ----
+EXTENDS ParReach
+
+ConnectedToSomeButNotAll ==
+  CHOOSE succ \in [Nodes -> SUBSET Nodes]
+  : \A n \in Nodes : Cardinality(succ[n]) = 2
+
+LimitedSeq(S) == UNION {
+  [1 .. len -> S]
+  : len \in 0 .. Cardinality(Nodes)
+}
+
+============================
+
diff --git a/specifications/MisraReachability/MCReachabilityTest.tla b/specifications/MisraReachability/MCReachabilityTest.tla
new file mode 100644
index 00000000..96ebeb00
--- /dev/null
+++ b/specifications/MisraReachability/MCReachabilityTest.tla
@@ -0,0 +1,15 @@
+---- MODULE MCReachabilityTest ----
+EXTENDS ReachabilityTest, Sequences
+
+CONSTANT RandomSuccCount
+
+RandomSuccSet == SuccSet2(RandomSuccCount)
+
+ASSUME \A i \in DOMAIN Test : Test[i]
+
+LimitedSeq(S) == UNION {
+  [1 .. len -> S]
+  : len \in 0 .. Cardinality(Nodes)
+}
+===================================
+
diff --git a/specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg b/specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg
new file mode 100644
index 00000000..7c117757
--- /dev/null
+++ b/specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg
@@ -0,0 +1,6 @@
+CONSTANTS
+  RandomSuccCount = 0
+  Nodes = {n1, n2, n3}
+  SuccSet <- SuccSet1
+  Seq <- LimitedSeq
+
diff --git a/specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg b/specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg
new file mode 100644
index 00000000..da2eb976
--- /dev/null
+++ b/specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg
@@ -0,0 +1,6 @@
+CONSTANTS
+  RandomSuccCount = 5
+  Nodes = {n1, n2, n3, n4}
+  SuccSet <- RandomSuccSet
+  Seq <- LimitedSeq
+
diff --git a/specifications/MisraReachability/MCReachable.cfg b/specifications/MisraReachability/MCReachable.cfg
new file mode 100644
index 00000000..efe6ec30
--- /dev/null
+++ b/specifications/MisraReachability/MCReachable.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  Nodes = {n1, n2, n3, n4}
+  Root = n1
+  Succ <- ConnectedToSomeButNotAll
+  Seq <- LimitedSeq
+INVARIANTS TypeOK Inv1 Inv2 Inv3 PartialCorrectness
+PROPERTY Termination
+SPECIFICATION Spec
+
diff --git a/specifications/MisraReachability/MCReachable.tla b/specifications/MisraReachability/MCReachable.tla
new file mode 100644
index 00000000..79048427
--- /dev/null
+++ b/specifications/MisraReachability/MCReachable.tla
@@ -0,0 +1,14 @@
+---- MODULE MCReachable ----
+EXTENDS Reachable
+
+ConnectedToSomeButNotAll ==
+  CHOOSE succ \in [Nodes -> SUBSET Nodes]
+  : \A n \in Nodes : Cardinality(succ[n]) = 2
+
+LimitedSeq(S) == UNION {
+  [1 .. len -> S]
+  : len \in 0 .. Cardinality(Nodes)
+}
+
+============================
+
diff --git a/specifications/MisraReachability/ParReach.tla b/specifications/MisraReachability/ParReach.tla
index 2a809a35..3d9e8e8c 100644
--- a/specifications/MisraReachability/ParReach.tla
+++ b/specifications/MisraReachability/ParReach.tla
@@ -216,7 +216,8 @@ R == INSTANCE Reachable WITH vroot <- vrootBar, pc <- pcBar
 (* it, use models with behavior specification spec that check the temporal *)
 (* property R!Spec.)                                                       *)
 (***************************************************************************)
-THEOREM Spec => R!Spec       
+Refines == R!Spec
+THEOREM Spec => Refines
 
 (***************************************************************************)
 (* By the definition of formula Spec of module Reachable, this theorem     *)
diff --git a/specifications/MisraReachability/Reachable.tla b/specifications/MisraReachability/Reachable.tla
index eeeb697e..1774d908 100644
--- a/specifications/MisraReachability/Reachable.tla
+++ b/specifications/MisraReachability/Reachable.tla
@@ -190,7 +190,8 @@ Inv3 == Reachable = marked \cup ReachableFrom(vroot)
 (* then `marked' equals Reachable.  The algorithm has terminated when pc   *)
 (* equals "Done", so this theorem asserts partial correctness.             *)
 (***************************************************************************)
-THEOREM Spec => []((pc = "Done") => (marked = Reachable)) 
+PartialCorrectness == (pc = "Done") => (marked = Reachable)
+THEOREM Spec => []PartialCorrectness
   (*************************************************************************)
   (* TypeOK implies (pc = "Done") => (vroot = {}).  Since,                 *)
   (* ReachableFrom({}) equals {}, Inv3 implies                             *)
diff --git a/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg b/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg
new file mode 100644
index 00000000..cd8b671b
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg
@@ -0,0 +1,17 @@
+\* MV CONSTANT declarations
+CONSTANTS
+a = a
+b = b
+c = c
+\* MV CONSTANT definitions
+CONSTANT
+Value <- const_156017750645611000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+Inv
+\* Generated on Mon Jun 10 07:38:26 PDT 2019
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/PaxosHowToWinATuringAward/MCConsensus.tla b/specifications/PaxosHowToWinATuringAward/MCConsensus.tla
new file mode 100644
index 00000000..3a343f8a
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCConsensus.tla
@@ -0,0 +1,16 @@
+---- MODULE MCConsensus ----
+EXTENDS Consensus, TLC
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+a, b, c
+----
+
+\* MV CONSTANT definitions Value
+const_156017750645611000 == 
+{a, b, c}
+----
+
+=============================================================================
+\* Modification History
+\* Created Mon Jun 10 07:38:26 PDT 2019 by lamport
diff --git a/specifications/PaxosHowToWinATuringAward/MCPaxos.tla b/specifications/PaxosHowToWinATuringAward/MCPaxos.tla
new file mode 100644
index 00000000..09e3d3c9
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCPaxos.tla
@@ -0,0 +1,45 @@
+---- MODULE MCPaxos ----
+EXTENDS Paxos, TLC
+
+CONSTANT MaxBallot
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+a1, a2, a3
+----
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+v1, v2
+----
+
+\* MV CONSTANT definitions Acceptor
+const_1560336937634605000 == 
+{a1, a2, a3}
+----
+
+\* MV CONSTANT definitions Value
+const_1560336937634606000 == 
+{v1, v2}
+----
+
+\* CONSTANT definitions @modelParameterConstants:1Quorum
+const_1560336937634607000 == 
+{{a1, a2}, {a1, a3}, {a2, a3}}
+----
+
+\* CONSTANT definition @modelParameterDefinitions:1
+def_ov_1560336937634609000 ==
+0..MaxBallot
+----
+\* CONSTANT definition @modelParameterDefinitions:2
+def_ov_1560336937634610000 ==
+0..MaxBallot
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1560336937635612000 ==
+V!Spec
+----
+=============================================================================
+\* Modification History
+\* Created Wed Jun 12 03:55:37 PDT 2019 by lamport
diff --git a/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg b/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg
new file mode 100644
index 00000000..53a0208c
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg
@@ -0,0 +1,35 @@
+\* MV CONSTANT declarations
+CONSTANT
+MaxBallot = 2
+CONSTANTS
+a1 = a1
+a2 = a2
+a3 = a3
+\* MV CONSTANT declarations
+CONSTANTS
+v1 = v1
+v2 = v2
+\* MV CONSTANT definitions
+CONSTANT
+Acceptor <- const_1560336937634605000
+\* MV CONSTANT definitions
+CONSTANT
+Value <- const_1560336937634606000
+\* CONSTANT definitions
+CONSTANT
+Quorum <- const_1560336937634607000
+\* CONSTANT definition
+CONSTANT
+None = None
+Ballot <- def_ov_1560336937634609000
+Ballot <- [Voting]def_ov_1560336937634610000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+Inv
+\* PROPERTY definition
+PROPERTY
+prop_1560336937635612000
+\* Generated on Wed Jun 12 03:55:37 PDT 2019
diff --git a/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg b/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg
new file mode 100644
index 00000000..520e0d69
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg
@@ -0,0 +1,35 @@
+\* MV CONSTANT declarations
+CONSTANT
+MaxBallot = 1
+CONSTANTS
+a1 = a1
+a2 = a2
+a3 = a3
+\* MV CONSTANT declarations
+CONSTANTS
+v1 = v1
+v2 = v2
+\* MV CONSTANT definitions
+CONSTANT
+Acceptor <- const_1560336937634605000
+\* MV CONSTANT definitions
+CONSTANT
+Value <- const_1560336937634606000
+\* CONSTANT definitions
+CONSTANT
+Quorum <- const_1560336937634607000
+\* CONSTANT definition
+CONSTANT
+None = None
+Ballot <- def_ov_1560336937634609000
+Ballot <- [Voting]def_ov_1560336937634610000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+Inv
+\* PROPERTY definition
+PROPERTY
+prop_1560336937635612000
+\* Generated on Wed Jun 12 03:55:37 PDT 2019
diff --git a/specifications/PaxosHowToWinATuringAward/MCVoting.cfg b/specifications/PaxosHowToWinATuringAward/MCVoting.cfg
new file mode 100644
index 00000000..05eeacc6
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCVoting.cfg
@@ -0,0 +1,33 @@
+\* MV CONSTANT declarations
+CONSTANTS
+a1 = a1
+a2 = a2
+a3 = a3
+\* MV CONSTANT declarations
+CONSTANTS
+v1 = v1
+v2 = v2
+\* MV CONSTANT definitions
+CONSTANT
+Acceptor <- const_156180051387243000
+\* MV CONSTANT definitions
+CONSTANT
+Value <- const_156180051387244000
+\* CONSTANT definitions
+CONSTANT
+Quorum <- const_156180051387245000
+\* CONSTANT definition
+CONSTANT
+Ballot <- def_ov_156180051387246000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+Inv
+\* PROPERTY definition
+PROPERTY
+prop_156180051387248000
+\* Generated on Sat Jun 29 02:28:33 PDT 2019
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/PaxosHowToWinATuringAward/MCVoting.tla b/specifications/PaxosHowToWinATuringAward/MCVoting.tla
new file mode 100644
index 00000000..1e61ffe9
--- /dev/null
+++ b/specifications/PaxosHowToWinATuringAward/MCVoting.tla
@@ -0,0 +1,39 @@
+---- MODULE MCVoting ----
+EXTENDS Voting, TLC
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+a1, a2, a3
+----
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+v1, v2
+----
+
+\* MV CONSTANT definitions Acceptor
+const_156180051387243000 == 
+{a1, a2, a3}
+----
+
+\* MV CONSTANT definitions Value
+const_156180051387244000 == 
+{v1, v2}
+----
+
+\* CONSTANT definitions @modelParameterConstants:2Quorum
+const_156180051387245000 == 
+{{a1, a2}, {a1, a3}, {a2, a3}}
+----
+
+\* CONSTANT definition @modelParameterDefinitions:0
+def_ov_156180051387246000 ==
+0..2
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_156180051387248000 ==
+C!Spec
+----
+=============================================================================
+\* Modification History
+\* Created Sat Jun 29 02:28:33 PDT 2019 by lamport
diff --git a/specifications/SpanningTree/SpanTree.cfg b/specifications/SpanningTree/SpanTree.cfg
new file mode 100644
index 00000000..36a00d29
--- /dev/null
+++ b/specifications/SpanningTree/SpanTree.cfg
@@ -0,0 +1,10 @@
+CONSTANTS
+  Nodes = {n1, n2, n3, n4, n5}
+  Edges = {{n1, n2}, {n1, n3}, {n2, n3}, {n2, n4}, {n3, n4}, {n3, n5}, {n4, n5}}
+  MaxCardinality = 6
+  Root = n1
+INVARIANT TypeOK
+PROPERTIES Liveness Safety
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/SpanningTree/SpanTreeRandom.cfg b/specifications/SpanningTree/SpanTreeRandom.cfg
new file mode 100644
index 00000000..70862f02
--- /dev/null
+++ b/specifications/SpanningTree/SpanTreeRandom.cfg
@@ -0,0 +1,10 @@
+CONSTANTS
+  Nodes = {n1, n2, n3, n4, n5, n6}
+  MaxCardinality = 6
+  Root = n1
+INVARIANT TypeOK
+\* https://github.com/tlaplus/tlaplus/issues/866
+\*PROPERTY Liveness Safety
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/SpanningTree/SpanTreeTest4Nodes.cfg b/specifications/SpanningTree/SpanTreeTest4Nodes.cfg
new file mode 100644
index 00000000..c1bf5c58
--- /dev/null
+++ b/specifications/SpanningTree/SpanTreeTest4Nodes.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  Nodes = {n1, n2, n3, n4}
+  MaxCardinality = 5
+  Root = n1
+INVARIANT TypeOK
+PROPERTIES Liveness Safety
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/SpanningTree/SpanTreeTest5Nodes.cfg b/specifications/SpanningTree/SpanTreeTest5Nodes.cfg
new file mode 100644
index 00000000..d68ffd09
--- /dev/null
+++ b/specifications/SpanningTree/SpanTreeTest5Nodes.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  Nodes = {n1, n2, n3, n4, n5}
+  MaxCardinality = 5
+  Root = n1
+INVARIANT TypeOK
+PROPERTIES Liveness Safety
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/Stones/Stones.cfg b/specifications/Stones/Stones.cfg
new file mode 100644
index 00000000..51c16a85
--- /dev/null
+++ b/specifications/Stones/Stones.cfg
@@ -0,0 +1,4 @@
+CONSTANTS
+  W = 40
+  N = 4
+
diff --git a/specifications/TeachingConcurrency/Simple.cfg b/specifications/TeachingConcurrency/Simple.cfg
new file mode 100644
index 00000000..8372dbb5
--- /dev/null
+++ b/specifications/TeachingConcurrency/Simple.cfg
@@ -0,0 +1,4 @@
+CONSTANT N = 5
+SPECIFICATION Spec
+INVARIANTS PCorrect TypeOK Inv
+
diff --git a/specifications/TeachingConcurrency/SimpleRegular.cfg b/specifications/TeachingConcurrency/SimpleRegular.cfg
new file mode 100644
index 00000000..a3d615fd
--- /dev/null
+++ b/specifications/TeachingConcurrency/SimpleRegular.cfg
@@ -0,0 +1,4 @@
+CONSTANT N = 8 
+SPECIFICATION Spec
+INVARIANTS PCorrect TypeOK Inv
+
diff --git a/specifications/TwoPhase/MCTwoPhase.cfg b/specifications/TwoPhase/MCTwoPhase.cfg
new file mode 100644
index 00000000..ceec4fe0
--- /dev/null
+++ b/specifications/TwoPhase/MCTwoPhase.cfg
@@ -0,0 +1,3 @@
+INVARIANT Inv
+SPECIFICATION Spec
+
diff --git a/specifications/TwoPhase/MCTwoPhase.tla b/specifications/TwoPhase/MCTwoPhase.tla
new file mode 100644
index 00000000..15bb9827
--- /dev/null
+++ b/specifications/TwoPhase/MCTwoPhase.tla
@@ -0,0 +1,7 @@
+----------------------------- MODULE MCTwoPhase -----------------------------
+XInit(v) == v = 0
+XAct(i, xInit, xNext) == xNext = xInit
+VARIABLES p, c, x
+INSTANCE TwoPhase
+=============================================================================
+
diff --git a/specifications/aba-asyn-byz/aba_asyn_byz.cfg b/specifications/aba-asyn-byz/aba_asyn_byz.cfg
new file mode 100644
index 00000000..bfc4bce7
--- /dev/null
+++ b/specifications/aba-asyn-byz/aba_asyn_byz.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK
+PROPERTIES Unforg_Ltl Corr_Ltl Agreement_Ltl
+SPECIFICATION Spec
+
diff --git a/specifications/bcastByz/bcastByz.cfg b/specifications/bcastByz/bcastByz.cfg
new file mode 100644
index 00000000..581bb993
--- /dev/null
+++ b/specifications/bcastByz/bcastByz.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK FCConstraints
+PROPERTIES CorrLtl RelayLtl UnforgLtl
+SPECIFICATION Spec
+
diff --git a/specifications/bcastByz/bcastByzNoBcast.cfg b/specifications/bcastByz/bcastByzNoBcast.cfg
new file mode 100644
index 00000000..f7a5ab49
--- /dev/null
+++ b/specifications/bcastByz/bcastByzNoBcast.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 10
+  T = 3
+  F = 2
+INVARIANTS TypeOK FCConstraints Unforg
+PROPERTIES CorrLtl RelayLtl
+SPECIFICATION SpecNoBcast
+
diff --git a/specifications/bcastFolklore/bcastFolklore.cfg b/specifications/bcastFolklore/bcastFolklore.cfg
new file mode 100644
index 00000000..5371d27c
--- /dev/null
+++ b/specifications/bcastFolklore/bcastFolklore.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK
+PROPERTIES UnforgLtl CorrLtl RelayLtl ReliableChan
+SPECIFICATION Spec
+
diff --git a/specifications/bosco/bosco.cfg b/specifications/bosco/bosco.cfg
new file mode 100644
index 00000000..30694dce
--- /dev/null
+++ b/specifications/bosco/bosco.cfg
@@ -0,0 +1,7 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK Lemma3_0 Lemma3_1 Lemma4_0 Lemma4_1
+SPECIFICATION Spec
+
diff --git a/specifications/c1cs/c1cs.cfg b/specifications/c1cs/c1cs.cfg
new file mode 100644
index 00000000..35c98675
--- /dev/null
+++ b/specifications/c1cs/c1cs.cfg
@@ -0,0 +1,10 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+  Values = {v1, v2}
+  Bottom = Bottom
+INVARIANTS TypeOK Validity Agreement WeakAgreement IndStrengthens
+PROPERTIES Termination
+SPECIFICATION Spec
+
diff --git a/specifications/cf1s-folklore/cf1s_folklore.cfg b/specifications/cf1s-folklore/cf1s_folklore.cfg
new file mode 100644
index 00000000..b8874992
--- /dev/null
+++ b/specifications/cf1s-folklore/cf1s_folklore.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK
+PROPERTIES OneStep0_Ltl OneStep1_Ltl
+SPECIFICATION Spec
+
diff --git a/specifications/cf1s-folklore/cf1s_folklore.tla b/specifications/cf1s-folklore/cf1s_folklore.tla
index 8494dcfa..53c2b7aa 100644
--- a/specifications/cf1s-folklore/cf1s_folklore.tla
+++ b/specifications/cf1s-folklore/cf1s_folklore.tla
@@ -150,9 +150,7 @@ OneStep0_Ltl ==
 (* If all processes propose 1, then every process crashes or decides 1. *)
 OneStep1_Ltl ==  
   (\A i \in Proc : pc[i] = "V1") => <>(\A i \in Proc : pc[i] # "U0" /\ pc[i] # "U1" /\ pc[i] # "D0")
-  
-         
-
+ 
 =============================================================================
 \* Modification History
 \* Last modified Mon Jul 09 13:26:59 CEST 2018 by tthai
diff --git a/specifications/chang_roberts/MCChangRoberts.cfg b/specifications/chang_roberts/MCChangRoberts.cfg
new file mode 100644
index 00000000..a2f9cfcf
--- /dev/null
+++ b/specifications/chang_roberts/MCChangRoberts.cfg
@@ -0,0 +1,6 @@
+CONSTANT N = 3
+INVARIANTS TypeOK Correctness
+PROPERTY Liveness
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/chang_roberts/MCChangRoberts.tla b/specifications/chang_roberts/MCChangRoberts.tla
new file mode 100644
index 00000000..b7796615
--- /dev/null
+++ b/specifications/chang_roberts/MCChangRoberts.tla
@@ -0,0 +1,9 @@
+--------------------------- MODULE MCChangRoberts ---------------------------
+EXTENDS Naturals
+CONSTANT N
+VARIABLES msgs, pc, initiator, state
+ASSUME N \in Nat
+Id == [i \in 1 .. N |-> i]
+INSTANCE ChangRoberts
+=============================================================================
+
diff --git a/specifications/detector_chan96/EnvironmentController.cfg b/specifications/detector_chan96/EnvironmentController.cfg
new file mode 100644
index 00000000..43202d46
--- /dev/null
+++ b/specifications/detector_chan96/EnvironmentController.cfg
@@ -0,0 +1,12 @@
+CONSTANTS
+  N = 3
+  T = 1
+  d0 = 2
+  SendPoint = 2
+  PredictPoint = 3
+  DELTA = 1
+  PHI = 1
+INVARIANT TypeOK
+PROPERTIES StrongCompleteness EventuallyStrongAccuracy
+SPECIFICATION Spec
+
diff --git a/specifications/detector_chan96/EnvironmentController.tla b/specifications/detector_chan96/EnvironmentController.tla
index c3e32f78..0a7fe234 100644
--- a/specifications/detector_chan96/EnvironmentController.tla
+++ b/specifications/detector_chan96/EnvironmentController.tla
@@ -1,6 +1,6 @@
 ----------------------- MODULE EnvironmentController -----------------------
 
-(* An encoding of a parameterized and partially syncrhonous model of the eventually  
+(* An encoding of a parameterized and partially synchronous model of the eventually  
    perfect failure detectors with crash faults from:
   
    [1] Chandra, Tushar Deepak, and Sam Toueg. "Unreliable failure detectors for 
@@ -87,7 +87,7 @@
         TLC spends more than 2 hours (from 11:17 to 13:26) verifying these properties.
       
    o PROBLEMS with TLC: I believe that PHIConstraint and PHIConstraint1 are equivalent. 
-     However, whenever I check this specification with PHIConstraing1, TLC shows an 
+     However, whenever I check this specification with PHIConstraint1, TLC shows an 
      error: "Too many possible next states for the last state in the trace." I guess 
      that the reasons are from optimizations for disjunctions. *)   
 
diff --git a/specifications/diskpaxos/MC_HDiskSynod.cfg b/specifications/diskpaxos/MC_HDiskSynod.cfg
new file mode 100644
index 00000000..185d4ec5
--- /dev/null
+++ b/specifications/diskpaxos/MC_HDiskSynod.cfg
@@ -0,0 +1,12 @@
+CONSTANTS
+  N = 3
+  Inputs = {in1, in2}
+  NotAnInput = NotAnInput
+  BallotCountPerProcess = 2
+  Ballot <- BallotImpl
+  Disk = {1, 2}
+  IsMajority <- IsMajorityImpl
+INVARIANTS HInv1 HInv2 HInv3 HInv4 HInv6
+INIT HInit
+NEXT HNext
+
diff --git a/specifications/diskpaxos/MC_HDiskSynod.tla b/specifications/diskpaxos/MC_HDiskSynod.tla
new file mode 100644
index 00000000..0a6bad4e
--- /dev/null
+++ b/specifications/diskpaxos/MC_HDiskSynod.tla
@@ -0,0 +1,9 @@
+---- MODULE MC_HDiskSynod ----
+EXTENDS HDiskSynod, TLC
+CONSTANT BallotCountPerProcess
+BallotImpl(p) ==
+  LET start == p * BallotCountPerProcess IN
+  start .. (start + BallotCountPerProcess - 1)
+IsMajorityImpl(s) == Cardinality(s) * 2 > N
+==============================
+
diff --git a/specifications/glowingRaccoon/clean.cfg b/specifications/glowingRaccoon/clean.cfg
new file mode 100644
index 00000000..bff77506
--- /dev/null
+++ b/specifications/glowingRaccoon/clean.cfg
@@ -0,0 +1,7 @@
+CONSTANTS
+  DNA = 5
+  PRIMER = 5
+INVARIANTS TypeOK primerPositive preservationInvariant
+PROPERTY preservationProperty
+SPECIFICATION Spec
+
diff --git a/specifications/glowingRaccoon/product.cfg b/specifications/glowingRaccoon/product.cfg
new file mode 100644
index 00000000..4da41249
--- /dev/null
+++ b/specifications/glowingRaccoon/product.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  DNA = 5
+  PRIMER = 5
+INVARIANTS TypeOK thirdCycleProduct
+PROPERTIES stagesSpec primerDepleted
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/glowingRaccoon/stages.cfg b/specifications/glowingRaccoon/stages.cfg
new file mode 100644
index 00000000..30194aae
--- /dev/null
+++ b/specifications/glowingRaccoon/stages.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  DNA = 5
+  PRIMER = 5
+INVARIANT TypeOK
+SPECIFICATION Spec
+PROPERTIES cleanSpec primerDepleted
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/lamport_mutex/MCLamportMutex.cfg b/specifications/lamport_mutex/MCLamportMutex.cfg
new file mode 100644
index 00000000..2d47c2cf
--- /dev/null
+++ b/specifications/lamport_mutex/MCLamportMutex.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  N = 3
+  MaxNat = 7
+  maxClock = 6
+  Nat <- NatOverride
+INVARIANTS TypeOK BoundedNetwork Mutex
+SPECIFICATION Spec
+CONSTRAINT ClockConstraint
+
diff --git a/specifications/lamport_mutex/MCLamportMutex.tla b/specifications/lamport_mutex/MCLamportMutex.tla
new file mode 100644
index 00000000..e385e0f5
--- /dev/null
+++ b/specifications/lamport_mutex/MCLamportMutex.tla
@@ -0,0 +1,7 @@
+--------------------------- MODULE MCLamportMutex ---------------------------
+EXTENDS LamportMutex
+CONSTANT MaxNat
+ASSUME MaxNat \in Nat
+NatOverride == 0 .. MaxNat
+=============================================================================
+
diff --git a/specifications/nbacc_ray97/nbacc_ray97.cfg b/specifications/nbacc_ray97/nbacc_ray97.cfg
new file mode 100644
index 00000000..0b5e4e0f
--- /dev/null
+++ b/specifications/nbacc_ray97/nbacc_ray97.cfg
@@ -0,0 +1,4 @@
+CONSTANT N = 2
+INVARIANT TypeOK
+SPECIFICATION Spec
+
diff --git a/specifications/nbacg_guer01/nbacg_guer01.cfg b/specifications/nbacg_guer01/nbacg_guer01.cfg
new file mode 100644
index 00000000..061169d8
--- /dev/null
+++ b/specifications/nbacg_guer01/nbacg_guer01.cfg
@@ -0,0 +1,5 @@
+CONSTANT N = 3
+INVARIANT TypeOK
+PROPERTIES AgrrLtl AbortValidityLtl CommitValidityLtl TerminationLtl
+SPECIFICATION Spec
+
diff --git a/specifications/spanning/MC_spanning.cfg b/specifications/spanning/MC_spanning.cfg
new file mode 100644
index 00000000..dbfa8935
--- /dev/null
+++ b/specifications/spanning/MC_spanning.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  Proc = {1, 2, 3}
+  NoPrnt =  NoPrnt
+  root = 1
+  nbrs <- Neighbors
+INVARIANTS TypeOK SntMsg
+\*PROPERTIES Termination OneParent
+SPECIFICATION Spec
+
diff --git a/specifications/spanning/MC_spanning.tla b/specifications/spanning/MC_spanning.tla
new file mode 100644
index 00000000..c969b1d8
--- /dev/null
+++ b/specifications/spanning/MC_spanning.tla
@@ -0,0 +1,4 @@
+---- MODULE MC_spanning ----
+EXTENDS spanning
+Neighbors == {<<1, 2>>, <<1, 3>>}
+============================
diff --git a/specifications/spanning/spanning.tla b/specifications/spanning/spanning.tla
index 39fb8b6c..ec92d36a 100644
--- a/specifications/spanning/spanning.tla
+++ b/specifications/spanning/spanning.tla
@@ -45,4 +45,4 @@ SntMsg == \A i \in Proc: (i # root /\ prnt[i] = NoPrnt => \A j \in Proc: <<i ,j>
 
 =============================================================================
 \* Modification History
-\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai
\ No newline at end of file
+\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai
diff --git a/specifications/sums_even/MC_sums_even.cfg b/specifications/sums_even/MC_sums_even.cfg
new file mode 100644
index 00000000..1969570a
--- /dev/null
+++ b/specifications/sums_even/MC_sums_even.cfg
@@ -0,0 +1,4 @@
+CONSTANT
+  MaxNat = 1000000
+  Nat <- NatOverride
+
diff --git a/specifications/sums_even/MC_sums_even.tla b/specifications/sums_even/MC_sums_even.tla
new file mode 100644
index 00000000..fe79a735
--- /dev/null
+++ b/specifications/sums_even/MC_sums_even.tla
@@ -0,0 +1,8 @@
+------------------------ MODULE MC_sums_even -----------------------
+EXTENDS sums_even
+CONSTANT MaxNat
+ASSUME MaxNat \in Nat
+NatOverride == 0 .. MaxNat
+ASSUME T1
+====================================================================
+
diff --git a/specifications/transaction_commit/PaxosCommit.cfg b/specifications/transaction_commit/PaxosCommit.cfg
new file mode 100644
index 00000000..aa4ba0a8
--- /dev/null
+++ b/specifications/transaction_commit/PaxosCommit.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  RM = {r1, r2}
+  Acceptor = {a1, a2, a3}
+  Majority = {{a1, a2}, {a1, a3}, {a2, a3}}
+  Ballot = {0,1}
+INVARIANT PCTypeOK
+SPECIFICATION PCSpec
+
diff --git a/specifications/transaction_commit/TCommit.cfg b/specifications/transaction_commit/TCommit.cfg
new file mode 100644
index 00000000..62f56f2e
--- /dev/null
+++ b/specifications/transaction_commit/TCommit.cfg
@@ -0,0 +1,5 @@
+CONSTANT RM = {r1, r2, r3}
+INVARIANTS TCTypeOK TCConsistent
+SPECIFICATION TCSpec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/transaction_commit/TwoPhase.cfg b/specifications/transaction_commit/TwoPhase.cfg
new file mode 100644
index 00000000..5bda57d9
--- /dev/null
+++ b/specifications/transaction_commit/TwoPhase.cfg
@@ -0,0 +1,4 @@
+CONSTANT RM = {r1, r2, r3}
+INVARIANT TPTypeOK
+SPECIFICATION TPSpec
+
