diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py
index 449751e0..91e23909 100644
--- a/.github/scripts/generate_manifest.py
+++ b/.github/scripts/generate_manifest.py
@@ -93,7 +93,7 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
                     }
                     for cfg_path in sorted(get_cfg_files(examples_root, tla_path))
                 ]
-            } | ({'proof' : {'runtime': 'unknown'}} if 'proof' in module_features else {})
+            } | ({'proof' : {'maxRuntimeMinutes': 1}} if 'proof' in module_features else {})
             for tla_path, module_features in get_tla_file_features(examples_root, spec_path, parser, queries)
         ]
     }
@@ -133,7 +133,7 @@ def find_corresponding_model(old_model, new_module):
     return models[0] if any(models) else None
 
 def integrate_model_info(old_model, new_model):
-    fields = ['runtime', 'mode', 'result', 'distinctStates', 'totalStates', 'stateDepth']
+    fields = ['runtime', 'mode', 'result', 'distinctStates', 'totalStates', 'stateDepth', 'workers']
     for field in fields:
         if field in old_model:
             new_model[field] = old_model[field]
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 5c011373..14024a57 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -38,6 +38,9 @@ jobs:
         with:
           distribution: adopt
           java-version: 17
+      - name: Install timeout command
+        if: matrix.os == 'macos-latest'
+        run: brew install coreutils
       - name: Download TLA⁺ dependencies (Windows)
         if: matrix.os == 'windows-latest'
         run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR false
@@ -146,13 +149,12 @@ jobs:
             | map(select(has("proof")))
             # Failing on Linux
             | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
-            # Take too long to check in the CI
-            | map(select(.path != "specifications/byzpaxos/BPConProof.tla"))
-            | map(select(.path != "specifications/tcp/tcp_proof.tla"))
-            | map(.path + "\u0000")
+            # Skip long-running proofs in CI
+            | map(select(.proof.maxRuntimeMinutes <= 5))
+            | map((.proof.maxRuntimeMinutes | tostring) + "\u0000" + .path + "\u0000")
             | join("")' \
-          | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
-          time "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
+          | xargs --verbose --null --no-run-if-empty -n 2 \
+          sh -c 'time timeout --signal=KILL "${1}m" "$DEPS_DIR/tlapm/bin/tlapm" "$2" -I "$DEPS_DIR/community" --stretch 5' --
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 2bb8adad..80be51b4 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -45,7 +45,7 @@ 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 `models`
+   - Module proof runtime: if module contains formal proofs, record the estimated maximum time necessary to check the proofs with TLAPM on an underpowered workstation such as a CI runner machine; add `"proof" : { "maxRuntimeMinutes" : N }` to the module fields at the same level as `models`. If you have a relatively powerful machine this might up to twice the amount of time it takes locally. If your proof completes in only a couple seconds, put 1 for this value.
      - 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
diff --git a/manifest-schema.json b/manifest-schema.json
index c7a7d3ab..74608e75 100644
--- a/manifest-schema.json
+++ b/manifest-schema.json
@@ -29,13 +29,10 @@
           },
           "proof": {
             "type": "object",
-            "required": ["runtime"],
+            "required": ["maxRuntimeMinutes"],
             "additionalProperties": false,
             "properties": {
-              "runtime": {
-                "type": "string",
-                "pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$"
-              }
+              "maxRuntimeMinutes": {"type": "integer"}
             }
           },
           "models": {
diff --git a/specifications/Bakery-Boulangerie/manifest.json b/specifications/Bakery-Boulangerie/manifest.json
index 7661e764..6e007e2a 100644
--- a/specifications/Bakery-Boulangerie/manifest.json
+++ b/specifications/Bakery-Boulangerie/manifest.json
@@ -13,7 +13,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:20"
+        "maxRuntimeMinutes": 2
       }
     },
     {
@@ -23,7 +23,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:30"
+        "maxRuntimeMinutes": 3
       }
     },
     {
@@ -54,4 +54,4 @@
       ]
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/CigaretteSmokers/manifest.json b/specifications/CigaretteSmokers/manifest.json
index adf41a6e..3b90e782 100644
--- a/specifications/CigaretteSmokers/manifest.json
+++ b/specifications/CigaretteSmokers/manifest.json
@@ -39,7 +39,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/CoffeeCan/manifest.json b/specifications/CoffeeCan/manifest.json
index 3351b4bc..c18f9632 100644
--- a/specifications/CoffeeCan/manifest.json
+++ b/specifications/CoffeeCan/manifest.json
@@ -56,7 +56,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/DieHard/manifest.json b/specifications/DieHard/manifest.json
index 4f6c5cfd..c8176e87 100644
--- a/specifications/DieHard/manifest.json
+++ b/specifications/DieHard/manifest.json
@@ -36,6 +36,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/DieHard/DieHard_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/DieHard/DieHarder.tla",
       "features": [],
