diff --git a/.github/scripts/check_manifest_features.py b/.github/scripts/check_manifest_features.py
index b2d8044e..032fbf9c 100644
--- a/.github/scripts/check_manifest_features.py
+++ b/.github/scripts/check_manifest_features.py
@@ -164,7 +164,8 @@ def check_features(parser, queries, manifest, examples_root):
             if parse_err:
                 success = False
                 logging.error(f'Module {module["path"]} contains syntax errors')
-            expected_features = get_tree_features(tree, queries)
+            module_features = get_tree_features(tree, queries)
+            expected_features = module_features - {'proof'}
             actual_features = set(module['features'])
             if expected_features != actual_features:
                 success = False
@@ -172,7 +173,10 @@ def check_features(parser, queries, manifest, examples_root):
                     f'Module {module["path"]} has incorrect features in manifest; '
                     + f'expected {list(expected_features)}, actual {list(actual_features)}'
                 )
-            expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in expected_features, queries)
+            if 'proof' in module_features and 'proof' not in module:
+                success = False
+                logging.error(f'Module {module["path"]} contains proof but no proof runtime details in manifest')
+            expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in module_features, queries)
             actual_imports = set(module['communityDependencies'])
             if expected_imports != actual_imports:
                 success = False
@@ -192,7 +196,7 @@ def check_features(parser, queries, manifest, examples_root):
 
 if __name__ == '__main__':
     parser = ArgumentParser(description='Checks metadata in manifest.json files against module and model files in repository.')
-    parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+    parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
     args = parser.parse_args()
 
     manifest = tla_utils.load_all_manifests(args.examples_root)
diff --git a/.github/scripts/check_manifest_files.py b/.github/scripts/check_manifest_files.py
index 268c08a3..aba2d06b 100644
--- a/.github/scripts/check_manifest_files.py
+++ b/.github/scripts/check_manifest_files.py
@@ -12,7 +12,7 @@
 import tla_utils
 
 parser = ArgumentParser(description='Checks manifests against module and model files in repository.')
-parser.add_argument('--ci_ignore_path', help='Path to the .ciignore file', required=True)
+parser.add_argument('--ci_ignore_path', help='Path to the .ciignore file', required=False, default='./.ciignore')
 args = parser.parse_args()
 
 ci_ignore_path = normpath(args.ci_ignore_path)
diff --git a/.github/scripts/check_manifest_schema.py b/.github/scripts/check_manifest_schema.py
index 78a34c23..32c14c6c 100644
--- a/.github/scripts/check_manifest_schema.py
+++ b/.github/scripts/check_manifest_schema.py
@@ -15,7 +15,7 @@
 import tla_utils
 
 parser = ArgumentParser(description='Checks tlaplus/examples manifest.json files against JSON schema file.')
-parser.add_argument('--schema_path', help='Path to the tlaplus/examples manifest-schema.json file', required=True)
+parser.add_argument('--schema_path', help='Path to the tlaplus/examples manifest-schema.json file', required=False, default='manifest-schema.json')
 args = parser.parse_args()
 
 examples_root = dirname(args.schema_path)
diff --git a/.github/scripts/check_markdown_table.py b/.github/scripts/check_markdown_table.py
index 4d112012..dc17819d 100644
--- a/.github/scripts/check_markdown_table.py
+++ b/.github/scripts/check_markdown_table.py
@@ -67,7 +67,7 @@ def from_json(path, spec):
         path,
         set(spec['authors']),
         'beginner' in spec['tags'],
-        any([module for module in spec['modules'] if 'proof' in module['features']]),
+        any([module for module in spec['modules'] if 'proof' in module]),
         any([module for module in spec['modules'] if 'pluscal' in module['features']]),
         any([model for module in spec['modules'] for model in module['models'] if model['mode'] != 'symbolic']),
         any([model for module in spec['modules'] for model in module['models'] if model['mode'] == 'symbolic']),
@@ -75,7 +75,7 @@ def from_json(path, spec):
     )
 
 parser = ArgumentParser(description='Validates the spec table in README.md against the manifest.json.')
-parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
+parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=False, default='./README.md')
 args = parser.parse_args()
 
 manifest = tla_utils.load_all_manifests(dirname(args.readme_path))
diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py
index c037baba..7a376fa8 100644
--- a/.github/scripts/check_proofs.py
+++ b/.github/scripts/check_proofs.py
@@ -3,6 +3,7 @@
 """
 
 from argparse import ArgumentParser
+from datetime import timedelta
 from os.path import dirname, join, normpath
 import logging
 import subprocess
@@ -10,8 +11,9 @@
 import tla_utils
 
 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=False, default = 'deps/tlapm')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
+parser.add_argument('--runtime_seconds_limit', help='Only run proofs with expected runtime less than this value', required=False, default=60)
 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')
@@ -22,46 +24,68 @@
 manifest = tla_utils.load_all_manifests(examples_root)
 skip_modules = args.skip
 only_modules = args.only
+hard_timeout_in_seconds = args.runtime_seconds_limit * 2
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
-proof_module_paths = [
-    module['path']
-    for path, spec in manifest
-    for module in spec['modules']
-        if 'proof' in module['features']
-        and module['path'] not in skip_modules
-        and (only_modules == [] or module['path'] in only_modules)
-]
+proof_module_paths = sorted(
+    [
+        (manifest_dir, spec, module, runtime)
+        for manifest_dir, spec in manifest
+        for module in spec['modules']
+        if 'proof' in module
+            and (runtime := tla_utils.parse_timespan(module['proof']['runtime'])) <= timedelta(seconds = args.runtime_seconds_limit)
+            and module['path'] not in skip_modules
+            and (only_modules == [] or module['path'] in only_modules)
+    ],
+    key = lambda m : m[3]
+)
 
 for path in skip_modules:
     logging.info(f'Skipping {path}')
 
 success = True
 tlapm_path = join(tlapm_path, 'bin', 'tlapm')
-for module_path in proof_module_paths:
+for manifest_dir, spec, module, expected_runtime in proof_module_paths:
+    module_path = module['path']
     logging.info(module_path)
     start_time = timer()
-    module_path = tla_utils.from_cwd(examples_root, module_path)
-    module_dir = dirname(module_path)
-    tlapm = subprocess.run(
-        [
-            tlapm_path, module_path,
-            '-I', module_dir,
-            '--stretch', '5'
-        ],
-        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.stdout)
+    full_module_path = tla_utils.from_cwd(examples_root, module_path)
+    module_dir = dirname(full_module_path)
+    try:
+        tlapm_result = subprocess.run(
+            [
+                tlapm_path, full_module_path,
+                '-I', module_dir,
+                '--stretch', '5'
+            ],
+            stdout  = subprocess.PIPE,
+            stderr  = subprocess.STDOUT,
+            text    = True,
+            timeout = hard_timeout_in_seconds
+        )
+        end_time = timer()
+        actual_runtime = timedelta(seconds = end_time - start_time)
+        output = ' '.join(tlapm_result.args) + '\n' + tlapm_result.stdout
+        logging.info(f'Checked proofs in {tla_utils.format_timespan(actual_runtime)} vs. {tla_utils.format_timespan(expected_runtime)} expected')
+        if tlapm_result.returncode != 0:
+            logging.error(f'Proof checking failed for {module_path}:')
+            logging.error(output)
+            success = False
+        else:
+            if 'proof' not in module or module['proof']['runtime'] == 'unknown':
+                module['proof'] = { 'runtime' : tla_utils.format_timespan(actual_runtime) }
+                manifest_path = join(manifest_dir, 'manifest.json')
+                tla_utils.write_json(spec, manifest_path)
+            logging.debug(output)
+    except subprocess.TimeoutExpired as tlapm_result:
+        # stdout is a string on Windows, byte array everywhere else
+        stdout = tlapm_result.stdout if type(tlapm_result.stdout) == str else tlapm_result.stdout.decode('utf-8')
+        args, timeout = tlapm_result.args
+        logging.error(f'{module_path} hit hard timeout of {timeout} seconds')
+        output = ' '.join(args) + '\n' + stdout
+        logging.error(output)
         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 ddab391f..dcf69bbb 100644
--- a/.github/scripts/check_small_models.py
+++ b/.github/scripts/check_small_models.py
@@ -13,11 +13,11 @@
 import tla_utils
 
 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=False, default='deps/apalache')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 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')
@@ -78,9 +78,11 @@ def check_model(module, model, expected_runtime):
             logging.debug(output)
             return True
         case TimeoutExpired():
-            args, _ = tlc_result.args
-            output = ' '.join(args) + '\n' + tlc_result.stdout
-            logging.error(f'{model_path} hit hard timeout of {hard_timeout_in_seconds} seconds')
+            args, timeout = tlc_result.args
+            # stdout is a string on Windows, byte array everywhere else
+            stdout = tlc_result.stdout if type(tlc_result.stdout) == str else tlc_result.stdout.decode('utf-8')
+            output = ' '.join(args) + '\n' + stdout
+            logging.error(f'{model_path} hit hard timeout of {timeout} seconds')
             logging.error(output)
             return False
         case _:
diff --git a/.github/scripts/format_markdown_table.py b/.github/scripts/format_markdown_table.py
index 361e3c22..15b0bada 100644
--- a/.github/scripts/format_markdown_table.py
+++ b/.github/scripts/format_markdown_table.py
@@ -13,7 +13,7 @@
 from mistletoe.markdown_renderer import MarkdownRenderer
 
 parser = ArgumentParser(description='Formats or modifies the spec table in README.md.')
-parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
+parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=False, default='README.md')
 args = parser.parse_args()
 
 columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']
diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py
index 52361ae5..e9e94dc0 100644
--- a/.github/scripts/generate_manifest.py
+++ b/.github/scripts/generate_manifest.py
@@ -35,9 +35,20 @@ def get_tla_files(examples_root, dir_path):
     Gets paths of all .tla files in the given directory, except for error
     trace specs.
     """
