diff --git a/.github/scripts/check_manifest_features.py b/.github/scripts/check_manifest_features.py
index 2b6c2ac0..e65106c7 100644
--- a/.github/scripts/check_manifest_features.py
+++ b/.github/scripts/check_manifest_features.py
@@ -112,7 +112,8 @@ def get_model_features(examples_root, path):
     'Sequences',
     'TLC',
     'TLCExt',
-    'Toolbox'
+    'Toolbox',
+    'Apalache'
 }
 
 # All the standard modules available when using TLAPS
@@ -230,7 +231,6 @@ def check_features(parser, queries, manifest, examples_root):
 if __name__ == '__main__':
     parser = ArgumentParser(description='Checks metadata in tlaplus/examples manifest.json against module and model files in repository.')
     parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
-    parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False)
     args = parser.parse_args()
 
     manifest_path = normpath(args.manifest_path)
diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py
index e213d6c7..999dbf52 100644
--- a/.github/scripts/check_proofs.py
+++ b/.github/scripts/check_proofs.py
@@ -9,26 +9,30 @@
 from timeit import default_timer as timer
 import tla_utils
 
-logging.basicConfig(level=logging.INFO)
-
 parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.')
 parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', 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 .tla modules to skip checking', required=False, default=[])
+parser.add_argument('--only', nargs='+', help='If provided, only check proofs in this space-separated list', required=False, default=[])
+parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
 tlapm_path = normpath(args.tlapm_path)
 manifest_path = normpath(args.manifest_path)
 manifest = tla_utils.load_json(manifest_path)
 examples_root = dirname(manifest_path)
-skip_modules = [normpath(path) for path in args.skip]
+skip_modules = args.skip
+only_modules = args.only
+
+logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 proof_module_paths = [
     module['path']
     for spec in manifest['specifications']
     for module in spec['modules']
         if 'proof' in module['features']
-        and normpath(module['path']) not in skip_modules
+        and module['path'] not in skip_modules
+        and (only_modules == [] or model['path'] in only_models)
 ]
 
 for path in skip_modules:
@@ -45,14 +49,19 @@
         [
             tlapm_path, module_path,
             '-I', module_dir
-        ], capture_output=True
+        ],
+        stdout=subprocess.PIPE,
+        stderr=subprocess.STDOUT,
+        text=True
     )
     end_time = timer()
     logging.info(f'Checked proofs in {end_time - start_time:.1f}s')
     if tlapm.returncode != 0:
         logging.error(f'Proof checking failed in {module_path}:')
-        logging.error(tlapm.stderr.decode('utf-8'))
+        logging.error(tlapm.stdout)
         success = False
+    else:
+        logging.debug(tlapm.stdout)
 
 exit(0 if success else 1)
 
diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py
index f54dc2c7..2171da82 100644
--- a/.github/scripts/check_small_models.py
+++ b/.github/scripts/check_small_models.py
@@ -13,22 +13,25 @@
 
 parser = ArgumentParser(description='Checks all small TLA+ models in the tlaplus/examples repo using TLC.')
 parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)
 parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
 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=[])
+parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
-logging.basicConfig(level=logging.INFO)
+logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 tools_jar_path = normpath(args.tools_jar_path)
+apalache_path = normpath(args.apalache_path)
 tlapm_lib_path = normpath(args.tlapm_lib_path)
 community_jar_path = normpath(args.community_modules_jar_path)
 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]
+skip_models = args.skip
+only_models = args.only
 
 def check_model(module_path, model, expected_runtime):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -38,6 +41,7 @@ def check_model(module_path, model, expected_runtime):
     start_time = timer()
     tlc_result = tla_utils.check_model(
         tools_jar_path,
+        apalache_path,
         module_path,
         model_path,
         tlapm_lib_path,
@@ -46,10 +50,10 @@ def check_model(module_path, model, expected_runtime):
         hard_timeout_in_seconds
     )
     end_time = timer()
+    output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout
     match tlc_result:
         case CompletedProcess():
             logging.info(f'{model_path} in {end_time - start_time:.1f}s vs. {expected_runtime.seconds}s expected')
-            output = ' '.join(tlc_result.args) + '\n' + tlc_result.stdout
             expected_result = model['result']
             actual_result = tla_utils.resolve_tlc_exit_code(tlc_result.returncode)
             if expected_result != actual_result:
