diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py
deleted file mode 100644
index 0e9e9601..00000000
--- a/.github/scripts/check_proofs.py
+++ /dev/null
@@ -1,92 +0,0 @@
-"""
-Validate all proofs in all modules with TLAPM.
-"""
-
-from argparse import ArgumentParser
-from datetime import timedelta
-from os.path import dirname, join, normpath
-import logging
-import subprocess
-from timeit import default_timer as timer
-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=False, default = 'deps/tlapm')
-parser.add_argument('--community_modules_path', help='Path to extracted community modules directory', required=False, default='')
-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 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)
-community_modules_path = normpath(args.community_modules_path) if args.community_modules_path else ''
-examples_root = args.examples_root
-manifest = tla_utils.load_all_manifests(examples_root)
-skip_modules = args.skip
-only_modules = args.only
-
-logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
-
-proof_module_paths = sorted(
-    [
-        (manifest_dir, spec, module, tla_utils.parse_timespan(module['proof']['runtime']))
-        for manifest_dir, spec in manifest
-        for module in spec['modules']
-        if 'proof' in module
-            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 manifest_dir, spec, module, expected_runtime in proof_module_paths:
-    module_path = module['path']
-    logging.info(module_path)
-    start_time = timer()
-    full_module_path = tla_utils.from_cwd(examples_root, module_path)
-    module_dir = dirname(full_module_path)
-    try:
-        tlapm_args = [
-            tlapm_path, full_module_path,
-            '-I', module_dir,
-            '--stretch', '5'
-        ]
-        if community_modules_path:
-            tlapm_args.extend(['-I', community_modules_path])
-        tlapm_result = subprocess.run(
-            tlapm_args,
-            stdout  = subprocess.PIPE,
-            stderr  = subprocess.STDOUT,
-            text    = True
-        )
-        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 = '' if tlapm_result.stdout is None else 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
-
-exit(0 if success else 1)
-
diff --git a/DEVELOPING.md b/DEVELOPING.md
index 7b1d083b..49d7079a 100644
--- a/DEVELOPING.md
+++ b/DEVELOPING.md
@@ -22,7 +22,6 @@ Here is a brief overview of each script in the order they are run in [the CI](.g
    The script ensures the models don't crash and that their result is as expected, either success or a specific type of failure.
    If applicable, the script also checks the size of the state graph against the values recorded in `manifest.json`.
 1. [`smoke_test_large_models.py`](.github/scripts/smoke_test_large_models.py): not all models in this repository can be run to completion within 30 seconds, so this script runs medium & large models for five seconds before terminating their process - just to ensure they basically function and don't immediately crash.
-1. [`check_proofs.py`](.github/scripts/check_proofs.py): this script runs TLAPM against all modules that contain formal proofs, to ensure the proofs are valid.
 
 There are also a number of utility scripts:
 1. [`generate_manifest.py`](.github/scripts/generate_manifest.py): this can be run by users to automatically generate a new `manifest.json` file for their specs.
@@ -82,10 +81,6 @@ python .github/scripts/check_small_models.py --tools_jar_path deps/tools/tla2too
 ```sh
 python .github/scripts/smoke_test_large_models.py --tools_jar_path deps/tools/tla2tools.jar --apalache_path deps/apalache --tlapm_lib_path deps/tlapm/library --community_modules_jar_path deps/community/modules.jar --examples_root .
 ```
-Note: `check_proofs.py` does not run on Windows.
-```sh
-python .github/scripts/check_proofs.py --tlapm_path deps/tlapm --examples_root .
-```
 You can also run the non-CI utility scripts as follows:
 ```sh
 python .github/scripts/generate_manifest.py --ci_ignore_path .ciignore