-    return [
-        path for path in glob.glob(f'{dir_path}/**/*.tla', root_dir=examples_root, recursive=True)
+    return sorted(
+        path
+        for path in glob.glob(f'{dir_path}/**/*.tla', root_dir=examples_root, recursive=True)
         if '_TTrace_' not in path
+    )
+
+def get_tla_file_features(examples_root, dir_path, parser, queries):
+    """
+    Gets paths of all .tla files in a given directory, along with their
+    features.
+    """
+    return [
+        (path, get_module_features(examples_root, path, parser, queries))
+        for path in get_tla_files(examples_root, dir_path)
     ]
 
 def get_cfg_files(examples_root, tla_path):
@@ -73,7 +84,7 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
             {
                 'path': tla_utils.to_posix(tla_path),
                 'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
-                'features': sorted(list(get_module_features(examples_root, tla_path, parser, queries))),
+                'features': sorted(list(module_features - {'proof'})),
                 'models': [
                     {
                         'path': tla_utils.to_posix(cfg_path),
@@ -83,8 +94,8 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
                     }
                     for cfg_path in sorted(get_cfg_files(examples_root, tla_path))
                 ]
-            }
-            for tla_path in sorted(get_tla_files(examples_root, spec_path))
+            } | ({'proof' : {'runtime': 'unknown'}} if 'proof' in module_features else {})
+            for tla_path, module_features in get_tla_file_features(examples_root, spec_path, parser, queries)
         ]
     }
 
@@ -107,9 +118,13 @@ def find_corresponding_module(old_module, new_spec):
     return modules[0] if any(modules) else None
 
 def integrate_module_info(old_module, new_module):
-    fields = []
-    for field in fields:
+    required_fields = []
+    for field in required_fields:
         new_module[field] = old_module[field]
+    optional_fields = ['proof']
+    for field in optional_fields:
+        if field in old_module:
+            new_module[field] = old_module[field]
 
 def find_corresponding_model(old_model, new_module):
     models = [
diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py
index e7b28e4f..68ea5bf8 100644
--- a/.github/scripts/parse_modules.py
+++ b/.github/scripts/parse_modules.py
@@ -11,11 +11,11 @@
 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=False, default='deps/apalache')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