@@ -70,14 +78,6 @@
           "workers": 1
         }
       ]
-    },
-    {
-      "path": "specifications/DieHard/DieHard_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/Disruptor/manifest.json b/specifications/Disruptor/manifest.json
index 972d934f..f8432347 100644
--- a/specifications/Disruptor/manifest.json
+++ b/specifications/Disruptor/manifest.json
@@ -19,11 +19,6 @@
         }
       ]
     },
-    {
-      "path": "specifications/Disruptor/APRingBuffer.tla",
-      "features": [],
-      "models": []
-    },
     {
       "path": "specifications/Disruptor/APDisruptor_SPMC.tla",
       "features": [],
@@ -36,6 +31,11 @@
         }
       ]
     },
+    {
+      "path": "specifications/Disruptor/APRingBuffer.tla",
+      "features": [],
+      "models": []
+    },
     {
       "path": "specifications/Disruptor/Disruptor_MPMC.tla",
       "features": [],
diff --git a/specifications/FiniteMonotonic/manifest.json b/specifications/FiniteMonotonic/manifest.json
index acf3e508..114add7e 100644
--- a/specifications/FiniteMonotonic/manifest.json
+++ b/specifications/FiniteMonotonic/manifest.json
@@ -50,7 +50,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
diff --git a/specifications/KeyValueStore/manifest.json b/specifications/KeyValueStore/manifest.json
index 8df9452b..b7b66373 100644
--- a/specifications/KeyValueStore/manifest.json
+++ b/specifications/KeyValueStore/manifest.json
@@ -28,6 +28,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/KeyValueStore/MCKVS.tla",
       "features": [],
@@ -68,14 +76,6 @@
       "path": "specifications/KeyValueStore/Util.tla",
       "features": [],
       "models": []
-    },
-    {
-      "path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/LearnProofs/manifest.json b/specifications/LearnProofs/manifest.json
index 47c40a63..a4eaa9ec 100644
--- a/specifications/LearnProofs/manifest.json
+++ b/specifications/LearnProofs/manifest.json
@@ -14,7 +14,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -24,7 +24,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:10"
+        "maxRuntimeMinutes": 1
       }
     },
     {
diff --git a/specifications/LoopInvariance/manifest.json b/specifications/LoopInvariance/manifest.json
index 4e72970f..f5432fa5 100644
--- a/specifications/LoopInvariance/manifest.json
+++ b/specifications/LoopInvariance/manifest.json
@@ -16,7 +16,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -56,7 +56,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:05:00"
+        "maxRuntimeMinutes": 10
       }
     },
     {
@@ -66,8 +66,8 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:01:30"
+        "maxRuntimeMinutes": 3
       }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/Majority/manifest.json b/specifications/Majority/manifest.json
