diff --git a/README.md b/README.md
index 1ced8949..069f7fd1 100644
--- a/README.md
+++ b/README.md
@@ -13,17 +13,17 @@ A central manifest of specs with descriptions and accounts of their various mode
## List of Examples
-| # | Name | Description | Authors | TLAPS Proof? | TLC Model? | Module Dependencies | PlusCal? | Apalache? |
-|:-:|------|-------------|---------|:------------:|:----------:|---------------------|:--------:|:---------:|
-| 1 | 2PCwithBTM | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | |
-| 2 | 802.16 | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | Int, Seq, FinSet | | |
-| 3 | aba-asyn-byz | Asynchronous Byzantine agreement (Bracha & Toueg, 1985) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | |
-| 4 | acp-nb | Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | |
-| 5 | acp-nb-wrong | Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | |
-| 6 | acp-sb | Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | |
-| 7 | allocator | Specification of a resource allocator | Stephan Merz | | ✔ | FinSet | | |
-| 8 | async-comm | The diversity of asynchronous communication (Chevrou et al., 2016) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | ✔ | Nat | | |
-| 9 | bcastByz | Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat, FinSet | | |
+| # | Name | Description | Authors | TLAPS Proof? | TLC Model? | Module Dependencies | PlusCal? | Apalache? |
+|:---:|-----------------------------------|-------------|---------|:------------:|:----------:|---------------------|:--------:|:---------:|
+| 1 | 2PCwithBTM | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | |
+| 2 | 802.16 | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | Int, Seq, FinSet | | |
+| 3 | aba-asyn-byz | Asynchronous Byzantine agreement (Bracha & Toueg, 1985) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | |
+| 4 | acp-nb | Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | |
+| 5 | acp-nb-wrong | Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | |
+| 6 | acp-sb | Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | |
+| 7 | allocator | Specification of a resource allocator | Stephan Merz | | ✔ | FinSet | | |
+| 8 | async-comm | The diversity of asynchronous communication (Chevrou et al., 2016) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | ✔ | Nat | | |
+| 9 | bcastByz | Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat, FinSet | | |
| 10 | bcastFolklore | Folklore reliable broadcast - Figure 4 (Chandra and Toueg, 1996) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat | | |
| 11 | bosco | One-Step Byzantine asynchronous consensus (Song & Renesse, 2008) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat, FinSet | | |
| 12 | Boulangerie | A variant of the bakery algorithm (Yoram & Patkin, 2015) | Leslie Lamport, Stephan Merz | ✔ | ✔ | Int | ✔ | |
@@ -101,24 +101,25 @@ A central manifest of specs with descriptions and accounts of their various mode
| 84 | EWD687a | Detecting termination in distributed computations by Edsger Dijkstra and Carel Scholten | Stephan Merz (PlusCal spec), Leslie Lamport & Markus Kuppe (TLA+ spec) | | ✔ | Integers, Graphs | ✔ | |
| 85 | Huang | Termination detection by using distributed snapshots by Shing-Tsaan Huang | Markus Kuppe | | ✔ | DyadicRationals | | |
| 86 | Azure Cosmos DB | Consistency models provided by Azure Cosmos DB | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe | | ✔ | Integers, Sequences, FiniteSets, Functions, SequencesExt | ✔ | |
-| 87 | MET for CRDT-Redis | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | Integers, Sequences, FiniteSets, TLC | ✔ | |
-| 88 | Parallel increment | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | Integers, FiniteSets, TLC | | |
-| 89 | The Streamlet consensus algorithm | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | Sequences, Integers, FiniteSets | ✔ | |
-| 90 | Petri Nets | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | Integers, Sequences, FiniteSets, TLC | | |
-| 91 | Knuth Yao & Markov Chains | Knuth-Yao algorithm for simulating a sixsided die | Ron Pressler, Markus Kuppe | | ✔ | DyadicRationals | | |
-| 92 | ewd426 - Token Stabilization | Self-stabilizing systems in spite of distributed control | Murat Demirbas, Markus Kuppe | | ✔ | Naturals, FiniteSets | | |
-| 93 | CRDT | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔| Naturals, FiniteSets | |
-| 94 | Multi-Car Elevator System | Directory | Andrew Helwer | | ✔ | Integers | | |
-| 95 | Snapshot Key-Value Store | Directory | Andrew Helwer | | ✔ | | | |
-| 96 | Nano Blockchain Protocol | Directory | Andrew Helwer | | ✔ | Naturals, Bags | | |
-| 97 | Coffee Can White/Black Bean Problem | Directory | Andrew Helwer | | ✔ | Naturals | | |
-| 98 | The Slush Protocol | Directory | Andrew Helwer | | ✔ | Naturals, FiniteSets, Sequences | ✔ | |
-| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | |
-| 100 | Simplified Fast Paxos | Simplified version of Fast Paxos (Lamport, 2006) | Lim Ngian Xin Terry, Gaurav Gandhi | |✔| TLC, Naturals, FiniteSets, Integers | | |
-| 101 | Learn TLA⁺ Proofs | Basic PlusCal algorithms and formal proofs of their correctness | Andrew Helwer | ✔ | ✔ | Sequences, Naturals, Integers, TLAPS | ✔ | |
-| 102 | Lexicographically-Least Circular Substring | Booth's 1980 algorithm to find the lexicographically-least circular substring | Andrew Helwer | | ✔ | FiniteSets, Integers, Naturals, Sequences | ✔ | |
-| 103 | Distributed Checkpoint Coordination | Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring | Andrew Helwer | | ✔ | FiniteSets, Naturals, Sequences, TLC | | |
-| 104 | Boyer-Moore Majority Vote | Efficient algorithm for finding a majority value | Stephan Merz | ✔ | ✔ | Integers, Sequences, FiniteSets, TLAPS | | |
+| 87 | MET for CRDT-Redis | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | Integers, Sequences, FiniteSets, TLC | ✔ | |
+| 88 | Parallel increment | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | Integers, FiniteSets, TLC | | |
+| 89 | The Streamlet consensus algorithm | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | Sequences, Integers, FiniteSets | ✔ | |
+| 90 | Petri Nets | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | Integers, Sequences, FiniteSets, TLC | | |
+| 91 | Knuth Yao & Markov Chains | Knuth-Yao algorithm for simulating a sixsided die | Ron Pressler, Markus Kuppe | | ✔ | DyadicRationals | | |
+| 92 | ewd426 - Token Stabilization | Self-stabilizing systems in spite of distributed control | Murat Demirbas, Markus Kuppe | | ✔ | Naturals, FiniteSets | | |
+| 93 | CRDT | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔| Naturals, FiniteSets | |
+| 94 | Multi-Car Elevator System | Directory | Andrew Helwer | | ✔ | Integers | | |
+| 95 | Snapshot Key-Value Store | Directory | Andrew Helwer | | ✔ | | | |
+| 96 | Nano Blockchain Protocol | Directory | Andrew Helwer | | ✔ | Naturals, Bags | | |
+| 97 | The Coffee Can Bean Problem | Directory | Andrew Helwer | | ✔ | Naturals | | |
+| 98 | The Slush Protocol | Directory | Andrew Helwer | | ✔ | Naturals, FiniteSets, Sequences | ✔ | |
+| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | |
+| 100 | Simplified Fast Paxos | Simplified version of Fast Paxos (Lamport, 2006) | Lim Ngian Xin Terry, Gaurav Gandhi | |✔| TLC, Naturals, FiniteSets, Integers | | |
+| 101 | Learn TLA⁺ Proofs | Basic PlusCal algorithms and formal proofs of their correctness | Andrew Helwer | ✔ | ✔ | Sequences, Naturals, Integers, TLAPS | ✔ | |
+| 102 | Minimal Circular Substring | Booth's 1980 algorithm to find the lexicographically-least circular substring | Andrew Helwer | | ✔ | FiniteSets, Integers, Naturals, Sequences | ✔ | |
+| 103 | Checkpoint Coordination | Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring | Andrew Helwer | | ✔ | FiniteSets, Naturals, Sequences, TLC | | |
+| 104 | Boyer-Moore Majority Vote | Efficient algorithm for finding a majority value | Stephan Merz | ✔ | ✔ | Integers, Sequences, FiniteSets, TLAPS | | |
+| 105 | Finitizing Monotonic Systems | A technique for making infinite-state monotonic systems finite | Andrew Helwer | | ✔ | Naturals, Sequences | | |
## License
diff --git a/manifest-schema.json b/manifest-schema.json
index f0906991..d483f8df 100644
--- a/manifest-schema.json
+++ b/manifest-schema.json
@@ -20,7 +20,7 @@
},
"tags": {
"type": "array",
- "items": {"enum": ["beginner"]}
+ "items": {"enum": ["beginner", "intermediate"]}
},
"modules": {
"type": "array",
diff --git a/manifest.json b/manifest.json
index fade6579..d06e5b6d 100644
--- a/manifest.json
+++ b/manifest.json
@@ -389,6 +389,92 @@
}
]
},
+ {
+ "path": "specifications/FiniteMonotonic",
+ "title": "Finite Model-Checking of Monotonic Systems",
+ "description": "Illustration of technique for making ordinarily-infinite monotonic systems finite for the purposes of model-checking.",
+ "source": "https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/",
+ "authors": [
+ "Andrew Helwer"
+ ],
+ "tags": [
+ "intermediate"
+ ],
+ "modules": [
+ {
+ "path": "specifications/FiniteMonotonic/CRDT.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": []
+ },
+ {
+ "path": "specifications/FiniteMonotonic/Finitize_CRDT.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": [
+ {
+ "path": "specifications/FiniteMonotonic/Finitize_CRDT.cfg",
+ "runtime": "00:00:05",
+ "size": "small",
+ "mode": "exhaustive search",
+ "config": [],
+ "features": [
+ "liveness"
+ ],
+ "result": "success"
+ }
+ ]
+ },
+ {
+ "path": "specifications/FiniteMonotonic/Constrain_CRDT.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": [
+ {
+ "path": "specifications/FiniteMonotonic/Constrain_CRDT.cfg",
+ "runtime": "00:00:05",
+ "size": "small",
+ "mode": "exhaustive search",
+ "config": [],
+ "features": [
+ "liveness",
+ "state constraint"
+ ],
+ "result": "success"
+ }
+ ]
+ },
+ {
+ "path": "specifications/FiniteMonotonic/Finitize_ReplicatedLog.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": [
+ {
+ "path": "specifications/FiniteMonotonic/Finitize_ReplicatedLog.cfg",
+ "runtime": "00:00:05",
+ "size": "small",
+ "mode": "exhaustive search",
+ "config": [],
+ "features": [
+ "liveness"
+ ],
+ "result": "success"
+ }
+ ]
+ },
+ {
+ "path": "specifications/FiniteMonotonic/ReplicatedLog.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": []
+ }
+ ]
+ },
{
"path": "specifications/GameOfLife",
"title": "Conway's Game of Life",
@@ -458,6 +544,22 @@
],
"tags": [],
"modules": [
+ {
+ "path": "specifications/KeyValueStore/ClientCentric.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": []
+ },
+ {
+ "path": "specifications/KeyValueStore/KVsnap.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [
+ "pluscal"
+ ],
+ "models": []
+ },
{
"path": "specifications/KeyValueStore/KeyValueStore.tla",
"communityDependencies": [],
@@ -504,13 +606,6 @@
}
]
},
- {
- "path": "specifications/KeyValueStore/KVsnap.tla",
- "communityDependencies": [],
- "tlaLanguageVersion": 2,
- "features": ["pluscal"],
- "models": []
- },
{
"path": "specifications/KeyValueStore/MCKVsnap.tla",
"communityDependencies": [],
@@ -539,13 +634,6 @@
"tlaLanguageVersion": 2,
"features": [],
"models": []
- },
- {
- "path": "specifications/KeyValueStore/ClientCentric.tla",
- "communityDependencies": [],
- "tlaLanguageVersion": 2,
- "features": [],
- "models": []
}
]
},
@@ -770,6 +858,55 @@
}
]
},
+ {
+ "path": "specifications/Majority",
+ "title": "Boyer-Moore majority vote algorithm",
+ "description": "An efficient algorithm for detecting a majority value in a sequence",
+ "source": "",
+ "authors": [
+ "Stephan Merz"
+ ],
+ "tags": [
+ "beginner"
+ ],
+ "modules": [
+ {
+ "path": "specifications/Majority/MCMajority.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": [
+ {
+ "path": "specifications/Majority/MCMajority.cfg",
+ "runtime": "00:00:05",
+ "size": "small",
+ "mode": "exhaustive search",
+ "config": [
+ "ignore deadlock"
+ ],
+ "features": [],
+ "result": "success"
+ }
+ ]
+ },
+ {
+ "path": "specifications/Majority/Majority.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [],
+ "models": []
+ },
+ {
+ "path": "specifications/Majority/MajorityProof.tla",
+ "communityDependencies": [],
+ "tlaLanguageVersion": 2,
+ "features": [
+ "proof"
+ ],
+ "models": []
+ }
+ ]
+ },
{
"path": "specifications/MisraReachability",
"title": "Misra Reachability Algorithm",
@@ -3252,7 +3389,7 @@
"config": [
"ignore deadlock"
],
- "features": [
+ "features": [
"liveness",
"state constraint",
"view"
@@ -3698,51 +3835,6 @@
"models": []
}
]
- },
- {
- "path": "specifications/Majority",
- "title": "Boyer-Moore majority vote algorithm",
- "description": "An efficient algorithm for detecting a majority value in a sequence",
- "source": "",
- "authors": [
- "Stephan Merz"
- ],
- "tags": ["beginner"],
- "modules": [
- {
- "path": "specifications/Majority/Majority.tla",
- "communityDependencies": [],
- "tlaLanguageVersion": 2,
- "features": [],
- "models": []
- },
- {
- "path": "specifications/Majority/MCMajority.tla",
- "communityDependencies": [],
- "tlaLanguageVersion": 2,
- "features": [],
- "models": [
- {
- "path": "specifications/Majority/MCMajority.cfg",
- "runtime": "00:00:05",
- "size": "small",
- "mode": "exhaustive search",
- "config": ["ignore deadlock"],
- "features": [],
- "result": "success"
- }
- ]
- },
- {
- "path": "specifications/Majority/MajorityProof.tla",
- "communityDependencies": [],
- "tlaLanguageVersion": 2,
- "features": [
- "proof"
- ],
- "models": []
- }
- ]
}
]
}
diff --git a/specifications/FiniteMonotonic/BlogPost.md b/specifications/FiniteMonotonic/BlogPost.md
new file mode 100644
index 00000000..090f657a
--- /dev/null
+++ b/specifications/FiniteMonotonic/BlogPost.md
@@ -0,0 +1,419 @@
+# Wrangling monotonic systems in TLA⁺: Tractable modeling of replicated logs & CRDTs
+*This blog post is licensed under [CC-BY-SA 4.0](https://creativecommons.org/licenses/by-sa/4.0/).
+Originally published by Andrew Helwer at https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/ on 2023-11-01.*
+
+TLA⁺ sees a lot of use modeling distributed systems.
+The ability to explore all possible interleavings of events makes concurrency simple to reason about.
+For this TLA⁺ uses something called finite model-checking, which is really just a breadth-first search through the entire state space.
+The key here - and this really must be emphasized - is that the model is *finite*.
+There can't be an infinite number of states, or of course the model checker will run forever.
+
+Unfortunately, a lot of distributed systems are designed with infinitely-expanding state at their core.
+You want your system to be *monotonic*, which means it never revisits an earlier state.
+This is because ordering things in a distributed system is very difficult.
+If your system always progresses through states, never returning to earlier ones, it gives you a simple way to order your system and say it was in one state before it was in another state.
+A whole class of problems evaporate.
+
+Here is an example: a number that only increases in value, which we'll call a monotonic counter.
+Monotonic counters are used everywhere in distributed systems.
+In fact, I struggle to think of a distributed system that *doesn't* have a monotonic counter somewhere in its design.
+Here's a short list of ways I've seen monotonic counters used:
+ * transaction IDs
+ * live configuration versioning
+ * indices in an append-only log
+ * proposal ballot numbers in consensus algorithms
+
+So here's the problem: we want to subject distributed systems to finite modeling, but they try to cram as much infinity as possible into their system designs.
+How do we square this circle?
+
+## The hammer: state restrictions
+
+Here's a method long used by many TLA⁺ practitioners, including myself.
+Just pick an arbitrary point and say "okay, we've explored enough of the state space, don't go beyond here".
+So your monotonic counters are limited to, say, 10 or below.
+If you haven't found a bug by the time your counter hits 10 it probably doesn't exist, so the thinking goes.
+This is actually pretty good thinking!
+Indeed, when designing a model you're often making tradeoffs between state exploration and your model finishing before the heat death of the universe.
+It's rare, for example, for a TLA⁺ model to use more than three nodes in a distributed system despite production systems often involving many, many more nodes than that.
+TLA⁺ is still extraordinarily effective at finding bugs in these models, which is a testament to the complexity of concurrent & distributed systems generally.
+Us programmers can barely think straight about one computer, let alone three or more!
+
+Unfortunately, if you add state restrictions you've cut yourself off from many powerful TLA⁺ features (see page 247, section 14.3.5 of [*Specifying Systems*](https://lamport.azurewebsites.net/tla/book.html) for details).
+In particular, you'll lose the ability to analyze liveness (good things eventually happen) or abstraction & refinement (showing that one spec is related to another).
+Sometimes this is a decent tradeoff, because safety checking (bad things don't happen) can still be used and is often all the system needs.
+Still, is there a technique to get the best of both worlds?
+
+## Lamport's abstraction
+
+In his 2005 paper *Real Time is Really Simple* ([pdf](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-30.pdf)), Leslie Lamport faced a similar problem modeling real-time systems in TLA⁺.
+Real-time systems have all sorts of restrictions like "this process must complete before this time" and "this process can only start after this time".
+It's interesting to think about how to model this.
+A simple approach could have a single variable called `clock` or `now` which monotonically increases as time passes (say, measuring seconds elapsed), and there are timers associated with specific future values of that variable.
+These timers function as either deadlines or triggers for events.
+
+Lamport's core insight was that the specific value of this clock variable *cannot matter*.
+How could it?
+What would it start at?
+Would it start at 0 as the system comes online?
+Would it be initialized to [Unix time](https://en.wikipedia.org/wiki/Unix_time)?
+Why not the Gregorian calendar, or even the Mayan calendar?
+The system would obviously function identically in all of these schemes.
+All that matters, he concluded, is how far away all our timers are from the present moment.
+So when time passes, we don't update the clock: we update the timers!
+
+This translates very well to a finite model.
+Instead of having an infinite monotonically-increasing clock, we just have a collection of timer variables whose values are restricted to some small quantity.
+These timers might be initialized to some value, but they only ever spiral down toward zero.
+The infinite rendered finite.
+We will apply this insight to all of our monotonic systems.
+
+## Constraining divergence
+
+It's time to put our thinking caps on and consider carefully what we actually want to model with these monotonic counters.
+I argue we *really* just want to capture divergence.
+All the interesting behavior in distributed systems occurs when the different nodes have a different view of what's true, usually caused by some of them lagging behind others in receiving & processing updates.
+Suppose you have a three node system, where each node has its view of the current value of some monotonic counter.
+Is there really any difference between those nodes believing the value is `1`, `2`, and `3` respectively, as opposed to `101`, `102`, and `103`?
+I argue there is not.
+We can think of these counters as analogous to the clock from up above: all we care about is the difference between the highest value believed to be true and the lowest value.
+We call this difference the divergence.
+Thus, normalize: when all the counters on all the nodes reach some nonzero value, transpose them so the lowest value is zero.
+We will call this operation garbage collection.
+
+We want to constrain divergence to a finite value.
+Here we see a classic tradeoff between expressivity and tractability: the larger the divergence limit, the larger our state space and thus the greater our possibility of generating interesting behavior that triggers bugs, but also the longer our model will run.
+What happens when a node tries to increment its counter beyond our divergence limit?
+Simple, we don't let it.
+Other nodes will need to catch up a bit and then all the counters will have to be garbage-collected to open up some space for additional incrementing.
+
+One might object that this is all a bit artificial: real systems don't have this monotonic counter garbage collection process, and they certainly don't keep nodes from progressing just because some other node is frozen.
+I contend this is necessary and part of the art of abstracting a system to model what is really interesting about it.
+We don't care about the actual values of these counters.
+We only care about their divergence, and this is how you model divergence without resorting to the state restriction hammer.
+As we'll see, we can also neatly separate these artificial aspects from the spec itself, so as not to distract readers with irrelevant detail.
+
+## Modeling a conflict-free replicated data type
+
+Let's take the quintessential monotonic eventually-consistent distributed system, a grow-only counter [CRDT](https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type).
+With a grow-only counter, you have a network of nodes keeping track of some increasing quantity - say, the number of requests they service.
+Each node holds a vector of counters, and a node is associated with a specific index in that vector.
+When a node services a request, it increments only its index in its vector.
+Occasionally, the nodes will gossip their entire vector to each other, and the recipient merges the vector with their own by taking the max of each element.
+Thus the total number of requests serviced by the system is found by summing all the elements of the vector on any given node, although the result might differ & lag slightly between nodes.
+Here's how we write this in TLA⁺:
+```tla
+------------------------------- MODULE CRDT ---------------------------------
+EXTENDS Naturals
+
+CONSTANT Node
+
+VARIABLE counter
+
+TypeOK ≜ counter ∈ [Node → [Node → ℕ]]
+
+Init ≜ counter = [n ∈ Node ↦ [o ∈ Node ↦ 0]]
+
+Increment(n) ≜ counter' = [counter EXCEPT ![n][n] = @ + 1]
+
+Gossip(n, o) ≜
+ LET Max(a, b) ≜ IF a > b THEN a ELSE b IN
+ counter' = [
+ counter EXCEPT ![o] = [
+ nodeView ∈ Node ↦
+ Max(counter[n][nodeView], counter[o][nodeView])
+ ]
+ ]
+
+Next ≜
+ ∨ ∃ n ∈ Node : Increment(n)
+ ∨ ∃ n, o ∈ Node : Gossip(n, o)
+
+Spec ≜
+ ∧ Init
+ ∧ □[Next]_counter
+
+=============================================================================
+```
+**Note**: *All TLA⁺ snippets in this post use the unicode format.
+Convert them to their ASCII equivalents (and vice-versa) using [tlauc](https://github.com/tlaplus-community/tlauc).*
+
+What things do we want to verify about this system?
+Here's a safety check we could add, just to make sure we modeled the system correctly: a node will always have the highest value of its own counter among all other nodes:
+```tla
+Safety ≜ ∀ n, o ∈ Node : counter[n][n] ≥ counter[o][n]
+```
+We also will want to validate that the system is monotonic.
+In TLA⁺ we do this by saying every single step ensures all the values in the `counter` variable are greater than or equal to their previous values:
+```tla
+Monotonic ≜ ∀ n, o ∈ Node : counter'[n][o] ≥ counter[n][o]
+Monotonicity ≜ □[Monotonic]_counter
+```
+Finally, the big one: this is an eventually-consistent system, so we want to validate its eventual consistency as a liveness property!
+We want to say it is always the case that eventually the vectors on all nodes will have the same value.
+Let's define this goal state as:
+```tla
+Convergence ≜ ∀ n, o ∈ Node : counter[n] = counter[o]
+```
+While we want to say this property will always eventually be true in our system, that isn't actually correct!
+Think of a system servicing huge numbers of requests, far more often than it gossips vectors to the other nodes.
+Such a system will always have its vectors slightly out of date, and so convergence never happens.
+Really our convergence property will only become true if all requests stop for a while.
+
+We model this by adding a boolean variable, `converge`, which is arbitrarily set to `TRUE` at some point and stops additional increments from occurring.
+Since this is a virtual variable that wouldn't exist in any real system, we should move it out into a model-checking spec that imports our "good copy" spec and wraps its definitions with `converge` logic:
+```tla
+------------------------------ MODULE MC_CRDT -------------------------------
+CONSTANT Node
+
+VARIABLES counter, converge
+
+vars ≜ ⟨counter, converge⟩
+
+S ≜ INSTANCE CRDT
+
+TypeOK ≜
+ ∧ S!TypeOK
+ ∧ converge ∈ BOOLEAN
+
+Safety ≜ S!Safety
+
+Monotonicity ≜ S!Monotonicity
+
+Liveness ≜ converge ↝ S!Convergence
+
+Init ≜
+ ∧ S!Init
+ ∧ converge = FALSE
+
+Increment(n) ≜
+ ∧ ¬converge
+ ∧ S!Increment(n)
+ ∧ UNCHANGED converge
+
+Gossip(n, o) ≜
+ ∧ S!Gossip(n, o)
+ ∧ UNCHANGED converge
+
+Converge ≜
+ ∧ converge' = TRUE
+ ∧ UNCHANGED counter
+
+Next ≜
+ ∨ ∃ n ∈ Node : Increment(n)
+ ∨ ∃ n, o ∈ Node : Gossip(n, o)
+ ∨ Converge
+
+Fairness ≜ ∀ n, o ∈ Node : WF_vars(Gossip(n, o))
+
+Spec ≜
+ ∧ Init
+ ∧ □[Next]_vars
+ ∧ Fairness
+
+=============================================================================
+```
+Of note is our new `Liveness` property, which states `converge` being true *leads to* (`↝`) our convergence condition:
+```tla
+Liveness ≜ converge ↝ S!Convergence
+```
+We also require an additional *fairness assumption* to satisfy this property, which states `Gossip` operations must actually happen and the system can't just obstinately sit doing nothing forever:
+```tla
+Fairness ≜ ∀ n, o ∈ Node : WF_vars(Gossip(n, o))
+```
+At this point we have to consider how to actually manage the (currently infinite) state of the model.
+We can run the modelchecker if we want, with this configuration:
+```sh
+SPECIFICATION Spec
+CONSTANT Node = {n1, n2, n3}
+INVARIANTS TypeOK Safety
+PROPERTIES Liveness Monotonicity
+```
+It will of course run forever.
+
+We can quickly define a state restriction in `MC_CRDT`:
+```tla
+StateConstraint ≜ ∀ n, o ∈ Node : counter[n][o] ≤ 3
+```
+Then use this configuration:
+```sh
+SPECIFICATION Spec
+CONSTANT Node = {n1, n2, n3}
+INVARIANTS TypeOK Safety
+PROPERTIES Liveness Monotonicity
+CONSTRAINT StateConstraint
+```
+The modelchecker will find 50,000 states and validates our `TypeOK` & `Safety` invariants against all of them (yay!), but silently ignores the `Liveness` and `Monotonicity` properties due to the inclusion of the state constraint.
+Here we have to deploy the technique we developed up above: constraining divergence & using garbage collection.
+We add a new `Divergence` constant and a `GarbageCollect` action:
+```tla
+------------------------------- MODULE MC_CRDT ------------------------------
+EXTENDS Naturals
+
+CONSTANTS Node, Divergence
+
+VARIABLES counter, converge
+
+vars ≜ ⟨counter, converge⟩
+
+S ≜ INSTANCE CRDT
+
+TypeOK ≜
+ ∧ S!TypeOK
+ ∧ counter ∈ [Node → [Node → 0 ‥ Divergence]]
+ ∧ converge ∈ BOOLEAN
+
+Safety ≜ S!Safety
+
+Monotonicity ≜ S!Monotonicity
+
+Liveness ≜ converge ⇒ S!Liveness
+
+Init ≜
+ ∧ S!Init
+ ∧ converge = FALSE
+
+Increment(n) ≜
+ ∧ ¬converge
+ ∧ counter[n][n] < Divergence
+ ∧ S!Increment(n)
+ ∧ UNCHANGED converge
+
+Gossip(n, o) ≜
+ ∧ S!Gossip(n, o)
+ ∧ UNCHANGED converge
+
+Converge ≜
+ ∧ converge' = TRUE
+ ∧ UNCHANGED counter
+
+GarbageCollect ≜
+ LET SetMin(s) ≜ CHOOSE e ∈ s : ∀ o ∈ s : e ≤ o IN
+ LET Transpose ≜ SetMin({counter[n][o] : n, o ∈ Node}) IN
+ ∧ counter' = [
+ n ∈ Node ↦ [
+ o ∈ Node ↦ counter[n][o] - Transpose
+ ]
+ ]
+ ∧ UNCHANGED converge
+
+Next ≜
+ ∨ ∃ n ∈ Node : Increment(n)
+ ∨ ∃ n, o ∈ Node : Gossip(n, o)
+ ∨ Converge
+ ∨ GarbageCollect
+
+Fairness ≜ ∀ n, o ∈ Node : WF_vars(Gossip(n, o))
+
+Spec ≜
+ ∧ Init
+ ∧ □[Next]_vars
+ ∧ Fairness
+
+=============================================================================
+```
+Note in the `Increment` action we have:
+```tla
+ ∧ counter[n][n] < Divergence
+```
+preventing any individual counter from exceeding our divergence constraint.
+The `GarbageCollect` action finds a counter value exceeded by every counter on every node, and subtracts it from all of them to transpose the counters closer to zero.
+
+We're ready!
+We can run the model with this configuration:
+```sh
+SPECIFICATION Spec
+CONSTANTS
+ Node = {n1, n2, n3}
+ Divergence = 3
+INVARIANTS TypeOK Safety
+PROPERTY Liveness
+```
+Once again the modelchecker finds 50,000 states, but this time it can actually run the liveness checking!
+Our `Safety` invariant passes like before, but this time our `Liveness` property passes as well!
+So our system is shown to converge as hoped.
+
+Unfortunately, our `Monotonicity` property doesn't fare as well.
+If we check:
+```sh
+PROPERTIES Liveness Monotonicity
+```
+We see that `Monotonicity` fails to hold whenever a `GarbageCollect` step occurs, which is unsurprising.
+Recall the statement of `Monotonicity`:
+```tla
+Monotonic ≜ ∀ n, o ∈ Node : counter'[n][o] ≥ counter[n][o]
+Monotonicity ≜ □[Monotonic]_counter
+```
+Since `GarbageCollect` decreases the values of all the elements of `counter`, this is clearly violated.
+How can we rescue the concept of monotonicity here?
+Transposition maintains the *relative* values of the counters, despite their absolute values changing.
+Another way to say this is that every counter changes by the same amount:
+```tla
+Monotonicity ≜ □[
+ ∨ S!Monotonic
+ ∨ ∀ a, b, c, d ∈ Node :
+ (counter'[a][b] - counter[a][b]) = (counter'[c][d] - counter[c][d])
+]_vars
+```
+This passes!
+We have now completed a demonstrative example of modelchecking a monotonic system.
+This approach can be applied to any other monotonic system.
+We can tune the divergence constraint to trade off between state exploration and ease of modelchecking; in our model of three nodes, this looks like:
+
+| Divergence | Distinct States | Modelcheck Time |
+|------------|-----------------|-----------------|
+| 1 | 264 | <1s |
+| 2 | 5232 | 1s |
+| 3 | 50,000 | 7s |
+| 4 | 300,750 | 50s |
+| 5 | 1,335,642 | 4m20s |
+
+By comparison keeping divergence at 3 but increasing the number of nodes to 4 scales the state space much faster: it hit 20 million distinct states before I killed the process after about an hour.
+It's possible to use symmetry reduction to collapse the number of states introduced by nodes, but you can see why most models only use three nodes!
+The combinatorial state explosion is real.
+
+## Modeling a replicated log
+
+I'll here sketch a similar tactic for modeling a replicated log.
+Replicated logs have transactions appended to them, growing forever.
+Not only that, they're brutal to modelcheck: since every action is recorded in the log, states gain path dependence.
+If action `A` occurs before action `B`, and it leads to the same outward system state as if `B` occurs before `A`, the modelchecker will nonetheless treat these as separate states because the order of `A` and `B` was recorded in the log.
+This gives *factorial* state explosion, restricting us to very short logs.
+In some systems this is barely enough to get things initialized, let alone explore interesting behavior.
+
+Our approach can help with both problems.
+Remember we only care about restricting divergence: here, that means divergence of how far behind a node is in executing log transactions.
+Nodes in the cluster process the log at different rates, and some can lag behind others.
+As before this causes a lot of interesting behavior.
+If we limit this divergence, then nodes can't add additional transactions to the log if that would push a node outside the execution divergence limit.
+On the other end, our garbage collection step will remove transactions from the beginning of the log once all nodes have executed them.
+Easy!
+
+[According to A. Jesse Jiryu Davis of MongoDB](https://groups.google.com/g/tlaplus/c/3V1JxNDSoas/m/3Y81pxi2AQAJ), this approach is similar to how some real-world replicated logs work (although usually the lagging nodes are kicked out instead of execution being paused).
+A nice bonus.
+You can find an example replicated log spec (and the CRDT spec from up above) [here](https://github.com/ahelwer/Examples/tree/057148b2fc8cdb21914fb3ba840681c22cf8c0f3/specifications/FiniteMonotonic).
+
+## Alternatives & future work
+
+This post didn't even touch the built-in TLA⁺ proof language, which might have found use here.
+Infinity is not an obstacle to mathematical induction!
+There are also alternative state representations which could have been used, to tighten the analogy to Lamport's *Real Time* approach.
+Instead of a garbage collection step resetting the state, the specs could have been rewritten to track state divergence explicitly.
+Another way of saying this is garbage collection could be built in to the CRDT model's `Gossip` step: the counters are normalized at the end of it.
+This might have been more elegant, potentially at the cost of making the spec harder to understand.
+It certainly would improve modelcheck time by reducing extraneous state transitions.
+
+I had previously written a spec of a real-world replicated log system (detailed in a [past post](/post/2023-04-05-checkpoint-coordination/)) that used the state restriction method to curtail infinity.
+It would be nice to go back and apply our new approach to an existing spec, not greenfield demonstration projects as in this post.
+Perhaps you'll see an update in a few months!
+
+I also have an upcoming industry contract to specify a database system that includes both monotonic counters and replicated logs, and I'm excited to see how this new approach pans out.
+If you'd like to hire me for a similar contract, contact consulting@disjunctive.llc!
+
+## Discussions
+
+ * [lobste.rs](https://lobste.rs/s/mo4epa/wrangling_monotonic_systems_tla)
+ * [fediverse](https://fosstodon.org/@ahelwer/111336831792925594)
+ * [TLA⁺ mailing list](https://groups.google.com/g/tlaplus/c/3V1JxNDSoas/m/ffHjY1VwFgAJ)
+ * [Hacker News](https://news.ycombinator.com/item?id=38103225)
+ * [LinkedIn](https://www.linkedin.com/posts/ahelwer_wrangling-monotonic-systems-in-tla-activity-7125557738771779584-Xwv3)
+
diff --git a/specifications/FiniteMonotonic/CRDT.tla b/specifications/FiniteMonotonic/CRDT.tla
new file mode 100644
index 00000000..5ddf74e5
--- /dev/null
+++ b/specifications/FiniteMonotonic/CRDT.tla
@@ -0,0 +1,41 @@
+------------------------------- MODULE CRDT ---------------------------------
+
+EXTENDS Naturals
+
+CONSTANT Node
+
+VARIABLE counter
+
+TypeOK == counter \in [Node -> [Node -> Nat]]
+
+Safety == \A n, o \in Node : counter[n][n] >= counter[o][n]
+
+Monotonic == \A n, o \in Node : counter'[n][o] >= counter[n][o]
+
+Monotonicity == [][Monotonic]_counter
+
+Convergence == \A n, o \in Node : counter[n] = counter[o]
+
+Init == counter = [n \in Node |-> [o \in Node |-> 0]]
+
+Increment(n) == counter' = [counter EXCEPT ![n][n] = @ + 1]
+
+Gossip(n, o) ==
+ LET Max(a, b) == IF a > b THEN a ELSE b IN
+ counter' = [
+ counter EXCEPT ![o] = [
+ nodeView \in Node |->
+ Max(counter[n][nodeView], counter[o][nodeView])
+ ]
+ ]
+
+Next ==
+ \/ \E n \in Node : Increment(n)
+ \/ \E n, o \in Node : Gossip(n, o)
+
+Spec ==
+ /\ Init
+ /\ [][Next]_counter
+
+=============================================================================
+
diff --git a/specifications/FiniteMonotonic/Constrain_CRDT.cfg b/specifications/FiniteMonotonic/Constrain_CRDT.cfg
new file mode 100644
index 00000000..82ca291e
--- /dev/null
+++ b/specifications/FiniteMonotonic/Constrain_CRDT.cfg
@@ -0,0 +1,6 @@
+SPECIFICATION Spec
+CONSTANT Node = {n1, n2, n3}
+INVARIANTS TypeOK Safety
+PROPERTIES Monotonicity Liveness
+CONSTRAINT StateConstraint
+
diff --git a/specifications/FiniteMonotonic/Constrain_CRDT.tla b/specifications/FiniteMonotonic/Constrain_CRDT.tla
new file mode 100644
index 00000000..9b58eb05
--- /dev/null
+++ b/specifications/FiniteMonotonic/Constrain_CRDT.tla
@@ -0,0 +1,55 @@
+-------------------------- MODULE Constrain_CRDT ----------------------------
+
+EXTENDS Naturals
+
+CONSTANT Node
+
+VARIABLES counter, converge
+
+vars == <>
+
+S == INSTANCE CRDT
+
+TypeOK ==
+ /\ S!TypeOK
+ /\ converge \in BOOLEAN
+
+Safety == S!Safety
+
+Monotonicity == S!Monotonicity
+
+Liveness == converge ~> S!Convergence
+
+Init ==
+ /\ S!Init
+ /\ converge = FALSE
+
+Increment(n) ==
+ /\ ~converge
+ /\ S!Increment(n)
+ /\ UNCHANGED converge
+
+Gossip(n, o) ==
+ /\ S!Gossip(n, o)
+ /\ UNCHANGED converge
+
+Converge ==
+ /\ converge' = TRUE
+ /\ UNCHANGED counter
+
+Next ==
+ \/ \E n \in Node : Increment(n)
+ \/ \E n, o \in Node : Gossip(n, o)
+ \/ Converge
+
+Fairness == \A n, o \in Node : WF_vars(Gossip(n, o))
+
+StateConstraint == \A n, o \in Node : counter[n][o] <= 3
+
+Spec ==
+ /\ Init
+ /\ [][Next]_vars
+ /\ Fairness
+
+=============================================================================
+
diff --git a/specifications/FiniteMonotonic/Finitize_CRDT.cfg b/specifications/FiniteMonotonic/Finitize_CRDT.cfg
new file mode 100644
index 00000000..43e5af04
--- /dev/null
+++ b/specifications/FiniteMonotonic/Finitize_CRDT.cfg
@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+ Node = {n1, n2, n3}
+ Divergence = 3
+INVARIANTS TypeOK Safety
+PROPERTIES Liveness Monotonicity
+
diff --git a/specifications/FiniteMonotonic/Finitize_CRDT.tla b/specifications/FiniteMonotonic/Finitize_CRDT.tla
new file mode 100644
index 00000000..f24c39ab
--- /dev/null
+++ b/specifications/FiniteMonotonic/Finitize_CRDT.tla
@@ -0,0 +1,72 @@
+--------------------------- MODULE Finitize_CRDT ----------------------------
+
+EXTENDS Naturals
+
+CONSTANTS Node, Divergence
+
+VARIABLES counter, converge
+
+vars == <>
+
+S == INSTANCE CRDT
+
+TypeOK ==
+ /\ S!TypeOK
+ /\ counter \in [Node -> [Node -> 0 .. Divergence]]
+ /\ converge \in BOOLEAN
+
+Safety == S!Safety
+
+Monotonicity == [][
+ \/ S!Monotonic
+ \/ \A a, b, c, d \in Node :
+ (counter'[a][b] - counter[a][b]) = (counter'[c][d] - counter[c][d])
+]_vars
+
+Liveness == converge ~> S!Convergence
+
+Init ==
+ /\ S!Init
+ /\ converge = FALSE
+
+Increment(n) ==
+ /\ ~converge
+ /\ counter[n][n] < Divergence
+ /\ S!Increment(n)
+ /\ UNCHANGED converge
+
+Gossip(n, o) ==
+ /\ S!Gossip(n, o)
+ /\ UNCHANGED converge
+
+Converge ==
+ /\ converge' = TRUE
+ /\ UNCHANGED counter
+
+GarbageCollect ==
+ LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
+ LET Transpose == SetMin({counter[n][o] : n, o \in Node}) IN
+ /\ counter' = [
+ n \in Node |-> [
+ o \in Node |-> counter[n][o] - Transpose
+ ]
+ ]
+ /\ UNCHANGED converge
+
+Next ==
+ \/ \E n \in Node : Increment(n)
+ \/ \E n, o \in Node : Gossip(n, o)
+ \/ Converge
+ \/ GarbageCollect
+
+Fairness == \A n, o \in Node : WF_vars(Gossip(n, o))
+
+StateConstraint == \A n, o \in Node : counter[n][o] <= 4
+
+Spec ==
+ /\ Init
+ /\ [][Next]_vars
+ /\ Fairness
+
+=============================================================================
+
diff --git a/specifications/FiniteMonotonic/Finitize_ReplicatedLog.cfg b/specifications/FiniteMonotonic/Finitize_ReplicatedLog.cfg
new file mode 100644
index 00000000..027b7109
--- /dev/null
+++ b/specifications/FiniteMonotonic/Finitize_ReplicatedLog.cfg
@@ -0,0 +1,8 @@
+SPECIFICATION Spec
+CONSTANTS
+ Node = {n1, n2, n3}
+ Transaction = {tx1, tx2, tx3}
+ Divergence = 5
+INVARIANT TypeOK
+PROPERTY Liveness
+
diff --git a/specifications/FiniteMonotonic/Finitize_ReplicatedLog.tla b/specifications/FiniteMonotonic/Finitize_ReplicatedLog.tla
new file mode 100644
index 00000000..4a5a46a7
--- /dev/null
+++ b/specifications/FiniteMonotonic/Finitize_ReplicatedLog.tla
@@ -0,0 +1,59 @@
+---------------------- MODULE Finitize_ReplicatedLog ------------------------
+
+EXTENDS Naturals, Sequences
+
+CONSTANTS Node, Transaction, Divergence
+
+VARIABLES log, executed, converge
+
+vars == <>
+
+S == INSTANCE ReplicatedLog
+
+TypeOK ==
+ /\ log \in Seq(Transaction)
+ /\ Len(log) <= Divergence
+ /\ executed \in [Node -> 0 .. Divergence]
+
+Liveness == converge ~> S!Convergence
+
+Init ==
+ /\ S!Init
+ /\ converge = FALSE
+
+WriteTx(n, tx) ==
+ /\ ~converge
+ /\ Len(log) < Divergence
+ /\ S!WriteTx(n, tx)
+ /\ UNCHANGED converge
+
+ExecuteTx(n) ==
+ /\ S!ExecuteTx(n)
+ /\ UNCHANGED converge
+
+GarbageCollect ==
+ LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
+ LET MinExecuted == SetMin({executed[o] : o \in Node}) IN
+ /\ log' = [i \in 1 .. Len(log) - MinExecuted |-> log[i + MinExecuted]]
+ /\ executed' = [n \in Node |-> executed[n] - MinExecuted]
+ /\ UNCHANGED converge
+
+Converge ==
+ /\ converge' = TRUE
+ /\ UNCHANGED <>
+
+Fairness == \A n \in Node : WF_vars(ExecuteTx(n))
+
+Next ==
+ \/ \E n \in Node : \E tx \in Transaction : WriteTx(n, tx)
+ \/ \E n \in Node : ExecuteTx(n)
+ \/ GarbageCollect
+ \/ Converge
+
+Spec ==
+ /\ Init
+ /\ [][Next]_vars
+ /\ Fairness
+
+=============================================================================
+
diff --git a/specifications/FiniteMonotonic/README.md b/specifications/FiniteMonotonic/README.md
new file mode 100644
index 00000000..39c96687
--- /dev/null
+++ b/specifications/FiniteMonotonic/README.md
@@ -0,0 +1,14 @@
+These specifications illustrate a technique for taking ordinarily-infinite monotonic systems and turning them finite for the purposes of model-checking.
+Briefly, this is accomplished by limiting the maximum divergence (difference between lowest and highest value) of any monotonic variable across the system, then continually transposing the set of monotonic variables to their lowest value.
+The technique is explained at length in [this](BlogPost.md) blog post.
+
+Specs & models include:
+- `CRDT.tla`: the "good copy" spec of a basic grow-only counter CRDT
+- `Finitize_CRDT.tla`: wraps `CRDT.tla` and implements the finitization technique
+- `Finitize_CRDT.cfg`: a model for `Finitize_CRDT.tla`
+- `Constrain_CRDT.tla`: finitizes `CRDT.tla` using state constraints instead; included for comparison
+- `Constrain_CRDT.cfg`: a model for `Constrain_CRDT.tla`
+- `ReplicatedLog.tla`: the "good copy" spec of a basic append-only replicated log
+- `Finitize_ReplicatedLog.tla`: wraps `ReplicatedLog.tla` and implements the finitization technique
+- `Finitize_ReplicatedLog.cfg`: a model for `Finitize_ReplicatedLog.tla`
+
diff --git a/specifications/FiniteMonotonic/ReplicatedLog.tla b/specifications/FiniteMonotonic/ReplicatedLog.tla
new file mode 100644
index 00000000..9a50abf8
--- /dev/null
+++ b/specifications/FiniteMonotonic/ReplicatedLog.tla
@@ -0,0 +1,39 @@
+--------------------------- MODULE ReplicatedLog ----------------------------
+EXTENDS Naturals, Sequences
+
+CONSTANTS Node, Transaction
+
+VARIABLES log, executed
+
+vars == <>
+
+TypeOK ==
+ /\ log \in Seq(Transaction)
+ /\ executed \in [Node -> Nat]
+
+Convergence == \A n \in Node : executed[n] = Len(log)
+
+Init ==
+ /\ log = <<>>
+ /\ executed = [n \in Node |-> 0]
+
+WriteTx(n, tx) ==
+ /\ executed[n] = Len(log)
+ /\ log' = Append(log, tx)
+ /\ executed' = [executed EXCEPT ![n] = @ + 1]
+
+ExecuteTx(n) ==
+ /\ executed[n] < Len(log)
+ /\ executed' = [executed EXCEPT ![n] = @ + 1]
+ /\ UNCHANGED log
+
+Next ==
+ \/ \E n \in Node : \E tx \in Transaction: WriteTx(n, tx)
+ \/ \E n \in Node : ExecuteTx(n)
+
+Spec ==
+ /\ Init
+ /\ [][Next]_vars
+
+=============================================================================
+