diff --git a/.github/scripts/record_model_state_space.py b/.github/scripts/record_model_state_space.py
index f8f2326a..c16f3088 100644
--- a/.github/scripts/record_model_state_space.py
+++ b/.github/scripts/record_model_state_space.py
@@ -11,10 +11,10 @@
 import tla_utils
 
 parser = ArgumentParser(description='Updates manifest.json with unique & total model states for each small model.')
-parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 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('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')
diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py
index 0edd04dc..72b1d61b 100644
--- a/.github/scripts/smoke_test_large_models.py
+++ b/.github/scripts/smoke_test_large_models.py
@@ -13,11 +13,11 @@
 import tla_utils
 
 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='deps/tools/tla2tools.jar')
+parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=False, default='deps/apalache')
+parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=False, default='deps/tlapm/library')
+parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=False, default='deps/community/modules.jar')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 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')
diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py
index 1816e791..67ec0179 100644
--- a/.github/scripts/tla_utils.py
+++ b/.github/scripts/tla_utils.py
@@ -108,6 +108,17 @@ def parse_timespan(unparsed):
     pattern = '%H:%M:%S'
     return timedelta.max if unparsed == 'unknown' else datetime.strptime(unparsed, pattern) - datetime.strptime('00:00:00', pattern)
 
+def format_timespan(t):
+    """
+    Formats the given timedelta into a HH:MM:SS string. If a timespan of
+    nonzero length, rounds up to minimum of one second.
+    """
+    if t < timedelta(seconds = 1):
+        return '00:00:01' if t > timedelta.min else '00:00:00'
+    else:
+        seconds = int(t.total_seconds())
+        return f'{seconds // 3600:02d}:{seconds % 3600 // 60:02d}:{seconds % 3600 % 60:02d}'
+
 def get_run_mode(mode):
     """
     Converts the model run mode found in manifest.json into TLC CLI
diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py
index 478bc7c7..71582922 100644
--- a/.github/scripts/translate_pluscal.py
+++ b/.github/scripts/translate_pluscal.py
@@ -12,8 +12,8 @@
 import tla_utils
 
 parser = ArgumentParser(description='Run PlusCal translation on all modules.')
-parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
-parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=False, default='./deps/tools/tla2tools.jar')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip converting', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
diff --git a/.github/scripts/unicode_conversion.py b/.github/scripts/unicode_conversion.py
index f7c67840..543028f6 100644
--- a/.github/scripts/unicode_conversion.py
+++ b/.github/scripts/unicode_conversion.py
@@ -12,8 +12,8 @@
 import tla_utils
 
 parser = ArgumentParser(description='Converts all TLA+ modules from ASCII to Unicode or vice-versa.')
-parser.add_argument('--tlauc_path', help='Path to the TLAUC executable', required=True)
-parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
+parser.add_argument('--tlauc_path', help='Path to the TLAUC executable', required=False, default='./deps/tlauc/tlauc')
+parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.')
 parser.add_argument('--to_ascii', help='Convert to ASCII instead of Unicode', action='store_true')
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip converting', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[])
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 6d696a08..0efddefb 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -14,7 +14,6 @@ concurrency:
 
 jobs:
   validate:
-    name: Validate Manifest, Specs, & Models
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -136,23 +135,9 @@ jobs:
       - name: Check proofs
         if: matrix.os != 'windows-latest' && !matrix.unicode
         run: |
-          SKIP=(
-            # Long-running; see https://github.com/tlaplus/tlapm/issues/85
-            specifications/ewd998/EWD998_proof.tla
-            specifications/Bakery-Boulangerie/Bakery.tla
-            specifications/Bakery-Boulangerie/Boulanger.tla
-            specifications/LoopInvariance/Quicksort.tla
-            specifications/LoopInvariance/SumSequence.tla
-            specifications/lamport_mutex/LamportMutex_proofs.tla
-            specifications/bcastByz/bcastByz.tla
-            # specifications/MisraReachability/ReachabilityProofs.tla
-            specifications/byzpaxos/VoteProof.tla
-            specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
-          )
           python $SCRIPT_DIR/check_proofs.py       \
             --tlapm_path $DEPS_DIR/tlapm           \
-            --examples_root .                      \
-            --skip "${SKIP[@]}"
+            --examples_root .
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 9feb56c1..bb370112 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -45,6 +45,8 @@ Steps:
    - Spec authors: a list of people who authored the spec
    - Spec tags:
      - `"beginner"` if your spec is appropriate for TLA⁺ newcomers
+   - Module proof runtime: if module contains formal proofs, record the approximate time necessary to check the proofs with TLAPM on an ordinary workstation; add `"proof" : { "runtime" : "HH:MM:SS" }` to the module fields at the same level as the `communityDependencies` and `models`
+     - If less than one minute, proof will be checked in its entirety by the CI
    - Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format
      - If less than 30 seconds, will be run in its entirety by the CI; otherwise will only be smoke-tested for 5 seconds
    - Model mode:
@@ -68,7 +70,7 @@ Steps:
    - A checkmark indicating whether the spec is appropriate for beginners
      - Checked IFF (if and only if) `beginner` is present in the `tags` field of your spec in `manifest.json`
    - A checkmark indicating whether the spec contains a formal proof
-     - Checked IFF a `proof` tag is present in the `features` field of least one module under your spec in `manifest.json`
+     - Checked IFF `proof` runtime details are present in at least one module under your spec in `manifest.json`
    - A checkmark indicating whether the spec contains PlusCal
      - Checked IFF a `pluscal` tag is present in the `features` field of least one module under your spec in `manifest.json`
    - A checkmark indicating whether the spec contains a TLC-checkable model
diff --git a/manifest-schema.json b/manifest-schema.json
index cb143ada..592d3d3e 100644
--- a/manifest-schema.json
+++ b/manifest-schema.json
@@ -29,14 +29,25 @@
           },
           "features": {
             "type": "array",
-            "items": {"enum": ["pluscal", "proof", "action composition"]}
+            "items": {"enum": ["pluscal", "action composition"]}
+          },
+          "proof": {
+            "type": "object",
+            "required": ["runtime"],
+            "additionalProperties": false,
+            "properties": {
+              "runtime": {
+                "type": "string",
+                "pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$"
+              }
+            }
           },
           "models": {
             "type": "array",
             "items": {
               "type": "object",
-              "additionalProperties": false,
               "required": ["path", "runtime", "mode", "result"],
+              "additionalProperties": false,
               "properties": {
                 "path": {"type": "string"},
                 "runtime": {
@@ -53,13 +64,13 @@
                     },
                     {
                       "type": "object",
-                      "additionalProperties": false,
                       "required": ["simulate"],
+                      "additionalProperties": false,
                       "properties": {
                         "simulate": {
                           "type": "object",
-                          "additionalProperties": false,
                           "required": ["traceCount"],
+                          "additionalProperties": false,
                           "properties": {
                             "traceCount": {"type": "number"}
                           }
diff --git a/specifications/Bakery-Boulangerie/manifest.json b/specifications/Bakery-Boulangerie/manifest.json
index 19818214..9125d62c 100644
--- a/specifications/Bakery-Boulangerie/manifest.json
+++ b/specifications/Bakery-Boulangerie/manifest.json
@@ -10,19 +10,23 @@
       "path": "specifications/Bakery-Boulangerie/Bakery.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:00:20"
+      }
     },
     {
       "path": "specifications/Bakery-Boulangerie/Boulanger.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:00:30"
+      }
     },
     {
       "path": "specifications/Bakery-Boulangerie/MCBakery.tla",
@@ -54,4 +58,4 @@
       ]
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/FiniteMonotonic/manifest.json b/specifications/FiniteMonotonic/manifest.json
index 1f9fe7a6..07e1ab42 100644
--- a/specifications/FiniteMonotonic/manifest.json
+++ b/specifications/FiniteMonotonic/manifest.json
@@ -20,10 +20,11 @@
     {
       "path": "specifications/FiniteMonotonic/CRDT_proof.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/FiniteMonotonic/DistributedReplicatedLog.tla",
diff --git a/specifications/LearnProofs/manifest.json b/specifications/LearnProofs/manifest.json
index e677a6d7..54c0e65c 100644
--- a/specifications/LearnProofs/manifest.json
+++ b/specifications/LearnProofs/manifest.json
@@ -11,19 +11,23 @@
       "path": "specifications/LearnProofs/AddTwo.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/LearnProofs/FindHighest.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:00:10"
+      }
     },
     {
       "path": "specifications/LearnProofs/MCFindHighest.tla",
diff --git a/specifications/LoopInvariance/manifest.json b/specifications/LoopInvariance/manifest.json
index 3cafa1f4..aabe723f 100644
--- a/specifications/LoopInvariance/manifest.json
+++ b/specifications/LoopInvariance/manifest.json
@@ -13,10 +13,12 @@
       "path": "specifications/LoopInvariance/BinarySearch.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/LoopInvariance/MCBinarySearch.tla",
@@ -54,19 +56,23 @@
       "path": "specifications/LoopInvariance/Quicksort.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:00:45"
+      }
     },
     {
       "path": "specifications/LoopInvariance/SumSequence.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
-      "models": []
+      "models": [],
+      "proof": {
+        "runtime": "00:01:30"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/Majority/manifest.json b/specifications/Majority/manifest.json
index c0182be3..42edd0ad 100644
--- a/specifications/Majority/manifest.json
+++ b/specifications/Majority/manifest.json
@@ -32,10 +32,11 @@
     {
       "path": "specifications/Majority/MajorityProof.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/MisraReachability/manifest.json b/specifications/MisraReachability/manifest.json
index 7e52f4a7..68aed1d6 100644
--- a/specifications/MisraReachability/manifest.json
+++ b/specifications/MisraReachability/manifest.json
@@ -70,10 +70,11 @@
     {
       "path": "specifications/MisraReachability/ParReachProofs.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/MisraReachability/Reachability.tla",
@@ -84,10 +85,11 @@
     {
       "path": "specifications/MisraReachability/ReachabilityProofs.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/MisraReachability/ReachabilityTest.tla",
@@ -106,10 +108,11 @@
     {
       "path": "specifications/MisraReachability/ReachableProofs.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/MultiCarElevator/manifest.json b/specifications/MultiCarElevator/manifest.json
index 98c4d3be..9198b8af 100644
--- a/specifications/MultiCarElevator/manifest.json
+++ b/specifications/MultiCarElevator/manifest.json
@@ -51,4 +51,4 @@
       ]
     }
   ]
-}
+}
\ No newline at end of file
diff --git a/specifications/NanoBlockchain/manifest.json b/specifications/NanoBlockchain/manifest.json
index 82cae2aa..d7f96caa 100644
--- a/specifications/NanoBlockchain/manifest.json
+++ b/specifications/NanoBlockchain/manifest.json
@@ -43,4 +43,4 @@
       "models": []
     }
   ]
-}
+}
\ No newline at end of file
diff --git a/specifications/Paxos/manifest.json b/specifications/Paxos/manifest.json
index 64505f12..79ff7aeb 100644
--- a/specifications/Paxos/manifest.json
+++ b/specifications/Paxos/manifest.json
@@ -8,10 +8,11 @@
     {
       "path": "specifications/Paxos/Consensus.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/Paxos/MCConsensus.tla",
@@ -70,10 +71,11 @@
     {
       "path": "specifications/Paxos/Voting.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/PaxosHowToWinATuringAward/manifest.json b/specifications/PaxosHowToWinATuringAward/manifest.json
index f59641ef..6bee1c44 100644
--- a/specifications/PaxosHowToWinATuringAward/manifest.json
+++ b/specifications/PaxosHowToWinATuringAward/manifest.json
@@ -10,10 +10,11 @@
     {
       "path": "specifications/PaxosHowToWinATuringAward/Consensus.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.tla",
@@ -78,10 +79,11 @@
     {
       "path": "specifications/PaxosHowToWinATuringAward/Voting.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/SimplifiedFastPaxos/manifest.json b/specifications/SimplifiedFastPaxos/manifest.json
index 866b3d88..7f271c63 100644
--- a/specifications/SimplifiedFastPaxos/manifest.json
+++ b/specifications/SimplifiedFastPaxos/manifest.json
@@ -39,4 +39,4 @@
       ]
     }
   ]
-}
+}
\ No newline at end of file
diff --git a/specifications/TeachingConcurrency/manifest.json b/specifications/TeachingConcurrency/manifest.json
index f9d0d478..fe0edc55 100644
--- a/specifications/TeachingConcurrency/manifest.json
+++ b/specifications/TeachingConcurrency/manifest.json
@@ -13,8 +13,7 @@
       "path": "specifications/TeachingConcurrency/Simple.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -26,14 +25,16 @@
           "totalStates": 1842,
           "stateDepth": 11
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/TeachingConcurrency/SimpleRegular.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -45,7 +46,10 @@
           "totalStates": 1454776,
           "stateDepth": 25
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/TwoPhase/manifest.json b/specifications/TwoPhase/manifest.json
index ba25fdc0..65e0369d 100644
--- a/specifications/TwoPhase/manifest.json
+++ b/specifications/TwoPhase/manifest.json
@@ -31,10 +31,11 @@
     {
       "path": "specifications/TwoPhase/TwoPhase.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/barriers/manifest.json b/specifications/barriers/manifest.json
index 072c4718..ffb8b10f 100644
--- a/specifications/barriers/manifest.json
+++ b/specifications/barriers/manifest.json
@@ -27,8 +27,7 @@
       "path": "specifications/barriers/Barriers.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -40,7 +39,10 @@
           "totalStates": 104515,
           "stateDepth": 93
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:02:00"
+      }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/bcastByz/manifest.json b/specifications/bcastByz/manifest.json
index 59cd181b..8778d2d0 100644
--- a/specifications/bcastByz/manifest.json
+++ b/specifications/bcastByz/manifest.json
@@ -10,9 +10,7 @@
     {
       "path": "specifications/bcastByz/bcastByz.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
+      "features": [],
       "models": [
         {
           "path": "specifications/bcastByz/bcastByz.cfg",
@@ -32,7 +30,10 @@
           "totalStates": 90,
           "stateDepth": 1
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:01:00"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/byzpaxos/VoteProof.tla b/specifications/byzpaxos/VoteProof.tla
index 76a67c5b..628c324e 100644
--- a/specifications/byzpaxos/VoteProof.tla
+++ b/specifications/byzpaxos/VoteProof.tla
@@ -1083,7 +1083,7 @@ THEOREM VT4 == TypeOK /\ VInv2 /\ VInv3  =>
     <3>3. /\ c \in 0 .. (b-1)
           /\ \E a \in Q : ~DidNotVoteIn(a,c)
           /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d)
-      BY <3>2
+      BY <3>2, SMTT(30)
     <3>. QED
       BY <3>3
   <2>4. PICK a0 \in Q, v \in Value : VotedFor(a0, c, v)
diff --git a/specifications/byzpaxos/manifest.json b/specifications/byzpaxos/manifest.json
index dcfbceba..2c5e1286 100644
--- a/specifications/byzpaxos/manifest.json
+++ b/specifications/byzpaxos/manifest.json
@@ -13,8 +13,7 @@
       "path": "specifications/byzpaxos/BPConProof.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -23,14 +22,16 @@
           "mode": "exhaustive search",
           "result": "unknown"
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:10:00"
+      }
     },
     {
       "path": "specifications/byzpaxos/Consensus.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -42,14 +43,16 @@
           "totalStates": 4,
           "stateDepth": 2
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/byzpaxos/PConProof.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -58,14 +61,16 @@
           "mode": "exhaustive search",
           "result": "success"
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/byzpaxos/VoteProof.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -77,7 +82,10 @@
           "totalStates": 318877,
           "stateDepth": 15
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:45"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/ewd840/manifest.json b/specifications/ewd840/manifest.json
index 3a5be40d..ab57bd94 100644
--- a/specifications/ewd840/manifest.json
+++ b/specifications/ewd840/manifest.json
@@ -63,10 +63,11 @@
     {
       "path": "specifications/ewd840/EWD840_proof.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:10"
+      }
     },
     {
       "path": "specifications/ewd840/SyncTerminationDetection.tla",
@@ -87,10 +88,11 @@
     {
       "path": "specifications/ewd840/SyncTerminationDetection_proof.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/ewd998/manifest.json b/specifications/ewd998/manifest.json
index f72db097..87604b55 100644
--- a/specifications/ewd998/manifest.json
+++ b/specifications/ewd998/manifest.json
@@ -27,10 +27,11 @@
     {
       "path": "specifications/ewd998/AsyncTerminationDetection_proof.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/ewd998/EWD998.tla",
@@ -185,10 +186,11 @@
     {
       "path": "specifications/ewd998/EWD998_proof.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:30"
+      }
     },
     {
       "path": "specifications/ewd998/Folds.tla",
diff --git a/specifications/lamport_mutex/manifest.json b/specifications/lamport_mutex/manifest.json
index fc23b49e..5bfa03be 100644
--- a/specifications/lamport_mutex/manifest.json
+++ b/specifications/lamport_mutex/manifest.json
@@ -14,10 +14,11 @@
     {
       "path": "specifications/lamport_mutex/LamportMutex_proofs.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:45"
+      }
     },
     {
       "path": "specifications/lamport_mutex/MCLamportMutex.tla",
@@ -36,4 +37,4 @@
       ]
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/locks_auxiliary_vars/manifest.json b/specifications/locks_auxiliary_vars/manifest.json
index 91b28eca..51c8fc74 100644
--- a/specifications/locks_auxiliary_vars/manifest.json
+++ b/specifications/locks_auxiliary_vars/manifest.json
@@ -11,8 +11,7 @@
       "path": "specifications/locks_auxiliary_vars/Lock.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -24,14 +23,15 @@
           "totalStates": 21,
           "stateDepth": 5
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     },
     {
       "path": "specifications/locks_auxiliary_vars/LockHS.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
+      "features": [],
       "models": [
         {
           "path": "specifications/locks_auxiliary_vars/LockHS.cfg",
@@ -42,14 +42,16 @@
           "totalStates": 41,
           "stateDepth": 10
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:30"
+      }
     },
     {
       "path": "specifications/locks_auxiliary_vars/Peterson.tla",
       "communityDependencies": [],
       "features": [
-        "pluscal",
-        "proof"
+        "pluscal"
       ],
       "models": [
         {
@@ -61,7 +63,10 @@
           "totalStates": 77,
           "stateDepth": 11
         }
-      ]
+      ],
+      "proof": {
+        "runtime": "00:00:30"
+      }
     },
     {
       "path": "specifications/locks_auxiliary_vars/Stuttering.tla",
@@ -70,4 +75,4 @@
       "models": []
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/sums_even/manifest.json b/specifications/sums_even/manifest.json
index ebfafd93..e1cb23b6 100644
--- a/specifications/sums_even/manifest.json
+++ b/specifications/sums_even/manifest.json
@@ -26,10 +26,11 @@
     {
       "path": "specifications/sums_even/sums_even.tla",
       "communityDependencies": [],
-      "features": [
-        "proof"
-      ],
-      "models": []
+      "features": [],
+      "models": [],
+      "proof": {
+        "runtime": "00:00:01"
+      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/transaction_commit/manifest.json b/specifications/transaction_commit/manifest.json
index ad771823..f3aab2ae 100644
--- a/specifications/transaction_commit/manifest.json
+++ b/specifications/transaction_commit/manifest.json
@@ -78,4 +78,4 @@
       ]
     }
   ]
-}
+}
\ No newline at end of file