index 09b9d9fc..75e5b808 100644
--- a/specifications/Majority/manifest.json
+++ b/specifications/Majority/manifest.json
@@ -37,7 +37,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/MisraReachability/manifest.json b/specifications/MisraReachability/manifest.json
index 413cc249..85be147e 100644
--- a/specifications/MisraReachability/manifest.json
+++ b/specifications/MisraReachability/manifest.json
@@ -85,7 +85,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -98,7 +98,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -118,7 +118,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/MissionariesAndCannibals/manifest.json b/specifications/MissionariesAndCannibals/manifest.json
index b9331697..a7c75cf4 100644
--- a/specifications/MissionariesAndCannibals/manifest.json
+++ b/specifications/MissionariesAndCannibals/manifest.json
@@ -36,7 +36,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/MultiCarElevator/manifest.json b/specifications/MultiCarElevator/manifest.json
index 4a0035a5..216badd4 100644
--- a/specifications/MultiCarElevator/manifest.json
+++ b/specifications/MultiCarElevator/manifest.json
@@ -54,7 +54,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/Paxos/manifest.json b/specifications/Paxos/manifest.json
index 1aa8fb41..2f7627d3 100644
--- a/specifications/Paxos/manifest.json
+++ b/specifications/Paxos/manifest.json
@@ -10,7 +10,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -68,7 +68,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/PaxosHowToWinATuringAward/manifest.json b/specifications/PaxosHowToWinATuringAward/manifest.json
index 65ea44e7..760e5325 100644
--- a/specifications/PaxosHowToWinATuringAward/manifest.json
+++ b/specifications/PaxosHowToWinATuringAward/manifest.json
@@ -12,7 +12,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -76,7 +76,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -84,7 +84,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/ReadersWriters/manifest.json b/specifications/ReadersWriters/manifest.json
index 69f4d47e..76c31936 100644
--- a/specifications/ReadersWriters/manifest.json
+++ b/specifications/ReadersWriters/manifest.json
@@ -42,7 +42,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/SlidingPuzzles/manifest.json b/specifications/SlidingPuzzles/manifest.json
index 13c7d3ef..9a81b596 100644
--- a/specifications/SlidingPuzzles/manifest.json
+++ b/specifications/SlidingPuzzles/manifest.json
@@ -19,7 +19,7 @@
     },
     {
       "path": "specifications/SlidingPuzzles/SlidingPuzzles_anim.tla",
-      "features": [ ],
+      "features": [],
       "models": [
         {
           "path": "specifications/SlidingPuzzles/SlidingPuzzles_anim.cfg",
diff --git a/specifications/SpanningTree/manifest.json b/specifications/SpanningTree/manifest.json
index 23337fa9..c910fe20 100644
--- a/specifications/SpanningTree/manifest.json
+++ b/specifications/SpanningTree/manifest.json
@@ -70,7 +70,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/SpecifyingSystems/manifest.json b/specifications/SpecifyingSystems/manifest.json
index 738b150c..bbe041f7 100644
--- a/specifications/SpecifyingSystems/manifest.json
+++ b/specifications/SpecifyingSystems/manifest.json
@@ -110,6 +110,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel.tla",
       "features": [],
@@ -125,6 +133,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/AsynchronousInterface/PrintValues.tla",
       "features": [],
@@ -145,6 +161,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/CachingMemory/MCInternalMemory.tla",
       "features": [],
@@ -234,6 +258,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/Composing/Channel_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/Composing/CompositeFIFO.tla",
       "features": [],
@@ -244,11 +276,27 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/Composing/HourClock_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/Composing/InternalMemory.tla",
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/Composing/InternalMemory_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/Composing/JointActionMemory.tla",
       "features": [],
@@ -312,6 +360,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/FIFO/Channel_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/FIFO/FIFO.tla",
       "features": [],
@@ -327,6 +383,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/FIFO/InnerFIFO_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/FIFO/MCInnerFIFO.tla",
       "features": [],
@@ -396,6 +460,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/SpecifyingSystems/HourClock/HourClock_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/Liveness/APHourClock.tla",
       "features": [],
@@ -425,11 +497,27 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/Liveness/HourClock_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/Liveness/InternalMemory.tla",
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/Liveness/InternalMemory_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/Liveness/LiveHourClock.tla",
       "features": [],
@@ -510,11 +598,27 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/RealTime/HourClock_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/RealTime/InternalMemory.tla",
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/RealTime/InternalMemory_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/RealTime/MCRealTime.tla",
       "features": [],
@@ -652,6 +756,14 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/SpecifyingSystems/TLC/AlternatingBit_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/SpecifyingSystems/TLC/BNFGrammars.tla",
       "features": [],
@@ -676,118 +788,6 @@
           "stateDepth": 10
         }
       ]
-    },
-    {
-      "path": "specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/Composing/Channel_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/Composing/HourClock_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/Composing/InternalMemory_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/FIFO/Channel_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/FIFO/InnerFIFO_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/HourClock/HourClock_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/Liveness/HourClock_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/Liveness/InternalMemory_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/RealTime/HourClock_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/RealTime/InternalMemory_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/SpecifyingSystems/TLC/AlternatingBit_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/TLC/manifest.json b/specifications/TLC/manifest.json
index 384180ed..ca382e9c 100644
--- a/specifications/TLC/manifest.json
+++ b/specifications/TLC/manifest.json
@@ -5,13 +5,6 @@
   ],
   "tags": [],
   "modules": [
-    {
-      "path": "specifications/TLC/TLCMC.tla",
-      "features": [
-        "pluscal"
-      ],
-      "models": []
-    },
     {
       "path": "specifications/TLC/MCReachability.tla",
       "features": [],
@@ -22,6 +15,13 @@
       "features": [],
       "models": []
     },
+    {
+      "path": "specifications/TLC/TLCMC.tla",
+      "features": [
+        "pluscal"
+      ],
+      "models": []
+    },
     {
       "path": "specifications/TLC/TestGraphs.tla",
       "features": [],
diff --git a/specifications/TeachingConcurrency/manifest.json b/specifications/TeachingConcurrency/manifest.json
index d9f43b46..0a6b1f62 100644
--- a/specifications/TeachingConcurrency/manifest.json
+++ b/specifications/TeachingConcurrency/manifest.json
@@ -26,7 +26,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -46,7 +46,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -54,7 +54,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -62,7 +62,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/TwoPhase/manifest.json b/specifications/TwoPhase/manifest.json
index 8e2d4920..3f5fd626 100644
--- a/specifications/TwoPhase/manifest.json
+++ b/specifications/TwoPhase/manifest.json
@@ -31,7 +31,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -39,7 +39,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/acp/manifest.json b/specifications/acp/manifest.json
index 2fee9f4f..10a097a1 100644
--- a/specifications/acp/manifest.json
+++ b/specifications/acp/manifest.json
@@ -8,18 +8,6 @@
   ],
   "tags": [],
   "modules": [
-    {
-      "path": "specifications/acp/APACP_SB.tla",
-      "features": [],
-      "models": [
-        {
-          "path": "specifications/acp/APACP_SB.cfg",
-          "runtime": "00:00:10",
-          "mode": "symbolic",
-          "result": "success"
-        }
-      ]
-    },
     {
       "path": "specifications/acp/ACP_NB.tla",
       "features": [],
@@ -71,6 +59,18 @@
           "stateDepth": 21
         }
       ]
+    },
+    {
+      "path": "specifications/acp/APACP_SB.tla",
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/acp/APACP_SB.cfg",
+          "runtime": "00:00:10",
+          "mode": "symbolic",
+          "result": "success"
+        }
+      ]
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/allocator/manifest.json b/specifications/allocator/manifest.json
index c9fa93b1..5f88d650 100644
--- a/specifications/allocator/manifest.json
+++ b/specifications/allocator/manifest.json
@@ -20,6 +20,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/allocator/AllocatorImplementation_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 2
+      }
+    },
     {
       "path": "specifications/allocator/AllocatorRefinement.tla",
       "features": [],
@@ -50,6 +58,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/allocator/SchedulingAllocator_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 2
+      }
+    },
     {
       "path": "specifications/allocator/SimpleAllocator.tla",
       "features": [],
@@ -65,29 +81,13 @@
         }
       ]
     },
-    {
-      "path": "specifications/allocator/AllocatorImplementation_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/allocator/SchedulingAllocator_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
     {
       "path": "specifications/allocator/SimpleAllocator_proof.tla",
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/barriers/manifest.json b/specifications/barriers/manifest.json
index 4968fe1b..dfac6499 100644
--- a/specifications/barriers/manifest.json
+++ b/specifications/barriers/manifest.json
@@ -51,8 +51,8 @@
         }
       ],
       "proof": {
-        "runtime": "00:02:00"
+        "maxRuntimeMinutes": 10
       }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/bcastByz/manifest.json b/specifications/bcastByz/manifest.json
index b0d1a1b5..2ef08ff4 100644
--- a/specifications/bcastByz/manifest.json
+++ b/specifications/bcastByz/manifest.json
@@ -31,7 +31,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:01:15"
+        "maxRuntimeMinutes": 5
       }
     }
   ]
diff --git a/specifications/byihive/manifest.json b/specifications/byihive/manifest.json
index 0e501375..89e5c7fa 100644
--- a/specifications/byihive/manifest.json
+++ b/specifications/byihive/manifest.json
@@ -54,6 +54,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/byihive/VoucherLifeCycle_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/byihive/VoucherRedeem.tla",
       "features": [],
@@ -83,14 +91,6 @@
           "stateDepth": 11
         }
       ]