@@ -67,10 +71,11 @@ def check_model(module_path, model, expected_runtime):
                     logging.error(f"(distinct/total/depth); expected: {tla_utils.get_state_count_info(model)}, actual: {state_count_info}")
                     logging.error(output)
                     return False
+            logging.debug(output)
             return True
         case TimeoutExpired():
             logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds')
-            logging.error(tlc_result.output.decode('utf-8'))
+            logging.error(output)
             return False
         case _:
             logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}')
@@ -85,8 +90,8 @@ def check_model(module_path, model, expected_runtime):
         for module in spec['modules']
         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)
+            and model['path'] not in skip_models
+            and (only_models == [] or model['path'] in only_models)
     ],
     key = lambda m: m[2],
     reverse=True
diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py
index 7ffd6d1d..008eab2f 100644
--- a/.github/scripts/generate_manifest.py
+++ b/.github/scripts/generate_manifest.py
@@ -167,7 +167,6 @@ def integrate_old_manifest_into_new(old_manifest, new_manifest):
     parser = ArgumentParser(description='Generates a new manifest.json derived from files in the repo.')
     parser.add_argument('--manifest_path', help='Path to the current tlaplus/examples manifest.json file', default='manifest.json')
     parser.add_argument('--ci_ignore_path', help='Path to the CI ignore file', default='.ciignore')
-    parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False)
     args = parser.parse_args()
 
     manifest_path = normpath(args.manifest_path)
diff --git a/.github/scripts/linux-setup.sh b/.github/scripts/linux-setup.sh
index fc5891f5..a6be00a7 100755
--- a/.github/scripts/linux-setup.sh
+++ b/.github/scripts/linux-setup.sh
@@ -40,6 +40,9 @@ main() {
   # Get TLA⁺ tools
   mkdir -p "$DEPS_DIR/tools"
   wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "$DEPS_DIR/tools"
+  # Get Apalache
+  wget -nv https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz -O /tmp/apalache.tgz
+  tar -xzf /tmp/apalache.tgz --directory "$DEPS_DIR"
   # Get TLA⁺ community modules
   mkdir -p "$DEPS_DIR/community"
   wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py
index 1d61ad97..d1cf225d 100644
--- a/.github/scripts/parse_modules.py
+++ b/.github/scripts/parse_modules.py
@@ -6,12 +6,13 @@
 from concurrent.futures import ThreadPoolExecutor
 import logging
 from os import cpu_count
-from os.path import dirname, normpath, pathsep
+from os.path import join, dirname, normpath, pathsep
 import subprocess
 import tla_utils
 
 parser = ArgumentParser(description='Parses all TLA+ modules in the tlaplus/examples repo using SANY.')
 parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)
 parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
 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)
@@ -23,12 +24,13 @@
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 tools_jar_path = normpath(args.tools_jar_path)
+apalache_jar_path = normpath(join(args.apalache_path, 'lib', 'apalache.jar'))
 tlaps_modules = normpath(args.tlapm_lib_path)
 community_modules = normpath(args.community_modules_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
-skip_modules = [normpath(path) for path in args.skip]
-only_modules = [normpath(path) for path in args.only]
+skip_modules = args.skip
+only_modules = args.only
 
 def parse_module(path):
     """
@@ -36,7 +38,13 @@ def parse_module(path):
     """
     logging.info(path)
     # Jar paths must go first
-    search_paths = pathsep.join([tools_jar_path, dirname(path), community_modules, tlaps_modules])
+    search_paths = pathsep.join([
+        tools_jar_path,
+        apalache_jar_path,
+        dirname(path),
+        community_modules,
+        tlaps_modules
+    ])
     sany = subprocess.run([
             'java',
             '-cp', search_paths,
@@ -63,8 +71,8 @@ def parse_module(path):
     tla_utils.from_cwd(examples_root, module['path'])
     for spec in manifest['specifications']
     for module in spec['modules']
-        if normpath(module['path']) not in skip_modules
-        and (only_modules == [] or normpath(module['path']) in only_modules)
+        if module['path'] not in skip_modules
+        and (only_modules == [] or module['path'] in only_modules)
 ]
 
 for path in skip_modules:
diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py
index bcd9d901..d9f0514c 100644
--- a/.github/scripts/smoke_test_large_models.py
+++ b/.github/scripts/smoke_test_large_models.py
@@ -13,18 +13,23 @@
 
 parser = ArgumentParser(description='Smoke-tests all larger TLA+ models in the tlaplus/examples repo using TLC.')
 parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)
 parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
 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=[])
+parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
 tools_jar_path = normpath(args.tools_jar_path)
+apalache_path = normpath(args.apalache_path)
 tlapm_lib_path = normpath(args.tlapm_lib_path)
 community_jar_path = normpath(args.community_modules_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
-skip_models = [normpath(path) for path in args.skip]
+skip_models = args.skip
+only_models = args.only
 
 def check_model(module_path, model):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -33,6 +38,7 @@ def check_model(module_path, model):
     smoke_test_timeout_in_seconds = 5
     tlc_result = tla_utils.check_model(
         tools_jar_path,
+        apalache_path,
         module_path,
         model_path,
         tlapm_lib_path,
@@ -42,6 +48,7 @@ def check_model(module_path, model):
     )
     match tlc_result:
         case TimeoutExpired():
+            logging.debug(tlc_result.stdout)
             return True
         case CompletedProcess():
             logging.warning(f'Model {model_path} finished quickly, within {smoke_test_timeout_in_seconds} seconds; consider labeling it a small model')
@@ -56,7 +63,7 @@ def check_model(module_path, model):
             logging.error(f'Unhandled TLC result type {type(tlc_result)}: {tlc_result}')
             return False
 
-logging.basicConfig(level=logging.INFO)
+logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 manifest = tla_utils.load_json(manifest_path)
 
@@ -66,7 +73,8 @@ def check_model(module_path, model):
     for module in spec['modules']
     for model in module['models']
         if model['size'] != 'small'
-        and normpath(model['path']) not in skip_models
+        and model['path'] not in skip_models
+        and (only_models == [] or model['path'] in only_models)
 ]
 
 for path in skip_models:
diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py
index 73a6430d..cabfe194 100644
--- a/.github/scripts/tla_utils.py
+++ b/.github/scripts/tla_utils.py
@@ -87,37 +87,65 @@ def get_run_mode(mode):
     else:
         raise NotImplementedError(f'Undefined model-check mode {mode}')
 
-def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, hard_timeout_in_seconds):
+def check_model(
+        tools_jar_path,
+        apalache_path,
+        module_path,
+        model_path,
+        tlapm_lib_path,
+        community_jar_path,
+        mode,
+        hard_timeout_in_seconds
+    ):
     """
     Model-checks the given model against the given module.
     """
     tools_jar_path = normpath(tools_jar_path)
+    apalache_path = normpath(join(apalache_path, 'bin', 'apalache-mc'))
+    apalache_jar_path = normpath(join(apalache_path, 'lib', 'apalache.jar'))
     module_path = normpath(module_path)
     model_path = normpath(model_path)
     tlapm_lib_path = normpath(tlapm_lib_path)
     community_jar_path = normpath(community_jar_path)
     try:
-        tlc = subprocess.run(
-            [
+        if mode == 'symbolic':
+            apalache = subprocess.run([
+                    apalache_path, 'check',
+                    f'--config={model_path}',
+                    module_path
+                ],
+                timeout=hard_timeout_in_seconds,
+                stdout=subprocess.PIPE,
+                stderr=subprocess.STDOUT,
+                text=True
+            )
+            return apalache
+        else:
+            tlc = subprocess.run([
                 'java',
                 '-Dtlc2.TLC.ide=Github',
                 '-Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff',
                 '-XX:+UseParallelGC',
                 # Jar paths must go first
-                '-cp', pathsep.join([tools_jar_path, community_jar_path, tlapm_lib_path]),
+                '-cp', pathsep.join([
+                    tools_jar_path,
+                    apalache_jar_path,
+                    community_jar_path,
+                    tlapm_lib_path
+                ]),
                 'tlc2.TLC',
                 module_path,
                 '-config', model_path,
                 '-workers', 'auto',
                 '-lncheck', 'final',
                 '-cleanup'
-            ] + get_run_mode(mode),
-            timeout=hard_timeout_in_seconds,
-            stdout=subprocess.PIPE,
-            stderr=subprocess.STDOUT,
-            text=True
-        )
-        return tlc
+                ] + get_run_mode(mode),
+                timeout=hard_timeout_in_seconds,
+                stdout=subprocess.PIPE,
+                stderr=subprocess.STDOUT,
+                text=True
+            )
+            return tlc
     except subprocess.TimeoutExpired as e:
         return e
 
diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py
index 324fbf3d..bf0f18b9 100644
--- a/.github/scripts/translate_pluscal.py
+++ b/.github/scripts/translate_pluscal.py
@@ -24,8 +24,8 @@
 tools_path = normpath(args.tools_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
-skip_modules = [normpath(path) for path in args.skip]
-only_modules = [normpath(path) for path in args.only]
+skip_modules = args.skip
+only_modules = args.only
 
 manifest = tla_utils.load_json(manifest_path)
 
@@ -35,8 +35,8 @@
     for spec in manifest['specifications']
     for module in spec['modules']
         if 'pluscal' in module['features']
-        and normpath(module['path']) not in skip_modules
-        and (only_modules == [] or normpath(module['path']) in only_modules)
+        and module['path'] not in skip_modules
+        and (only_modules == [] or module['path'] in only_modules)
 ]
 
 for path in skip_modules:
@@ -53,6 +53,7 @@ def translate_module(module_path):
     match result:
         case CompletedProcess():
             if result.returncode == 0:
+                logging.debug(result.stdout)
                 return True
             else:
                 logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}')
diff --git a/.github/scripts/unicode_conversion.py b/.github/scripts/unicode_conversion.py
index 7cffa8aa..0fddbff4 100644
--- a/.github/scripts/unicode_conversion.py
+++ b/.github/scripts/unicode_conversion.py
@@ -26,8 +26,8 @@
 to_ascii = args.to_ascii
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
-skip_modules = [normpath(path) for path in args.skip]
-only_modules = [normpath(path) for path in args.only]
+skip_modules = args.skip
+only_modules = args.only
 
 manifest = tla_utils.load_json(manifest_path)
 
@@ -36,8 +36,8 @@
     tla_utils.from_cwd(examples_root, module['path'])
     for spec in manifest['specifications']
     for module in spec['modules']
-        if normpath(module['path']) not in skip_modules
-        and (only_modules == [] or normpath(module['path']) in only_modules)
+        if module['path'] not in skip_modules
+        and (only_modules == [] or module['path'] in only_modules)
 ]
 
 for path in skip_modules:
@@ -54,6 +54,7 @@ def convert_module(module_path):
     match result:
         case CompletedProcess():
             if result.returncode == 0:
+                logging.debug(result.stdout)
                 return True
             else:
                 logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}')
diff --git a/.github/scripts/unicode_number_set_shim.py b/.github/scripts/unicode_number_set_shim.py
index 6ad246b5..84f4a1fc 100644
--- a/.github/scripts/unicode_number_set_shim.py
+++ b/.github/scripts/unicode_number_set_shim.py
@@ -117,7 +117,6 @@ def write_module(examples_root, module_path, module_bytes):
 if __name__ == '__main__':
     parser = ArgumentParser(description='Adds ℕ/ℤ/ℝ Unicode number set shim definitions to modules as needed.')
     parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
-    parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False)
     parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip', required=False, default=[])
     parser.add_argument('--only', nargs='+', help='If provided, only modify models in this space-separated list', required=False, default=[])
     args = parser.parse_args()
@@ -125,8 +124,8 @@ def write_module(examples_root, module_path, module_bytes):
     manifest_path = normpath(args.manifest_path)
     manifest = tla_utils.load_json(manifest_path)
     examples_root = dirname(manifest_path)
-    skip_modules = [normpath(path) for path in args.skip]
-    only_modules = [normpath(path) for path in args.only]
+    skip_modules = args.skip
+    only_modules = args.only
 
     TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language(), 'tlaplus')
     parser = Parser()
@@ -137,8 +136,8 @@ def write_module(examples_root, module_path, module_bytes):
         module['path']
         for spec in manifest['specifications']
         for module in spec['modules']
-            if normpath(module['path']) not in skip_modules
-            and (only_modules == [] or normpath(module['path']) in only_modules)
+            if module['path'] not in skip_modules
+            and (only_modules == [] or module['path'] in only_modules)
     ]
 
     for module_path in modules:
