Select some/all replication fuzz tests for checking. At the beginning of these fuzz tests, disable oplog truncation and enable the logging component that is introduced for the sake of trace checking. At the end of these tests, run the scripts that extract an execution trace and compare it to our selected TLA+ specs. Output a useful report and fail the test if the actual trace is not permitted by one of the specs.