-    },
-    {
-      "path": "specifications/byihive/VoucherLifeCycle_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }
\ No newline at end of file
diff --git a/specifications/byzpaxos/manifest.json b/specifications/byzpaxos/manifest.json
index cc5bf18a..82dc824b 100644
--- a/specifications/byzpaxos/manifest.json
+++ b/specifications/byzpaxos/manifest.json
@@ -23,7 +23,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:10:00"
+        "maxRuntimeMinutes": 45
       }
     },
     {
@@ -43,7 +43,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -60,7 +60,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -80,7 +80,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:01:15"
+        "maxRuntimeMinutes": 3
       }
     }
   ]
diff --git a/specifications/dag-consensus/manifest.json b/specifications/dag-consensus/manifest.json
index ddbeb34e..b331049d 100644
--- a/specifications/dag-consensus/manifest.json
+++ b/specifications/dag-consensus/manifest.json
@@ -1,6 +1,10 @@
 {
-  "sources": ["https://github.com/nano-o/dag-consensus"],
-  "authors": ["Giuliano Losa"],
+  "sources": [
+    "https://github.com/nano-o/dag-consensus"
+  ],
+  "authors": [
+    "Giuliano Losa"
+  ],
   "tags": [],
   "modules": [
     {
@@ -65,4 +69,4 @@
       "models": []
     }
   ]
-}
+}
\ No newline at end of file
diff --git a/specifications/ewd687a/manifest.json b/specifications/ewd687a/manifest.json
index 9b40b71a..7216fed7 100644
--- a/specifications/ewd687a/manifest.json
+++ b/specifications/ewd687a/manifest.json
@@ -38,6 +38,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/ewd687a/EWD687a_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 3
+      }
+    },
     {
       "path": "specifications/ewd687a/MCEWD687a.tla",
       "features": [],
@@ -49,14 +57,6 @@
           "result": "success"
         }
       ]
-    },
-    {
-      "path": "specifications/ewd687a/EWD687a_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/ewd840/manifest.json b/specifications/ewd840/manifest.json
index a9567350..93c38027 100644
--- a/specifications/ewd840/manifest.json
+++ b/specifications/ewd840/manifest.json
@@ -84,7 +84,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:10"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -107,7 +107,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/ewd998/manifest.json b/specifications/ewd998/manifest.json
index 4fefc24c..dafe41cc 100644
--- a/specifications/ewd998/manifest.json
+++ b/specifications/ewd998/manifest.json
@@ -28,7 +28,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -134,6 +134,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/ewd998/EWD998PCal_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 10
+      }
+    },
     {
       "path": "specifications/ewd998/EWD998_anim.tla",
       "features": [],
@@ -154,7 +162,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:05:00"
+        "maxRuntimeMinutes": 2
       }
     },
     {
@@ -199,14 +207,6 @@
       "path": "specifications/ewd998/Utils.tla",
       "features": [],
       "models": []
-    },
-    {
-      "path": "specifications/ewd998/EWD998PCal_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }
diff --git a/specifications/glowingRaccoon/manifest.json b/specifications/glowingRaccoon/manifest.json
index 9cd85572..c3dab157 100644
--- a/specifications/glowingRaccoon/manifest.json
+++ b/specifications/glowingRaccoon/manifest.json
@@ -44,6 +44,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/glowingRaccoon/clean_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/glowingRaccoon/product.tla",
       "features": [],
@@ -74,20 +82,12 @@
         }
       ]
     },