diff --git a/.github/scripts/windows-setup.sh b/.github/scripts/windows-setup.sh
index 3645de5d..9f0e5f18 100755
--- a/.github/scripts/windows-setup.sh
+++ b/.github/scripts/windows-setup.sh
@@ -37,6 +37,11 @@ main() {
   # Get TLA⁺ tools
   mkdir -p "$DEPS_DIR/tools"
   curl http://nightly.tlapl.us/dist/tla2tools.jar --output "$DEPS_DIR/tools/tla2tools.jar"
+  # Get Apalache
+  curl -L https://github.com/informalsystems/apalache/releases/latest/download/apalache.zip --output apalache.zip
+  7z x apalache.zip
+  mv apalache "$DEPS_DIR/"
+  rm apalache.zip
   # Get TLA⁺ community modules
   mkdir -p "$DEPS_DIR/community"
   curl -L https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output "$DEPS_DIR/community/modules.jar"
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index d7075b6e..18e5c172 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -110,6 +110,7 @@ jobs:
           fi
           python $SCRIPT_DIR/parse_modules.py                            \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --apalache_path $DEPS_DIR/apalache                           \
             --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json                                \
@@ -121,9 +122,12 @@ jobs:
           if [ ${{ matrix.unicode }} ]; then
             # This redefines Real so cannot be shimmed
             SKIP+=("specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.cfg")
+            # Apalache does not yet support Unicode
+            SKIP+=("specifications/EinsteinRiddle/Einstein.cfg")
           fi
           python $SCRIPT_DIR/check_small_models.py                       \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --apalache_path $DEPS_DIR/apalache                           \
             --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json                                \
@@ -140,6 +144,7 @@ jobs:
           fi
           python $SCRIPT_DIR/smoke_test_large_models.py                  \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --apalache_path $DEPS_DIR/apalache                           \
             --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json                                \
diff --git a/.gitignore b/.gitignore
index a542435b..abff5e71 100644
--- a/.gitignore
+++ b/.gitignore
@@ -46,3 +46,6 @@ tree-sitter-tlaplus/
 ## Ignore tools/ folder created by .devcontainer.json
 tools/
 
+# Ignore directory created by Apalache
+_apalache-out
+
diff --git a/README.md b/README.md
index 0b039bae..540f4063 100644
--- a/README.md
+++ b/README.md
@@ -53,6 +53,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Snapshot Key-Value Store](specifications/KeyValueStore)                                            | Andrew Helwer, Murat Demirbas                       |          |             |    ✔    |     ✔     |          |
 | [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts)               | Stephan Merz                                        |          |             |    ✔    |     ✔     |          |
 | [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR)                                            | Guanzhou Hu                                         |          |             |    ✔    |     ✔     |          |
+| [Einstein's Riddle](specifications/EinsteinRiddle)                                                  | Isaac DeFrain, Giuliano Losa                        |          |             |         |           |    ✔     |
 | [Resource Allocator](specifications/allocator)                                                      | Stephan Merz                                        |          |             |         |     ✔     |          |
 | [Transitive Closure](specifications/TransitiveClosure)                                              | Stephan Merz                                        |          |             |         |     ✔     |          |
 | [Atomic Commitment Protocol](specifications/acp)                                                    | Stephan Merz                                        |          |             |         |     ✔     |          |
@@ -70,7 +71,6 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Multi-Car Elevator System](specifications/MultiCarElevator)                                        | Andrew Helwer                                       |          |             |         |     ✔     |          |
 | [Nano Blockchain Protocol](specifications/NanoBlockchain)                                           | Andrew Helwer                                       |          |             |         |     ✔     |          |
 | [The Readers-Writers Problem](specifications/ReadersWriters)                                        | Isaac DeFrain                                       |          |             |         |     ✔     |          |
