SERVER-43589 Trace logging for RaftMongo.tla

29 files changed, 443 insertions, 168 deletions

diff --git a/src/mongo/db/pipeline/document_source_check_resume_token.cpp b/src/mongo/db/pipeline/document_source_check_resume_token.cpp
index 239d3096c66..c88bd0da724 100644
--- a/src/mongo/db/pipeline/document_source_check_resume_token.cpp
+++ b/src/mongo/db/pipeline/document_source_check_resume_token.cpp
@@ -31,6 +31,7 @@
 
 #include "mongo/db/curop.h"
 #include "mongo/db/pipeline/document_source_check_resume_token.h"
+#include "mongo/db/repl/oplog_entry.h"
 
 using boost::intrusive_ptr;
 namespace mongo {
@@ -333,8 +334,9 @@ void DocumentSourceShardCheckResumability::_assertOplogHasEnoughHistory(
         // if its timestamp is later than the resume token. No events earlier than the token can
         // have fallen off this oplog, and it is therefore safe to resume. Otherwise, verify that
         // the timestamp of the first oplog entry is earlier than that of the resume token.
+        using repl::kInitiatingSetMsg;
         const bool isNewRS =
-            Value::compare(firstOplogEntry["o"]["msg"], Value("initiating set"_sd), nullptr) == 0 &&
+            Value::compare(firstOplogEntry["o"]["msg"], Value(kInitiatingSetMsg), nullptr) == 0 &&
             Value::compare(firstOplogEntry["op"], Value("n"_sd), nullptr) == 0;
         uassert(ErrorCodes::ChangeStreamFatalError,
                 "Resume of change stream was not possible, as the resume point may no longer be in "
diff --git a/src/mongo/db/repl/SConscript b/src/mongo/db/repl/SConscript
index 5ad50fdb6e2..a3353f63b1e 100644
--- a/src/mongo/db/repl/SConscript
+++ b/src/mongo/db/repl/SConscript
@@ -58,6 +58,7 @@ env.Library(
         '$BUILD_DIR/mongo/db/transaction',
         '$BUILD_DIR/mongo/idl/idl_parser',
         '$BUILD_DIR/mongo/rpc/command_status',
+        '$BUILD_DIR/mongo/util/tla_plus_trace',
     ],
 )
 
@@ -551,22 +552,6 @@ env.Library(
     LIBDEPS_PRIVATE=[
         '$BUILD_DIR/mongo/db/commands/mongod_fsync',
         'replication_auth',
-        'tla_plus_trace_repl',
-    ],
-)
-
-env.Library(
-    target='tla_plus_trace_repl',
-    source=[
-        'tla_plus_trace_repl.cpp',
-        env.Idlc('tla_plus_trace_repl.idl')[0],
-    ],
-    LIBDEPS=[
-        '$BUILD_DIR/mongo/base',
-        '$BUILD_DIR/mongo/db/server_options',
-        '$BUILD_DIR/mongo/idl/idl_parser',
-        '$BUILD_DIR/mongo/util/fail_point',
-        'repl_coordinator_interface',
     ],
 )
 
@@ -656,8 +641,10 @@ env.Library(
         'replication_coordinator_impl.cpp',
         'replication_coordinator_impl_elect_v1.cpp',
         'replication_coordinator_impl_heartbeat.cpp',
+        'replication_coordinator_impl_tla_plus_trace.cpp',
         'vote_requester.cpp',
-        env.Idlc("replication_coordinator_impl.idl")[0],
+        env.Idlc('replication_coordinator_impl.idl')[0],
+        env.Idlc('tla_plus_trace_repl.idl')[0],
     ],
     LIBDEPS=[
         '$BUILD_DIR/mongo/db/common',
@@ -688,6 +675,7 @@ env.Library(
         '$BUILD_DIR/mongo/db/commands/test_commands_enabled',
         '$BUILD_DIR/mongo/db/index_builds_coordinator_interface',
         '$BUILD_DIR/mongo/idl/server_parameter',
+        '$BUILD_DIR/mongo/util/tla_plus_trace',
     ],
 )
 
@@ -1184,10 +1172,11 @@ env.Library(
         'rollback_source_impl',
     ],
     LIBDEPS_PRIVATE=[
-        'repl_server_parameters',
         '$BUILD_DIR/mongo/db/commands/mongod_fcv',
         '$BUILD_DIR/mongo/db/commands/test_commands_enabled',
         '$BUILD_DIR/mongo/db/index_builds_coordinator_interface',
+        '$BUILD_DIR/mongo/util/tla_plus_trace',
+        'repl_server_parameters',
     ],
 )
 
diff --git a/src/mongo/db/repl/oplog_applier_impl.cpp b/src/mongo/db/repl/oplog_applier_impl.cpp
index b036bad722b..ab42b32502a 100644
--- a/src/mongo/db/repl/oplog_applier_impl.cpp
+++ b/src/mongo/db/repl/oplog_applier_impl.cpp
@@ -43,7 +43,6 @@
 #include "mongo/db/logical_session_id.h"
 #include "mongo/db/repl/apply_ops.h"
 #include "mongo/db/repl/insert_group.h"
-#include "mongo/db/repl/tla_plus_trace_repl.h"
 #include "mongo/db/repl/transaction_oplog_application.h"
 #include "mongo/db/stats/timer_stats.h"
 #include "mongo/platform/basic.h"
@@ -475,6 +474,12 @@ void OplogApplierImpl::_run(OplogBuffer* oplogBuffer) {
                                 << lastAppliedOpTimeAtEndOfBatch.toString()
                                 << " in the middle of batch application");
 
+
+        // For RaftMongo.tla trace-checking, dump the oplog including new entries, before the new
+        // entries are visible and cause other RaftMongo events.
+        _replCoord->tlaPlusRaftMongoEvent(
+            &opCtx, RaftMongoSpecActionEnum::kAppendOplog, lastOpTimeInBatch.getTimestamp());
+
         // 3. Update oplog visibility by notifying the storage engine of the new oplog entries.
         const bool orderedCommit = true;
         _storageInterface->oplogDiskLocRegister(
@@ -673,10 +678,6 @@ StatusWith<OpTime> OplogApplierImpl::_applyOplogBatch(OperationContext* opCtx,
         }
     }
 
-    if (MONGO_unlikely(logForTLAPlusSpecs.shouldFail())) {
-        tlaPlusRaftMongoEvent(opCtx, RaftMongoSpecActionEnum::kAppendOplog);
-    }
-
     // Tell the storage engine to flush the journal now that a replication batch has completed. This
     // means that all the writes associated with the oplog entries in the batch are finished and no
     // new writes with timestamps associated with those oplog entries will show up in the future. We
diff --git a/src/mongo/db/repl/oplog_entry.h b/src/mongo/db/repl/oplog_entry.h
index f298614b11b..c01b2766d1b 100644
--- a/src/mongo/db/repl/oplog_entry.h
+++ b/src/mongo/db/repl/oplog_entry.h
@@ -40,6 +40,11 @@ namespace mongo {
 namespace repl {
 
 /**
+ * The first oplog entry is a no-op with this message in its "msg" field.
+ */
+constexpr auto kInitiatingSetMsg = "initiating set"_sd;
+
+/**
  * A parsed DurableReplOperation along with information about the operation that should only exist
  * in-memory.
  *
diff --git a/src/mongo/db/repl/replication_coordinator.h b/src/mongo/db/repl/replication_coordinator.h
index dbddf496bfd..0d35d3c3e8d 100644
--- a/src/mongo/db/repl/replication_coordinator.h
+++ b/src/mongo/db/repl/replication_coordinator.h
@@ -41,6 +41,7 @@
 #include "mongo/db/repl/repl_settings.h"
 #include "mongo/db/repl/split_horizon.h"
 #include "mongo/db/repl/sync_source_selector.h"
+#include "mongo/db/repl/tla_plus_trace_repl_gen.h"
 #include "mongo/db/repl/topology_version_gen.h"
 #include "mongo/util/net/hostandport.h"
 #include "mongo/util/time_support.h"
@@ -791,7 +792,7 @@ public:
     /**
      * Returns the current term.
      */
-    virtual long long getTerm() = 0;
+    virtual long long getTerm() const = 0;
 
     /**
      * Attempts to update the current term for the V1 election protocol. If the term changes and
@@ -953,6 +954,14 @@ public:
         TopologyVersion previous,
         Date_t deadline) = 0;
 
+    /**
+     * Trace a replication event for the RaftMongo.tla spec.
+     */
+    virtual void tlaPlusRaftMongoEvent(
+        OperationContext* opCtx,
+        RaftMongoSpecActionEnum action,
+        boost::optional<Timestamp> oplogReadTimestamp = boost::none) const {}
+
 protected:
     ReplicationCoordinator();
 };
diff --git a/src/mongo/db/repl/replication_coordinator_external_state_impl.cpp b/src/mongo/db/repl/replication_coordinator_external_state_impl.cpp
index f300d875cce..a35da52da17 100644
--- a/src/mongo/db/repl/replication_coordinator_external_state_impl.cpp
+++ b/src/mongo/db/repl/replication_coordinator_external_state_impl.cpp
@@ -109,6 +109,7 @@
 #include "mongo/util/scopeguard.h"
 #include "mongo/util/str.h"
 #include "mongo/util/time_support.h"
+#include "mongo/util/tla_plus_trace.h"
 
 namespace mongo {
 namespace repl {
@@ -409,8 +410,7 @@ Status ReplicationCoordinatorExternalStateImpl::initializeReplSetStorage(Operati
 
                                WriteUnitOfWork wuow(opCtx);
                                Helpers::putSingleton(opCtx, configCollectionName, config);
-                               const auto msgObj = BSON("msg"
-                                                        << "initiating set");
+                               const auto msgObj = BSON("msg" << kInitiatingSetMsg);
                                _service->getOpObserver()->onOpMessage(opCtx, msgObj);
                                wuow.commit();
                                // ReplSetTest assumes that immediately after the replSetInitiate
@@ -419,12 +419,17 @@ Status ReplicationCoordinatorExternalStateImpl::initializeReplSetStorage(Operati
                                // fail if it finds its sync source has an empty oplog.  Thus, we
                                // need to wait here until the seed document is visible in our oplog.
                                _storageInterface->waitForAllEarlierOplogWritesToBeVisible(opCtx);
+                               if (MONGO_unlikely(logForTLAPlusSpecs.shouldFail())) {
+                                   repl::ReplicationCoordinator::get(opCtx)->tlaPlusRaftMongoEvent(
+                                       opCtx, repl::RaftMongoSpecActionEnum::kReplSetInitiate);
+                               }
                            });
 
         FeatureCompatibilityVersion::setIfCleanStartup(opCtx, _storageInterface);
     } catch (const DBException& ex) {
         return ex.toStatus();
     }
+
     return Status::OK();
 }
 
diff --git a/src/mongo/db/repl/replication_coordinator_impl.cpp b/src/mongo/db/repl/replication_coordinator_impl.cpp
index cc62c73fe94..889d385fafd 100644
--- a/src/mongo/db/repl/replication_coordinator_impl.cpp
+++ b/src/mongo/db/repl/replication_coordinator_impl.cpp
@@ -73,6 +73,7 @@
 #include "mongo/db/repl/replication_process.h"
 #include "mongo/db/repl/rslog.h"
 #include "mongo/db/repl/storage_interface.h"
+#include "mongo/db/repl/tla_plus_trace_repl_gen.h"
 #include "mongo/db/repl/topology_coordinator.h"
 #include "mongo/db/repl/transaction_oplog_application.h"
 #include "mongo/db/repl/update_position_args.h"
@@ -92,6 +93,7 @@
 #include "mongo/util/stacktrace.h"
 #include "mongo/util/time_support.h"
 #include "mongo/util/timer.h"
+#include "mongo/util/tla_plus_trace.h"
 
 namespace mongo {
 namespace repl {
@@ -981,6 +983,7 @@ void ReplicationCoordinatorImpl::signalDrainComplete(OperationContext* opCtx,
     if (_applierState != ApplierState::Draining) {
         return;
     }
+    _tlaPlusRaftMongoEvent(lk, opCtx, RaftMongoSpecActionEnum::kBecomePrimaryByMagic);
     lk.unlock();
 
     _externalState->onDrainComplete(opCtx);
@@ -3554,6 +3557,12 @@ bool ReplicationCoordinatorImpl::shouldChangeSyncSource(
 void ReplicationCoordinatorImpl::_updateLastCommittedOpTimeAndWallTime(WithLock lk) {
     if (_topCoord->updateLastCommittedOpTimeAndWallTime()) {
         _setStableTimestampForStorage(lk);
+        if (MONGO_unlikely(logForTLAPlusSpecs.shouldFail())) {
+            EnsureOperationContext ensureOpCtx;
+            _tlaPlusRaftMongoEvent(lk,
+                                   ensureOpCtx.getOperationContext(),
+                                   RaftMongoSpecActionEnum::kAdvanceCommitPoint);
+        }
     }
 }
 
@@ -3795,6 +3804,15 @@ void ReplicationCoordinatorImpl::_advanceCommitPoint(
         }
 
         _setStableTimestampForStorage(lk);
+        if (MONGO_unlikely(logForTLAPlusSpecs.shouldFail())) {
+            EnsureOperationContext ensureOpCtx;
+            auto action = fromSyncSource
+                ? RaftMongoSpecActionEnum::kLearnCommitPointFromSyncSourceNeverBeyondLastApplied
+                : RaftMongoSpecActionEnum::kLearnCommitPointWithTermCheck;
+
+            _tlaPlusRaftMongoEvent(lk, ensureOpCtx.getOperationContext(), action);
+        }
+
         // Even if we have no new snapshot, we need to notify waiters that the commit point moved.
         _externalState->notifyOplogMetadataWaiters(committedOpTimeAndWallTime.opTime);
     }
@@ -3957,7 +3975,7 @@ Status ReplicationCoordinatorImpl::processHeartbeatV1(const ReplSetHeartbeatArgs
     return result;
 }
 
-long long ReplicationCoordinatorImpl::getTerm() {
+long long ReplicationCoordinatorImpl::getTerm() const {
     // Note: no mutex acquisition here, as we are reading an Atomic variable.
     return _termShadow.load();
 }
diff --git a/src/mongo/db/repl/replication_coordinator_impl.h b/src/mongo/db/repl/replication_coordinator_impl.h
index 78389986f77..5e5476a075e 100644
--- a/src/mongo/db/repl/replication_coordinator_impl.h
+++ b/src/mongo/db/repl/replication_coordinator_impl.h
@@ -45,8 +45,10 @@
 #include "mongo/db/repl/replication_coordinator.h"
 #include "mongo/db/repl/replication_coordinator_external_state.h"
 #include "mongo/db/repl/sync_source_resolver.h"
+#include "mongo/db/repl/tla_plus_trace_repl_gen.h"
 #include "mongo/db/repl/topology_coordinator.h"
 #include "mongo/db/repl/update_position_args.h"
+#include "mongo/db/service_context.h"
 #include "mongo/executor/task_executor.h"
 #include "mongo/platform/atomic_word.h"
 #include "mongo/platform/random.h"
@@ -292,7 +294,7 @@ public:
     /**
      * Get current term from topology coordinator
      */
-    virtual long long getTerm() override;
+    virtual long long getTerm() const override;
 
     // Returns the ServiceContext where this instance runs.
     virtual ServiceContext* getServiceContext() override {
@@ -344,6 +346,11 @@ public:
         TopologyVersion previous,
         Date_t deadline) override;
 
+    void tlaPlusRaftMongoEvent(
+        OperationContext* opCtx,
+        RaftMongoSpecActionEnum action,
+        boost::optional<Timestamp> oplogReadTimestamp = boost::none) const override;
+
     // ================== Test support API ===================
 
     /**
@@ -720,6 +727,26 @@ private:
         AtomicWord<unsigned> _canServeNonLocalReads;
     };
 
+    // Inner class to ensure an opCtx is available in a scope.
+    class EnsureOperationContext {
+    public:
+        EnsureOperationContext() : _opCtxPtr(cc().getOperationContext()) {
+            if (!_opCtxPtr) {
+                // The UniqueOperationContext's deleter will call cc().resetOperationContext().
+                _tmpOpCtx = cc().makeOperationContext();
+                _opCtxPtr = _tmpOpCtx.get();
+            }
+        }
+
+        OperationContext* getOperationContext() const {
+            return _opCtxPtr;
+        }
+
+    private:
+        ServiceContext::UniqueOperationContext _tmpOpCtx;
+        OperationContext* _opCtxPtr;
+    };
+
     void _resetMyLastOpTimes(WithLock lk);
 
     /**
@@ -1335,6 +1362,15 @@ private:
      */
     int64_t _nextRandomInt64_inlock(int64_t limit);
 
+    /**
+     * Trace a replication event for the RaftMongo.tla spec.
+     */
+    void _tlaPlusRaftMongoEvent(WithLock,
+                                OperationContext* opCtx,
+                                RaftMongoSpecActionEnum action,
+                                boost::optional<Timestamp> oplogReadTimestamp = boost::none) const
+        noexcept;
+
     //
     // All member variables are labeled with one of the following codes indicating the
     // synchronization rules for accessing them.
diff --git a/src/mongo/db/repl/replication_coordinator_impl_tla_plus_trace.cpp b/src/mongo/db/repl/replication_coordinator_impl_tla_plus_trace.cpp
new file mode 100644
index 00000000000..43d32d26d6c
--- /dev/null
+++ b/src/mongo/db/repl/replication_coordinator_impl_tla_plus_trace.cpp
@@ -0,0 +1,144 @@
+/**
+ *    Copyright (C) 2019-present MongoDB, Inc.
+ *
+ *    This program is free software: you can redistribute it and/or modify
+ *    it under the terms of the Server Side Public License, version 1,
+ *    as published by MongoDB, Inc.
+ *
+ *    This program is distributed in the hope that it will be useful,
+ *    but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ *    Server Side Public License for more details.
+ *
+ *    You should have received a copy of the Server Side Public License
+ *    along with this program. If not, see
+ *    <http://www.mongodb.com/licensing/server-side-public-license>.
+ *
+ *    As a special exception, the copyright holders give permission to link the
+ *    code of portions of this program with the OpenSSL library under certain
+ *    conditions as described in each individual source file and distribute
+ *    linked combinations including the program with the OpenSSL library. You
+ *    must comply with the Server Side Public License in all respects for
+ *    all of the code used other than as permitted herein. If you modify file(s)
+ *    with this exception, you may extend this exception to your version of the
+ *    file(s), but you are not obligated to do so. If you do not wish to do so,
+ *    delete this exception statement from your version. If you delete this
+ *    exception statement from all source files in the program, then also delete
+ *    it in the license file.
+ */
+
+#define MONGO_LOG_DEFAULT_COMPONENT ::mongo::logger::LogComponent::kTlaPlusTrace
+
+#include "mongo/platform/basic.h"
+
+#include "mongo/db/client.h"
+#include "mongo/db/db_raii.h"
+#include "mongo/db/repl/replication_coordinator_impl.h"
+#include "mongo/db/repl/tla_plus_trace_repl_gen.h"
+#include "mongo/db/storage/kv/kv_engine.h"
+#include "mongo/util/log.h"
+#include "mongo/util/tla_plus_trace.h"
+
+namespace mongo::repl {
+
+void ReplicationCoordinatorImpl::tlaPlusRaftMongoEvent(
+    OperationContext* opCtx,
+    RaftMongoSpecActionEnum action,
+    boost::optional<Timestamp> oplogReadTimestamp) const {
+    if (MONGO_unlikely(logForTLAPlusSpecs.shouldFail())) {
+        stdx::unique_lock<Latch> lk(_mutex);
+        _tlaPlusRaftMongoEvent(lk, opCtx, action, oplogReadTimestamp);
+    }
+}
+
+void ReplicationCoordinatorImpl::_tlaPlusRaftMongoEvent(
+    WithLock,
+    OperationContext* opCtx,
+    RaftMongoSpecActionEnum action,
+    boost::optional<Timestamp> oplogReadTimestamp) const noexcept {
+    if (MONGO_unlikely(
+            logForTLAPlusSpecs.scopedIf(enabledForSpec(TLAPlusSpecEnum::kRaftMongo)).isActive())) {
+        auto actionName = RaftMongoSpecAction_serializer(action);
+
+        ShouldNotConflictWithSecondaryBatchApplicationBlock noConflict(opCtx->lockState());
+
+        // Read the oplog collection without using DBLock or AutoGetCollectionForRead, they take
+        // RSTL while we hold _mutex, which is the wrong lock order and risks deadlock. We don't
+        // need the RSTL because _mutex protects us from state changes. Global IS lock should
+        // suffice to read the oplog, but lock the DB and collection so we can read from the oplog
+        // and prevent a rollback from truncating it while we read.
+        // TODO (SERVER-44906): Remove db and collection locks.
+        LOG(2) << "Getting global lock in IS mode to log " << actionName << " for RaftMongo.tla";
+
+        opCtx->lockState()->lockGlobal(opCtx, MODE_IS);
+        ON_BLOCK_EXIT([&opCtx]() { opCtx->lockState()->unlockGlobal(); });
+
+        const auto oplogNs = NamespaceString::kRsOplogNamespace;
+        const auto dbResource = ResourceId(RESOURCE_DATABASE, oplogNs.db());
+        opCtx->lockState()->lock(opCtx, dbResource, MODE_IS);
+        ON_BLOCK_EXIT([&opCtx, &dbResource]() { opCtx->lockState()->unlock(dbResource); });
+
+        const auto collResource = ResourceId(RESOURCE_COLLECTION, oplogNs.ns());
+        opCtx->lockState()->lock(opCtx, collResource, MODE_IS);
+        ON_BLOCK_EXIT([&opCtx, &collResource]() { opCtx->lockState()->unlock(collResource); });
+
+        auto oplogCollection =
+            CollectionCatalog::get(opCtx).lookupCollectionByNamespace(opCtx, oplogNs);
+        invariant(oplogCollection);
+
+        // If the recovery unit is inactive, ensure it's still inactive after this function.
+        std::unique_ptr<RecoveryUnit> oldRecoveryUnit;
+        auto oldRecoveryUnitState = WriteUnitOfWork::RecoveryUnitState::kNotInUnitOfWork;
+        if (opCtx->recoveryUnit()->getState() == RecoveryUnit::State::kInactive) {
+            oldRecoveryUnit = opCtx->releaseRecoveryUnit();
+            oldRecoveryUnitState = opCtx->setRecoveryUnit(
+                std::unique_ptr<RecoveryUnit>(
+                    opCtx->getServiceContext()->getStorageEngine()->newRecoveryUnit()),
+                WriteUnitOfWork::RecoveryUnitState::kNotInUnitOfWork);
+        }
+
+        ON_BLOCK_EXIT([&opCtx, &oldRecoveryUnit, &oldRecoveryUnitState]() {
+            if (oldRecoveryUnit) {
+                opCtx->setRecoveryUnit(std::move(oldRecoveryUnit), oldRecoveryUnitState);
+            };
+        });
+
+        auto oplogRecordStore = oplogCollection->getRecordStore();
+        auto isPrimary = _getMemberState_inlock() == MemberState::RS_PRIMARY;
+        auto serverState = isPrimary ? RaftMongoSpecServerStateEnum::kLeader
+                                     : RaftMongoSpecServerStateEnum::kFollower;
+
+        LOG(2) << "Going to log " << actionName << " as "
+               << RaftMongoSpecServerState_serializer(serverState)
+               << " for RaftMongo.tla, reading oplog with timestamp " << oplogReadTimestamp;
+
+        // On a primary, read the oplog forward with default oplog visibility rules. Same on a
+        // secondary, but if a timestamp is provided, read backwards to see all entries.
+        auto backward = oplogReadTimestamp.has_value();
+        auto cursor = oplogRecordStore->getCursor(opCtx, !backward);
+        std::vector<OpTime> entryOpTimes;
+        while (auto record = cursor->next()) {
+            auto opTime = OplogEntry(record.get().data.toBson()).getOpTime();
+            if (!oplogReadTimestamp || oplogReadTimestamp >= opTime.getTimestamp()) {
+                entryOpTimes.emplace_back(opTime);
+            }
+        }
+
+        TlaPlusTraceEvent event;
+        event.setSpec(TLAPlusSpecEnum::kRaftMongo);
+        event.setAction(RaftMongoSpecAction_serializer(action));
+
+        RaftMongoSpecEvent raftEvent;
+        raftEvent.setServerState(serverState);
+        raftEvent.setCommitPoint(_topCoord->getLastCommittedOpTime());
+        raftEvent.setTerm(getTerm());
+
+        if (backward) {
+            std::reverse(entryOpTimes.begin(), entryOpTimes.end());
+        }
+        raftEvent.setLog(entryOpTimes);
+        event.setState(raftEvent.toBSON());
+        logTlaPlusTraceEvent(event);
+    }
+}
+}  // namespace mongo::repl
diff --git a/src/mongo/db/repl/replication_coordinator_mock.cpp b/src/mongo/db/repl/replication_coordinator_mock.cpp
index 34866d8aee9..ba14eb1c1ce 100644
--- a/src/mongo/db/repl/replication_coordinator_mock.cpp
+++ b/src/mongo/db/repl/replication_coordinator_mock.cpp
@@ -480,7 +480,7 @@ bool ReplicationCoordinatorMock::getWriteConcernMajorityShouldJournal() {
     return true;
 }
 
-long long ReplicationCoordinatorMock::getTerm() {
+long long ReplicationCoordinatorMock::getTerm() const {
     return _term;
 }
 
diff --git a/src/mongo/db/repl/replication_coordinator_mock.h b/src/mongo/db/repl/replication_coordinator_mock.h
index 7ba8f65c2c3..cdbd5fab445 100644
--- a/src/mongo/db/repl/replication_coordinator_mock.h
+++ b/src/mongo/db/repl/replication_coordinator_mock.h
@@ -256,7 +256,7 @@ public:
 
     virtual bool getWriteConcernMajorityShouldJournal();
 
-    virtual long long getTerm();
+    virtual long long getTerm() const;
 
     virtual Status updateTerm(OperationContext* opCtx, long long term);
 
diff --git a/src/mongo/db/repl/replication_coordinator_noop.cpp b/src/mongo/db/repl/replication_coordinator_noop.cpp
index 9cd64d94b5a..68701956af1 100644
--- a/src/mongo/db/repl/replication_coordinator_noop.cpp
+++ b/src/mongo/db/repl/replication_coordinator_noop.cpp
@@ -416,7 +416,7 @@ Status ReplicationCoordinatorNoOp::processHeartbeatV1(const ReplSetHeartbeatArgs
     MONGO_UNREACHABLE;
 }
 
-long long ReplicationCoordinatorNoOp::getTerm() {
+long long ReplicationCoordinatorNoOp::getTerm() const {
     MONGO_UNREACHABLE;
 }
 
diff --git a/src/mongo/db/repl/replication_coordinator_noop.h b/src/mongo/db/repl/replication_coordinator_noop.h
index 9f3cf5eee0b..50bea2c4ec4 100644
--- a/src/mongo/db/repl/replication_coordinator_noop.h
+++ b/src/mongo/db/repl/replication_coordinator_noop.h
@@ -219,7 +219,7 @@ public:
 
     void dropAllSnapshots() final;
 
-    long long getTerm() final;
+    long long getTerm() const final;
 
     Status updateTerm(OperationContext*, long long) final;
 
diff --git a/src/mongo/db/repl/rollback_impl.cpp b/src/mongo/db/repl/rollback_impl.cpp
index 4bfdb8dd2d8..b94f350d503 100644
--- a/src/mongo/db/repl/rollback_impl.cpp
+++ b/src/mongo/db/repl/rollback_impl.cpp
@@ -541,6 +541,7 @@ void RollbackImpl::_runPhaseFromAbortToReconstructPreparedTxns(
     // collection counts, reconstruct the prepared transactions now, adding on any additional counts
     // to the now corrected record store.
     reconstructPreparedTransactions(opCtx, OplogApplication::Mode::kRecovering);
+    _replicationCoordinator->tlaPlusRaftMongoEvent(opCtx, RaftMongoSpecActionEnum::kRollbackOplog);
 }
 
 void RollbackImpl::_correctRecordStoreCounts(OperationContext* opCtx) {
diff --git a/src/mongo/db/repl/tla_plus_trace_repl.idl b/src/mongo/db/repl/tla_plus_trace_repl.idl
index 10713e1a8c7..4fc5da794bb 100644
--- a/src/mongo/db/repl/tla_plus_trace_repl.idl
+++ b/src/mongo/db/repl/tla_plus_trace_repl.idl
@@ -26,41 +26,50 @@
 # it in the license file.
 #
 
-# TLA+ Trace Checker Event IDL File
+# RaftMongo.tla Trace Events
 
 global:
-    cpp_namespace: "mongo"
+    cpp_namespace: "mongo::repl"
 
 imports:
     - "mongo/idl/basic_types.idl"
-    - "mongo/util/net/hostandport.idl"
+    - "mongo/db/repl/replication_types.idl"
+    - "mongo/util/tla_plus_trace.idl"
 
 enums:
-    TLAPlusSpec:
-        description: "The supported TLA+ specs."
+    RaftMongoSpecAction:
+        description: "The supported actions in the RaftMongo.tla spec."
         type: string
         values:
-            kRaftMongo: "RaftMongo"
+            kAdvanceCommitPoint: "AdvanceCommitPoint"
+            kAppendOplog: "AppendOplog"
+            kBecomePrimaryByMagic: "BecomePrimaryByMagic"
+            kClientWrite: "ClientWrite"
+            kLearnCommitPointFromSyncSourceNeverBeyondLastApplied: "LearnCommitPointFromSyncSourceNeverBeyondLastApplied"
+            kLearnCommitPointWithTermCheck: "LearnCommitPointWithTermCheck"
+            kReplSetInitiate: "ReplSetInitiate"
+            kRollbackOplog: "RollbackOplog"
 
-    RaftMongoSpecAction:
-        description: "The supported actions in the RaftMongoSpec."
+    RaftMongoSpecServerState:
+        description: "The server states (leader or follower) modeled in RaftMongo.tla."
         type: string
         values:
-            kAppendOplog: "AppendOplog"
+            kLeader: "Leader"
+            kFollower: "Follower"
 
 structs:
-    TlaPlusTraceEvent:
-        description: "A document used for generating a TLA+ trace checker event."
+    RaftMongoSpecEvent:
+        description: "A subdocument containing values modeled by the RaftMongo.tla spec."
         fields:
-            spec:
-                type: TLAPlusSpec
-                description: "The TLA+ Spec that this event corresponds to."
-            action:
-                type: string
-                description: "The action that this event is logging."
-            host:
-                type: HostAndPort
-                description: "The HostAndPort logging the event."
-            state:
-                type: object
-                description: "State relevant to the current spec and action."
\ No newline at end of file
+            serverState:
+                type: RaftMongoSpecServerState
+                description: "This server's state."
+            commitPoint:
+                type: optime
+                description: "The current commit point according to this server."
+            term:
+                type: long
+                description: "The current term according to this server."
+            log:
+                type: array<optime>
+                description: "Optimes of all entries in the oplog."
diff --git a/src/mongo/db/storage/biggie/biggie_recovery_unit.cpp b/src/mongo/db/storage/biggie/biggie_recovery_unit.cpp
index 08e487fb603..f5ae5b9b6ac 100644
--- a/src/mongo/db/storage/biggie/biggie_recovery_unit.cpp
+++ b/src/mongo/db/storage/biggie/biggie_recovery_unit.cpp
@@ -44,17 +44,17 @@ RecoveryUnit::RecoveryUnit(KVEngine* parentKVEngine, std::function<void()> cb)
     : _waitUntilDurableCallback(cb), _KVEngine(parentKVEngine) {}
 
 RecoveryUnit::~RecoveryUnit() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     _abort();
 }
 
 void RecoveryUnit::beginUnitOfWork(OperationContext* opCtx) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     _setState(State::kInactiveInUnitOfWork);
 }
 
 void RecoveryUnit::doCommitUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
 
     if (_dirty) {
         invariant(_forked);
@@ -87,18 +87,18 @@ void RecoveryUnit::doCommitUnitOfWork() {
 }
 
 void RecoveryUnit::doAbortUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     _abort();
 }
 
 bool RecoveryUnit::waitUntilDurable(OperationContext* opCtx) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     invariant(!opCtx->lockState()->isLocked() || storageGlobalParams.repair);
     return true;  // This is an in-memory storage engine.
 }
 
 void RecoveryUnit::doAbandonSnapshot() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     _forked = false;
     _dirty = false;
 }
diff --git a/src/mongo/db/storage/ephemeral_for_test/ephemeral_for_test_recovery_unit.cpp b/src/mongo/db/storage/ephemeral_for_test/ephemeral_for_test_recovery_unit.cpp
index 8d1ac9735a7..4c74286c825 100644
--- a/src/mongo/db/storage/ephemeral_for_test/ephemeral_for_test_recovery_unit.cpp
+++ b/src/mongo/db/storage/ephemeral_for_test/ephemeral_for_test_recovery_unit.cpp
@@ -39,16 +39,16 @@
 namespace mongo {
 
 EphemeralForTestRecoveryUnit::~EphemeralForTestRecoveryUnit() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
 }
 
 void EphemeralForTestRecoveryUnit::beginUnitOfWork(OperationContext* opCtx) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     _setState(State::kInactiveInUnitOfWork);
 }
 
 void EphemeralForTestRecoveryUnit::doCommitUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     _setState(State::kCommitting);
 
     try {
@@ -71,7 +71,7 @@ void EphemeralForTestRecoveryUnit::doCommitUnitOfWork() {
 }
 
 void EphemeralForTestRecoveryUnit::doAbortUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     _setState(State::kAborting);
 
     try {
@@ -101,7 +101,7 @@ bool EphemeralForTestRecoveryUnit::inActiveTxn() const {
 }
 
 void EphemeralForTestRecoveryUnit::doAbandonSnapshot() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
 }
 
 Status EphemeralForTestRecoveryUnit::obtainMajorityCommittedSnapshot() {
diff --git a/src/mongo/db/storage/mobile/mobile_recovery_unit.cpp b/src/mongo/db/storage/mobile/mobile_recovery_unit.cpp
index 3cc2433870b..71baedeb757 100644
--- a/src/mongo/db/storage/mobile/mobile_recovery_unit.cpp
+++ b/src/mongo/db/storage/mobile/mobile_recovery_unit.cpp
@@ -58,7 +58,7 @@ MobileRecoveryUnit::MobileRecoveryUnit(MobileSessionPool* sessionPool)
 }
 
 MobileRecoveryUnit::~MobileRecoveryUnit() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     _abort();
     RECOVERY_UNIT_TRACE() << "Destroyed.";
 }
@@ -79,12 +79,12 @@ void MobileRecoveryUnit::_abort() {
     _setState(State::kAborting);
     abortRegisteredChanges();
 
-    invariant(!_isActive(), toString(_getState()));
+    invariant(!_isActive(), toString(getState()));
     _setState(State::kInactive);
 }
 
 void MobileRecoveryUnit::beginUnitOfWork(OperationContext* opCtx) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
 
     RECOVERY_UNIT_TRACE() << "Unit of work Active.";
 
@@ -100,7 +100,7 @@ void MobileRecoveryUnit::beginUnitOfWork(OperationContext* opCtx) {
 }
 
 void MobileRecoveryUnit::doCommitUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
 
     RECOVERY_UNIT_TRACE() << "Unit of work commited, marked inactive.";
 
@@ -108,7 +108,7 @@ void MobileRecoveryUnit::doCommitUnitOfWork() {
 }
 
 void MobileRecoveryUnit::doAbortUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
 
     RECOVERY_UNIT_TRACE() << "Unit of work aborted, marked inactive.";
 
@@ -150,7 +150,7 @@ bool MobileRecoveryUnit::waitUntilDurable(OperationContext* opCtx) {
 }
 
 void MobileRecoveryUnit::doAbandonSnapshot() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     if (_isActive()) {
         // We can't be in a WriteUnitOfWork, so it is safe to rollback.
         _txnClose(false);
@@ -186,7 +186,7 @@ void MobileRecoveryUnit::_ensureSession(OperationContext* opCtx) {
 }
 
 void MobileRecoveryUnit::_txnOpen(OperationContext* opCtx, bool readOnly) {
-    invariant(!_isActive(), toString(_getState()));
+    invariant(!_isActive(), toString(getState()));
     RECOVERY_UNIT_TRACE() << "_txnOpen called with readOnly:" << (readOnly ? "TRUE" : "FALSE");
     _ensureSession(opCtx);
 
@@ -222,7 +222,7 @@ void MobileRecoveryUnit::_txnOpen(OperationContext* opCtx, bool readOnly) {
 }
 
 void MobileRecoveryUnit::_txnClose(bool commit) {
-    invariant(_isActive(), toString(_getState()));
+    invariant(_isActive(), toString(getState()));
     RECOVERY_UNIT_TRACE() << "_txnClose called with " << (commit ? "commit " : "rollback ");
 
     if (commit) {
diff --git a/src/mongo/db/storage/recovery_unit.cpp b/src/mongo/db/storage/recovery_unit.cpp
index 3d167d7a9c3..0e0951c63e6 100644
--- a/src/mongo/db/storage/recovery_unit.cpp
+++ b/src/mongo/db/storage/recovery_unit.cpp
@@ -63,7 +63,7 @@ void RecoveryUnit::runPreCommitHooks(OperationContext* opCtx) {
 }
 
 void RecoveryUnit::registerChange(std::unique_ptr<Change> change) {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     _changes.push_back(std::move(change));
 }
 
diff --git a/src/mongo/db/storage/recovery_unit.h b/src/mongo/db/storage/recovery_unit.h
index 5158340a399..281000423e7 100644
--- a/src/mongo/db/storage/recovery_unit.h
+++ b/src/mongo/db/storage/recovery_unit.h
@@ -587,7 +587,10 @@ public:
         kAborting,
         kCommitting,
     };
-    State getState_forTest() const;
+
+    State getState() const {
+        return _state;
+    }
 
     std::string toString(State state) const {
         switch (state) {
@@ -615,13 +618,6 @@ protected:
     RecoveryUnit();
 
     /**
-     * Returns the current state.
-     */
-    State _getState() const {
-        return _state;
-    }
-
-    /**
      * Transitions to new state.
      */
     void _setState(State newState) {
diff --git a/src/mongo/db/storage/wiredtiger/SConscript b/src/mongo/db/storage/wiredtiger/SConscript
index 88451147071..d6bb12053de 100644
--- a/src/mongo/db/storage/wiredtiger/SConscript
+++ b/src/mongo/db/storage/wiredtiger/SConscript
@@ -91,6 +91,7 @@ if wiredtiger:
             '$BUILD_DIR/mongo/db/snapshot_window_options',
             '$BUILD_DIR/mongo/db/storage/storage_repair_observer',
             '$BUILD_DIR/mongo/util/options_parser/options_parser',
+            '$BUILD_DIR/mongo/util/tla_plus_trace',
             ],
         )
 
diff --git a/src/mongo/db/storage/wiredtiger/wiredtiger_oplog_manager.cpp b/src/mongo/db/storage/wiredtiger/wiredtiger_oplog_manager.cpp
index e57d25e58ee..8d4599d5e3a 100644
--- a/src/mongo/db/storage/wiredtiger/wiredtiger_oplog_manager.cpp
+++ b/src/mongo/db/storage/wiredtiger/wiredtiger_oplog_manager.cpp
@@ -34,6 +34,8 @@
 #include <cstring>
 
 #include "mongo/db/concurrency/lock_state.h"
+#include "mongo/db/repl/replication_coordinator.h"
+#include "mongo/db/repl/tla_plus_trace_repl_gen.h"
 #include "mongo/db/storage/wiredtiger/wiredtiger_kv_engine.h"
 #include "mongo/db/storage/wiredtiger/wiredtiger_oplog_manager.h"
 #include "mongo/db/storage/wiredtiger/wiredtiger_util.h"
@@ -41,6 +43,7 @@
 #include "mongo/util/concurrency/idle_thread_block.h"
 #include "mongo/util/log.h"
 #include "mongo/util/scopeguard.h"
+#include "mongo/util/tla_plus_trace.h"
 
 namespace mongo {
 namespace {
@@ -233,6 +236,22 @@ void WiredTigerOplogManager::_oplogJournalThreadLoop(WiredTigerSessionCache* ses
         // oplog read timestamp's documents are durable before publishing that timestamp.
         sessionCache->waitUntilDurable(opCtx.get(), /*forceCheckpoint=*/false, false);
 
+        // Log RaftMongo.tla ClientWrite actions when new oplog entries become visible, which is
+        // when they can first cause further actions. If we instead logged entries when they're
+        // written, they could have holes behind them, which would later be filled with entries with
+        // older optimes. Such behavior is not and need not be modeled in RaftMongo.tla.
+        // Skip when term = -1: replSetInitiate has written the first entry and it has the global
+        // lock, logging would deadlock.
+        if (MONGO_unlikely(logForTLAPlusSpecs.shouldFail())) {
+            auto replCoord = repl::ReplicationCoordinator::get(opCtx.get());
+            if (replCoord->getTerm() != -1) {
+                replCoord->tlaPlusRaftMongoEvent(
+                    opCtx.get(),
+                    repl::RaftMongoSpecActionEnum::kClientWrite,
+                    Timestamp(static_cast<unsigned long long>(newTimestamp)));
+            }
+        }
+
         lk.lock();
         // Publish the new timestamp value.  Avoid going backward.
         auto oldTimestamp = getOplogReadTimestamp();
diff --git a/src/mongo/db/storage/wiredtiger/wiredtiger_recovery_unit.cpp b/src/mongo/db/storage/wiredtiger/wiredtiger_recovery_unit.cpp
index 3b5e48f041e..3bd2c4ba214 100644
--- a/src/mongo/db/storage/wiredtiger/wiredtiger_recovery_unit.cpp
+++ b/src/mongo/db/storage/wiredtiger/wiredtiger_recovery_unit.cpp
@@ -162,7 +162,7 @@ WiredTigerRecoveryUnit::WiredTigerRecoveryUnit(WiredTigerSessionCache* sc,
     : _sessionCache(sc), _oplogManager(oplogManager) {}
 
 WiredTigerRecoveryUnit::~WiredTigerRecoveryUnit() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     _abort();
 }
 
@@ -206,16 +206,16 @@ void WiredTigerRecoveryUnit::_abort() {
 }
 
 void WiredTigerRecoveryUnit::beginUnitOfWork(OperationContext* opCtx) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     invariant(!_isCommittingOrAborting(),
               str::stream() << "cannot begin unit of work while commit or rollback handlers are "
                                "running: "
-                            << toString(_getState()));
+                            << toString(getState()));
     _setState(_isActive() ? State::kActive : State::kInactiveInUnitOfWork);
 }
 
 void WiredTigerRecoveryUnit::prepareUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     invariant(!_prepareTimestamp.isNull());
 
     auto session = getSession();
@@ -229,12 +229,12 @@ void WiredTigerRecoveryUnit::prepareUnitOfWork() {
 }
 
 void WiredTigerRecoveryUnit::doCommitUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     _commit();
 }
 
 void WiredTigerRecoveryUnit::doAbortUnitOfWork() {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     _abort();
 }
 
@@ -245,7 +245,7 @@ void WiredTigerRecoveryUnit::_ensureSession() {
 }
 
 bool WiredTigerRecoveryUnit::waitUntilDurable(OperationContext* opCtx) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     invariant(!opCtx->lockState()->isLocked() || storageGlobalParams.repair);
     const bool forceCheckpoint = false;
     const bool stableCheckpoint = false;
@@ -255,7 +255,7 @@ bool WiredTigerRecoveryUnit::waitUntilDurable(OperationContext* opCtx) {
 
 bool WiredTigerRecoveryUnit::waitUntilUnjournaledWritesDurable(OperationContext* opCtx,
                                                                bool stableCheckpoint) {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     invariant(!opCtx->lockState()->isLocked() || storageGlobalParams.repair);
     const bool forceCheckpoint = true;
     // Calling `waitUntilDurable` with `forceCheckpoint` set to false only performs a log
@@ -269,7 +269,7 @@ void WiredTigerRecoveryUnit::assertInActiveTxn() const {
     if (_isActive()) {
         return;
     }
-    severe() << "Recovery unit is not active. Current state: " << toString(_getState());
+    severe() << "Recovery unit is not active. Current state: " << toString(getState());
     fassertFailed(28575);
 }
 
@@ -301,7 +301,7 @@ WiredTigerSession* WiredTigerRecoveryUnit::getSessionNoTxn() {
 }
 
 void WiredTigerRecoveryUnit::doAbandonSnapshot() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     if (_isActive()) {
         // Can't be in a WriteUnitOfWork, so safe to rollback
         _txnClose(false);
@@ -315,7 +315,7 @@ void WiredTigerRecoveryUnit::preallocateSnapshot() {
 }
 
 void WiredTigerRecoveryUnit::_txnClose(bool commit) {
-    invariant(_isActive(), toString(_getState()));
+    invariant(_isActive(), toString(getState()));
     WT_SESSION* s = _session->getSession();
     if (_timer) {
         const int transactionTime = _timer->millis();
@@ -456,10 +456,10 @@ boost::optional<Timestamp> WiredTigerRecoveryUnit::getPointInTimeReadTimestamp()
 }
 
 void WiredTigerRecoveryUnit::_txnOpen() {
-    invariant(!_isActive(), toString(_getState()));
+    invariant(!_isActive(), toString(getState()));
     invariant(!_isCommittingOrAborting(),
               str::stream() << "commit or rollback handler reopened transaction: "
-                            << toString(_getState()));
+                            << toString(getState()));
     _ensureSession();
 
     // Only start a timer for transaction's lifetime if we're going to log it.
@@ -607,7 +607,7 @@ Status WiredTigerRecoveryUnit::setTimestamp(Timestamp timestamp) {
     _ensureSession();
     LOG(3) << "WT set timestamp of future write operations to " << timestamp;
     WT_SESSION* session = _session->getSession();
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     invariant(_prepareTimestamp.isNull());
     invariant(_commitTimestamp.isNull(),
               str::stream() << "Commit timestamp set to " << _commitTimestamp.toString()
@@ -635,7 +635,7 @@ void WiredTigerRecoveryUnit::setCommitTimestamp(Timestamp timestamp) {
     // setPrepareTimestamp() is called. Prepared transactions ensure the correct timestamping
     // semantics and the set-once commitTimestamp behavior is exactly what prepared transactions
     // want.
-    invariant(!_inUnitOfWork() || !_prepareTimestamp.isNull(), toString(_getState()));
+    invariant(!_inUnitOfWork() || !_prepareTimestamp.isNull(), toString(getState()));
     invariant(_commitTimestamp.isNull(),
               str::stream() << "Commit timestamp set to " << _commitTimestamp.toString()
                             << " and trying to set it to " << timestamp.toString());
@@ -665,7 +665,7 @@ Timestamp WiredTigerRecoveryUnit::getDurableTimestamp() const {
 }
 
 void WiredTigerRecoveryUnit::clearCommitTimestamp() {
-    invariant(!_inUnitOfWork(), toString(_getState()));
+    invariant(!_inUnitOfWork(), toString(getState()));
     invariant(!_commitTimestamp.isNull());
     invariant(!_lastTimestampSet,
               str::stream() << "Last timestamp set is " << _lastTimestampSet->toString()
@@ -676,7 +676,7 @@ void WiredTigerRecoveryUnit::clearCommitTimestamp() {
 }
 
 void WiredTigerRecoveryUnit::setPrepareTimestamp(Timestamp timestamp) {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     invariant(_prepareTimestamp.isNull(),
               str::stream() << "Trying to set prepare timestamp to " << timestamp.toString()
                             << ". It's already set to " << _prepareTimestamp.toString());
@@ -691,7 +691,7 @@ void WiredTigerRecoveryUnit::setPrepareTimestamp(Timestamp timestamp) {
 }
 
 Timestamp WiredTigerRecoveryUnit::getPrepareTimestamp() const {
-    invariant(_inUnitOfWork(), toString(_getState()));
+    invariant(_inUnitOfWork(), toString(getState()));
     invariant(!_prepareTimestamp.isNull());
     invariant(_commitTimestamp.isNull(),
               str::stream() << "Commit timestamp is " << _commitTimestamp.toString()
@@ -710,7 +710,7 @@ void WiredTigerRecoveryUnit::setPrepareConflictBehavior(PrepareConflictBehavior
     // ignoring prepare conflicts, since that behavior is applied when the transaction is opened.
     invariant(
         !_isActive(),
-        str::stream() << "Current state: " << toString(_getState())
+        str::stream() << "Current state: " << toString(getState())
                       << ". Invalid internal state while setting prepare conflict behavior to: "
                       << static_cast<int>(behavior));
 
@@ -725,7 +725,7 @@ void WiredTigerRecoveryUnit::setRoundUpPreparedTimestamps(bool value) {
     // This cannot be called after WiredTigerRecoveryUnit::_txnOpen.
     invariant(!_isActive(),
               str::stream() << "Can't change round up prepared timestamps flag "
-                            << "when current state is " << toString(_getState()));
+                            << "when current state is " << toString(getState()));
     _roundUpPreparedTimestamps =
         (value) ? RoundUpPreparedTimestamps::kRound : RoundUpPreparedTimestamps::kNoRound;
 }
@@ -736,7 +736,7 @@ void WiredTigerRecoveryUnit::setTimestampReadSource(ReadSource readSource,
            << ", provided timestamp: " << ((provided) ? provided->toString() : "none");
 
     invariant(!_isActive() || _timestampReadSource == readSource,
-              str::stream() << "Current state: " << toString(_getState())
+              str::stream() << "Current state: " << toString(getState())
                             << ". Invalid internal state while setting timestamp read source: "
                             << static_cast<int>(readSource) << ", provided timestamp: "
                             << (provided ? provided->toString() : "none"));
@@ -775,7 +775,7 @@ std::shared_ptr<StorageStats> WiredTigerRecoveryUnit::getOperationStatistics() c
 
 void WiredTigerRecoveryUnit::setCatalogConflictingTimestamp(Timestamp timestamp) {
     // This cannot be called after a storage snapshot is allocated.
-    invariant(!_isActive(), toString(_getState()));
+    invariant(!_isActive(), toString(getState()));
     invariant(_timestampReadSource == ReadSource::kNoTimestamp,
               str::stream() << "Illegal to set catalog conflicting timestamp for a read source "
                             << static_cast<int>(_timestampReadSource));
diff --git a/src/mongo/embedded/replication_coordinator_embedded.cpp b/src/mongo/embedded/replication_coordinator_embedded.cpp
index 7d0a9551a8f..b9736047396 100644
--- a/src/mongo/embedded/replication_coordinator_embedded.cpp
+++ b/src/mongo/embedded/replication_coordinator_embedded.cpp
@@ -441,7 +441,7 @@ Status ReplicationCoordinatorEmbedded::processHeartbeatV1(const ReplSetHeartbeat
     UASSERT_NOT_IMPLEMENTED;
 }
 
-long long ReplicationCoordinatorEmbedded::getTerm() {
+long long ReplicationCoordinatorEmbedded::getTerm() const {
     UASSERT_NOT_IMPLEMENTED;
 }
 
diff --git a/src/mongo/embedded/replication_coordinator_embedded.h b/src/mongo/embedded/replication_coordinator_embedded.h
index bea48b742b3..531b0b9c462 100644
--- a/src/mongo/embedded/replication_coordinator_embedded.h
+++ b/src/mongo/embedded/replication_coordinator_embedded.h
@@ -227,7 +227,7 @@ public:
 
     void dropAllSnapshots() override;
 
-    long long getTerm() override;
+    long long getTerm() const override;
 
     Status updateTerm(OperationContext*, long long) override;
 
diff --git a/src/mongo/util/SConscript b/src/mongo/util/SConscript
index 62e33a6232d..2b9952d1eeb 100644
--- a/src/mongo/util/SConscript
+++ b/src/mongo/util/SConscript
@@ -657,3 +657,18 @@ if use_libunwind:
             '$BUILD_DIR/third_party/shim_unwind',
         ],
     )
+
+env.Library(
+    target='tla_plus_trace',
+    source=[
+        'tla_plus_trace.cpp',
+        env.Idlc('tla_plus_trace.idl')[0],
+    ],
+    LIBDEPS=[
+        '$BUILD_DIR/mongo/base',
+        '$BUILD_DIR/mongo/db/server_options',
+        '$BUILD_DIR/mongo/idl/idl_parser',
+        'fail_point',
+        'net/network',
+    ],
+)
diff --git a/src/mongo/db/repl/tla_plus_trace_repl.cpp b/src/mongo/util/tla_plus_trace.cpp
index 2c97131038d..d634a171a8f 100644
--- a/src/mongo/db/repl/tla_plus_trace_repl.cpp
+++ b/src/mongo/util/tla_plus_trace.cpp
@@ -31,34 +31,25 @@
 
 #include "mongo/platform/basic.h"
 
-#include "mongo/db/repl/tla_plus_trace_repl.h"
+#include "mongo/util/tla_plus_trace.h"
 
-#include "mongo/db/repl/replication_coordinator.h"
 #include "mongo/util/log.h"
-#include "mongo/util/net/socket_utils.h"
 #include "mongo/util/time_support.h"
 
-
 namespace mongo {
-namespace repl {
-
-namespace {
 
-constexpr StringData kSpecFieldName = "specs"_sd;
+MONGO_FAIL_POINT_DEFINE(logForTLAPlusSpecs);
 
-auto enabledForSpec(TLAPlusSpecEnum spec) {
+std::function<bool(const BSONObj& data)> enabledForSpec(TLAPlusSpecEnum spec) {
     return [spec](const BSONObj& data) {
-        auto array = data[kSpecFieldName].Array();
+        auto array = data["specs"_sd].Array();
         return std::find_if(array.begin(), array.end(), [&spec](BSONElement elem) {
                    return elem.String() == TLAPlusSpec_serializer(spec);
                }) != array.end();
     };
 }
 
-/**
- *  Logs the provided message at a timestamp greater than the current time.
- */
-void logEvent(std::string message) {
+void logTlaPlusTraceEvent(const TlaPlusTraceEvent& event) {
     Date_t beforeTime = Date_t::now();
     Date_t afterTime = Date_t::now();
     while (afterTime == beforeTime) {
@@ -67,43 +58,6 @@ void logEvent(std::string message) {
     }
 
     invariant(afterTime > beforeTime, "Clock went backwards");
-    log() << message;
-}
-
-void logTlaPlusRaftMongoEvent(OperationContext* opCtx, RaftMongoSpecActionEnum action) {
-    TlaPlusTraceEvent event;
-    event.setSpec(TLAPlusSpecEnum::kRaftMongo);
-    event.setAction(RaftMongoSpecAction_serializer(action));
-    event.setHost(HostAndPort(getHostName(), serverGlobalParams.port));
-
-    auto service = cc().getServiceContext();
-    if (!service->getStorageEngine()) {
-        LOG(2) << "Aborting logTlaPlusRaftMongoEvent: storage layer not yet initialized";
-        return;
-    }
-
-    auto replCoord = ReplicationCoordinator::get(service);
-
-    BSONObjBuilder bob;
-    // Ignore other states not covered in the spec.
-    bob.append("serverState",
-               replCoord->getMemberState() == MemberState::RS_PRIMARY ? "Leader" : "Follower");
-    bob.append("commitPoint", replCoord->getLastCommittedOpTime().toBSON());
-    bob.append("term", replCoord->getTerm());
-    event.setState(bob.obj());
-
-    logEvent(event.toBSON().toString());
-}
-
-}  // namespace
-
-MONGO_FAIL_POINT_DEFINE(logForTLAPlusSpecs)
-
-void tlaPlusRaftMongoEvent(OperationContext* opCtx, RaftMongoSpecActionEnum action) {
-    if (MONGO_unlikely(
-            logForTLAPlusSpecs.scopedIf(enabledForSpec(TLAPlusSpecEnum::kRaftMongo)).isActive())) {
-        logTlaPlusRaftMongoEvent(opCtx, action);
-    }
+    log() << event.toBSON().jsonString();
 }
-}  // namespace repl
 }  // namespace mongo
diff --git a/src/mongo/db/repl/tla_plus_trace_repl.h b/src/mongo/util/tla_plus_trace.h
index 74659102a53..081ba610b5e 100644
--- a/src/mongo/db/repl/tla_plus_trace_repl.h
+++ b/src/mongo/util/tla_plus_trace.h
@@ -29,21 +29,28 @@
 
 #pragma once
 
-#include "mongo/db/repl/tla_plus_trace_repl_gen.h"
 #include "mongo/util/fail_point.h"
+#include "mongo/util/tla_plus_trace_gen.h"
 
 namespace mongo {
-namespace repl {
 
-/*
- * Log execution traces so we can compare MongoDB's implementation to our TLA+ specs.
- */
 extern FailPoint logForTLAPlusSpecs;
 
 /**
- * Trace an event for the RaftMongo spec.
+ * Use like:
+ * if (MONGO_unlikely(logForTLAPlusSpecs.scopedIf(
+ *         enabledForSpec(TLAPlusSpecEnum::kRaftMongo)).isActive()))
+ * {
+ *     ... log event for spec "Foo.tla" ...
+ * }
+ *
+ * The return value is a lambda like "bool lambda(const BSONObj& data)".
+ */
+std::function<bool(const BSONObj& data)> enabledForSpec(TLAPlusSpecEnum spec);
+
+/**
+ * Trace an event for a TLA+ spec.
  */
-void tlaPlusRaftMongoEvent(OperationContext* opCtx, RaftMongoSpecActionEnum action);
+void logTlaPlusTraceEvent(const TlaPlusTraceEvent& event);
 
-}  // namespace repl
 }  // namespace mongo
diff --git a/src/mongo/util/tla_plus_trace.idl b/src/mongo/util/tla_plus_trace.idl
new file mode 100644
index 00000000000..a0c3684798c
--- /dev/null
+++ b/src/mongo/util/tla_plus_trace.idl
@@ -0,0 +1,64 @@
+# Copyright (C) 2019-present MongoDB, Inc.
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the Server Side Public License, version 1,
+# as published by MongoDB, Inc.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# Server Side Public License for more details.
+#
+# You should have received a copy of the Server Side Public License
+# along with this program. If not, see
+# <http://www.mongodb.com/licensing/server-side-public-license>.
+#
+# As a special exception, the copyright holders give permission to link the
+# code of portions of this program with the OpenSSL library under certain
+# conditions as described in each individual source file and distribute
+# linked combinations including the program with the OpenSSL library. You
+# must comply with the Server Side Public License in all respects for
+# all of the code used other than as permitted herein. If you modify file(s)
+# with this exception, you may extend this exception to your version of the
+# file(s), but you are not obligated to do so. If you do not wish to do so,
+# delete this exception statement from your version. If you delete this
+# exception statement from all source files in the program, then also delete
+# it in the license file.
+#
+
+# TLA+ Trace Checker Event IDL File
+
+global:
+    cpp_namespace: "mongo"
+    cpp_includes:
+        - "mongo/db/server_options.h"
+        - "mongo/util/net/socket_utils.h"
+
+imports:
+    - "mongo/idl/basic_types.idl"
+    - "mongo/util/net/hostandport.idl"
+
+enums:
+    TLAPlusSpec:
+        description: "The supported TLA+ specs."
+        type: string
+        values:
+            kRaftMongo: "RaftMongo"
+
+structs:
+    TlaPlusTraceEvent:
+        description: "A document used for generating a TLA+ trace checker event."
+        fields:
+            spec:
+                type: TLAPlusSpec
+                description: "The TLA+ Spec that this event corresponds to."
+            action:
+                type: string
+                description: "The action that this event is logging."
+            host:
+                type: HostAndPort
+                description: "The HostAndPort logging the event."
+                default: HostAndPort(getHostName(), serverGlobalParams.port)
+            state:
+                type: object
+                description: "State relevant to the current spec and action."