-    {
-      "path": "specifications/glowingRaccoon/clean_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
     {
       "path": "specifications/glowingRaccoon/stages_proof.tla",
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/lamport_mutex/manifest.json b/specifications/lamport_mutex/manifest.json
index 86a5c322..2cf5848f 100644
--- a/specifications/lamport_mutex/manifest.json
+++ b/specifications/lamport_mutex/manifest.json
@@ -27,7 +27,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:05:00"
+        "maxRuntimeMinutes": 5
       }
     },
     {
@@ -46,4 +46,4 @@
       ]
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/locks_auxiliary_vars/manifest.json b/specifications/locks_auxiliary_vars/manifest.json
index 8b8c9f12..6d6c7b8d 100644
--- a/specifications/locks_auxiliary_vars/manifest.json
+++ b/specifications/locks_auxiliary_vars/manifest.json
@@ -24,7 +24,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -42,7 +42,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:30"
+        "maxRuntimeMinutes": 2
       }
     },
     {
@@ -62,7 +62,7 @@
         }
       ],
       "proof": {
-        "runtime": "00:00:30"
+        "maxRuntimeMinutes": 1
       }
     },
     {
@@ -71,4 +71,4 @@
       "models": []
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/spanning/manifest.json b/specifications/spanning/manifest.json
index 2bcd6641..c8dbf05e 100644
--- a/specifications/spanning/manifest.json
+++ b/specifications/spanning/manifest.json
@@ -41,7 +41,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/sums_even/manifest.json b/specifications/sums_even/manifest.json
index cdaff1a5..9a6dfbed 100644
--- a/specifications/sums_even/manifest.json
+++ b/specifications/sums_even/manifest.json
@@ -27,7 +27,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
diff --git a/specifications/tcp/manifest.json b/specifications/tcp/manifest.json
index 6005b98c..eb9caa02 100644
--- a/specifications/tcp/manifest.json
+++ b/specifications/tcp/manifest.json
@@ -19,6 +19,11 @@
         }
       ]
     },
+    {
+      "path": "specifications/tcp/IndInv_apa.tla",
+      "features": [],
+      "models": []
+    },
     {
       "path": "specifications/tcp/MCtcp.tla",
       "features": [],
@@ -34,11 +39,6 @@
         }
       ]
     },
-    {
-      "path": "specifications/tcp/IndInv_apa.tla",
-      "features": [],
-      "models": []
-    },
     {
       "path": "specifications/tcp/tcp.tla",
       "features": [],
@@ -49,8 +49,8 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:51:00"
+        "maxRuntimeMinutes": 60
       }
     }
   ]
-}
\ No newline at end of file
+}
diff --git a/specifications/transaction_commit/manifest.json b/specifications/transaction_commit/manifest.json
index cb31cf02..86006739 100644
--- a/specifications/transaction_commit/manifest.json
+++ b/specifications/transaction_commit/manifest.json
@@ -55,6 +55,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/transaction_commit/PaxosCommit_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 5
+      }
+    },
     {
       "path": "specifications/transaction_commit/TCommit.tla",
       "features": [],
@@ -70,6 +78,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/transaction_commit/TCommit_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/transaction_commit/TwoPhase.tla",
       "features": [],
@@ -85,29 +101,13 @@
         }
       ]
     },
-    {
-      "path": "specifications/transaction_commit/PaxosCommit_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
-    {
-      "path": "specifications/transaction_commit/TCommit_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
-    },
     {
       "path": "specifications/transaction_commit/TwoPhase_proof.tla",
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]
-}
\ No newline at end of file
+}