-| [Einstein's Riddle](specifications/EinsteinRiddle)                                                  | Isaac DeFrain, Giuliano Losa                        |          |             |         |     ✔     |    ✔     |
 | [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           |          |             |         |     ✔     |          |
@@ -85,10 +85,10 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Chameneos, a Concurrency Game](specifications/Chameneos)                                           | Mariusz Ryndzionek                                  |          |             |         |     ✔     |          |
 | [PCR Testing for Snippets of DNA](specifications/glowingRaccoon)                                    | Martin Harrison                                     |          |             |         |     ✔     |          |
 | [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                          |          |             |         |      ✔    |          |
 | [TCP as defined in RFC 9293](specifications/tcp)                                                    | Markus Kuppe                                        |          |             |         |      ✔    |          |
+| [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                                      |          |             |         |           |          |
+| [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.
diff --git a/manifest-schema.json b/manifest-schema.json
index a8121585..11297238 100644
--- a/manifest-schema.json
+++ b/manifest-schema.json
@@ -61,7 +61,7 @@
                       "mode": {
                         "oneOf": [
                           {
-                            "enum": ["exhaustive search", "generate"]
+                            "enum": ["exhaustive search", "generate", "symbolic"]
                           },
                           {
                             "type": "object",
diff --git a/manifest.json b/manifest.json
index 4385e8f3..512f52ad 100644
--- a/manifest.json
+++ b/manifest.json
@@ -454,9 +454,9 @@
           "models": [
             {
               "path": "specifications/EinsteinRiddle/Einstein.cfg",
-              "runtime": "unknown",
-              "size": "large",
-              "mode": "exhaustive search",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "symbolic",
               "features": [],
               "result": "safety failure"
             }
diff --git a/specifications/EinsteinRiddle/Einstein.tla b/specifications/EinsteinRiddle/Einstein.tla
index eb67a5d3..02b7cfb1 100644
--- a/specifications/EinsteinRiddle/Einstein.tla
+++ b/specifications/EinsteinRiddle/Einstein.tla
@@ -38,7 +38,7 @@
 (* Instructions to run `^Apalache^' appear at the end of the file.               *)
 (*********************************************************************************)
 
-EXTENDS Naturals, FiniteSets
+EXTENDS Naturals, FiniteSets, Apalache
 
 House == 1..5
 
@@ -46,13 +46,17 @@ House == 1..5
 \* would be evaluated faster.  However, TLC!Permutations equals a
 \* set of records whereas Permutation below equals a set of tuples/
 \* sequences.  Also, Permutation expects Cardinality(S) = 5.
-Permutation(S) ==
-    { p \in [ House -> S ] :
-        /\ p[2] \in S \ {p[1]}
-        /\ p[3] \in S \ {p[1], p[2]}
-        /\ p[4] \in S \ {p[1], p[2], p[3]}
-        /\ p[5] \in S \ {p[1], p[2], p[3], p[4]} }
-                
+\* @type: Set(Str) => Set(Seq(Str));
+Permutation(S) == {
+  FunAsSeq(p, 5, 5) : p \in {
+    p \in [ House -> S ] :
+      /\ p[2] \in S \ {p[1]}
+      /\ p[3] \in S \ {p[1], p[2]}
+      /\ p[4] \in S \ {p[1], p[2], p[3]}
+      /\ p[5] \in S \ {p[1], p[2], p[3], p[4]}
+    }
+  }
+
 \* In most specs, the following parameterization would be defined as
 \* constants.  Given that Einstein's riddle has only this
 \* parameterization, the constants are replaced with constant-level
@@ -65,15 +69,15 @@ PETS == Permutation({ "bird", "cat", "dog", "fish", "horse" })
 CIGARS == Permutation({ "blend", "bm", "dh", "pm", "prince" })
 
 VARIABLES
-    \* @type: Int -> Str;
+    \* @type: Seq(Str);
     nationality,    \* tuple of nationalities
-    \* @type: Int -> Str;
+    \* @type: Seq(Str);
     colors,         \* tuple of house colors
-    \* @type: Int -> Str;
+    \* @type: Seq(Str);
     pets,           \* tuple of pets
-    \* @type: Int -> Str;
+    \* @type: Seq(Str);
     cigars,         \* tuple of cigars
-    \* @type: Int -> Str;
+    \* @type: Seq(Str);
     drinks          \* tuple of drinks
 
 ------------------------------------------------------------
@@ -136,7 +140,7 @@ Init ==
 
 \* Apalache cannot infer the type of `vars' because it could be a sequence or a tuple.
 \* So we explicitely tell Apalache that it is a sequence by adding the following annotation:
-\* @type: Seq(Int -> Str);
+\* @type: Seq(Seq(Str));
 vars == <<nationality, colors, cigars, pets, drinks>>
 
 Next ==
@@ -167,4 +171,4 @@ FindSolution == ~Solution
 \* `^apalache-mc check --init=Init --inv=FindSolution --length=0 --run-dir=./outout Einstein.tla^'
 \* You will then find the solution in `^./output/violation.tla^'.
 
-============================================================
\ No newline at end of file
+============================================================