diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml
index b8e70d712be1..c9d130610447 100644
--- a/.azure-pipelines-templates/model_checking.yml
+++ b/.azure-pipelines-templates/model_checking.yml
@@ -31,6 +31,18 @@ jobs:
         workingDirectory: tla
         displayName: MCccfraftWithReconfig.cfg
 
+      - script: |
+          set -ex
+          python3.8 -m venv env
+          source env/bin/activate
+          python -m pip install -r requirements.txt
+          ls ../tla/*.json
+          python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft_stats.json
+        env:
+          METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION)
+        workingDirectory: tests
+        displayName: Uploading TLC stats to cimetrics
+
       - task: PublishPipelineArtifact@1
         inputs:
           artifactName: "Model Checking Traces"
diff --git a/metrics.yml b/metrics.yml
index d7834b71c03d..fe243e962460 100644
--- a/metrics.yml
+++ b/metrics.yml
@@ -10,4 +10,5 @@ monitoring_span: 150
 groups:
   "SGX": ".*_sgx_.*"
   "Virtual": ".*_virtual_.*"
+  "TLC": "tlc_.*"
   "Others": ".*"
diff --git a/tests/upload_tlc_stats.py b/tests/upload_tlc_stats.py
new file mode 100644
index 000000000000..f85ac7dc51e2
--- /dev/null
+++ b/tests/upload_tlc_stats.py
@@ -0,0 +1,46 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+# Licensed under the Apache 2.0 License.
+
+import json
+import os
+import argparse
+import cimetrics.upload
+
+from loguru import logger as LOG
+
+
+def run(test_label, filename):
+    if os.path.exists(filename):
+        with open(filename) as f:
+            data = json.load(f)
+            duration_sec = data["duration"]
+            dstates = data["distinct"]
+            LOG.info(
+                "Uploading metrics for {} - duration: {}, distinct states: {}",
+                test_label,
+                duration_sec,
+                dstates,
+            )
+            with cimetrics.upload.metrics(complete=False) as metrics:
+                metrics.put(f"tlc_{test_label}_duration_s", duration_sec)
+                metrics.put(f"tlc_{test_label}_states", dstates)
+
+    else:
+        LOG.warning(f"Could not find file {filename}: skipping metrics upload")
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(description="Upload TLC stats to cimetrics.")
+
+    parser.add_argument(
+        "test_label",
+        help="test name to upload metrics under",
+    )
+
+    parser.add_argument(
+        "filename",
+        help="TLC stats JSON file to upload",
+    )
+
+    args = parser.parse_args()
+    run(args.test_label, args.filename)
diff --git a/tla/.gitignore b/tla/.gitignore
index f6ead829812d..a9a5e5239d8a 100644
--- a/tla/.gitignore
+++ b/tla/.gitignore
@@ -12,4 +12,5 @@ tools/
 *.dot
 *TTrace*.tla
 *TTrace*.bin
-**/states.dump*
\ No newline at end of file
+*_stats.json
+**/states.dump*
diff --git a/tla/StatsFile.tla b/tla/StatsFile.tla
new file mode 100644
index 000000000000..8fd576267984
--- /dev/null
+++ b/tla/StatsFile.tla
@@ -0,0 +1,14 @@
+---- MODULE StatsFile----
+EXTENDS TLC, Json, Sequences
+
+\* Filename to write TLC stats to
+CONSTANT StatsFilename
+ASSUME StatsFilename \in STRING
+
+\* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format
+\* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking
+WriteStatsFile == 
+    /\ PrintT("Writing stats to file: " \o StatsFilename)
+    /\ ndJsonSerialize(StatsFilename, <<TLCGet("stats")>>)
+
+====
\ No newline at end of file
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
index c8a7312fb46d..5602cd0ed89d 100644
--- a/tla/consensus/MCccfraft.cfg
+++ b/tla/consensus/MCccfraft.cfg
@@ -7,6 +7,8 @@ CONSTANTS
     MaxTermLimit = 1
     MaxCommitsNotified = 0
     RequestLimit = 3
+
+    StatsFilename = "MCccfraft_stats.json"
     
     Timeout <- MCTimeout
     Send <- MCSend
@@ -50,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
index f6f1a1576c31..a1890a759340 100644
--- a/tla/consensus/MCccfraft.tla
+++ b/tla/consensus/MCccfraft.tla
@@ -1,5 +1,5 @@
 ---------- MODULE MCccfraft ----------
-EXTENDS ccfraft, TLC
+EXTENDS ccfraft, StatsFile
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree
@@ -21,6 +21,7 @@ ASSUME MaxCommitsNotified \in Nat
 CONSTANT RequestLimit
 ASSUME RequestLimit \in Nat
 
+
 ToServers ==
     UNION Range(Configurations)
 
@@ -137,4 +138,6 @@ AllReconfigurationsCommitted ==
 DebugAllReconfigurationsReachableInv ==
     ~AllReconfigurationsCommitted
 
+
+
 ===================================
\ No newline at end of file
diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
index fa0415237361..914b0e160935 100644
--- a/tla/consensus/MCccfraftAtomicReconfig.cfg
+++ b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -7,6 +7,8 @@ CONSTANTS
     MaxTermLimit = 4
     MaxCommitsNotified = 2
     RequestLimit = 3
+
+    StatsFilename = "MCccfraftAtomicReconfig_stats.json"
     
     Timeout <- MCTimeout
     Send <- MCSend
@@ -50,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
index 9768c626666e..f6890893c8b0 100644
--- a/tla/consensus/MCccfraftWithReconfig.cfg
+++ b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -6,7 +6,9 @@ CONSTANTS
 
     MaxTermLimit = 3
     MaxCommitsNotified = 2
-    RequestLimit = 3
+    RequestLimit = 2
+
+    StatsFilename = "MCccfraftWithReconfig_stats.json"
     
     Timeout <- MCTimeout
     Send <- MCSend
@@ -50,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp