diff --git a/README.md b/README.md
index ef97fa4d..8aa16616 100644
--- a/README.md
+++ b/README.md
@@ -100,6 +100,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
 | [Yo-Yo Leader Election](specifications/YoYo)                                                        | Ludovic Yvoz, Stephan Merz                          |          |             |         |      ✔    |          |
 | [TCP as defined in RFC 9293](specifications/tcp)                                                    | Markus Kuppe                                        |          |             |         |      ✔    |          |
+| [B-trees](specifications/btree)                                                                     | Lorin Hochstein                                     |          |             |         |      ✔    |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                                      |          |             |         |           |          |
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |             |         |           |          |
 | [Buffered Random Access File](specifications/braf)                                                  | Calvin Loncaric                                     |          |             |         |     ✔     |          |
diff --git a/specifications/btree/README.md b/specifications/btree/README.md
new file mode 100644
index 00000000..1b5ad57b
--- /dev/null
+++ b/specifications/btree/README.md
@@ -0,0 +1,2 @@
+TLA⁺ specification of a [B-tree](https://en.wikipedia.org/wiki/B-tree) datastructure by [Lorin Hochstein](https://lorinhochstein.org/), sourced from [this git repo](https://github.com/lorin/btree-tla) and covered at length in [this blog post](https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/).
+
diff --git a/specifications/btree/btree.cfg b/specifications/btree/btree.cfg
new file mode 100644
index 00000000..25036df5
--- /dev/null
+++ b/specifications/btree/btree.cfg
@@ -0,0 +1,35 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    READY = ready
+    GET_VALUE = get_value
+    FIND_LEAF_TO_ADD = find_leaf_to_add
+    WHICH_TO_SPLIT = which_to_split
+
+    ADD_TO_LEAF = add_to_leaf
+    SPLIT_ROOT_LEAF = split_root_leaf
+    SPLIT_ROOT_INNER = split_root_inner
+    SPLIT_INNER = split_inner
+    SPLIT_LEAF = split_leaf
+    UPDATE_LEAF = update_leaf
+
+
+    NIL = nil
+    MISSING = missing
+
+    Vals = {x,y,z}
+
+    MaxOccupancy = 2
+    MaxNode = 8
+    MaxKey = 4
+
+\* PROPERTY
+\* Refinement
+
+INVARIANT
+TypeOk
+InnersMustHaveLast
+LeavesCantHaveLast
+KeyOrderPreserved
+KeysInLeavesAreUnique
+FreeNodesRemain
diff --git a/specifications/btree/btree.tla b/specifications/btree/btree.tla
new file mode 100644
index 00000000..7efe170e
--- /dev/null
+++ b/specifications/btree/btree.tla
@@ -0,0 +1,317 @@
+\* Note: deletes have not been implemented
+---- MODULE btree ----
+EXTENDS TLC,
+        Naturals,
+        FiniteSets,
+        Sequences
+
+CONSTANTS Vals,
+          MaxKey,
+          MaxNode,
+          MaxOccupancy,
+
+          \* states
+          READY,
+          GET_VALUE,
+          FIND_LEAF_TO_ADD,
+          WHICH_TO_SPLIT,
+          ADD_TO_LEAF,
+          SPLIT_LEAF,
+          SPLIT_INNER,
+          SPLIT_ROOT_LEAF,
+          SPLIT_ROOT_INNER,
+          UPDATE_LEAF
+
+Keys == 1..MaxKey
+Nodes == 1..MaxNode
+
+NIL == CHOOSE x : x \notin Nodes
+MISSING == CHOOSE v : v \notin Vals
+
+
+VARIABLES root,
+          isLeaf, keysOf, childOf, lastOf, valOf,
+          focus,
+          toSplit,
+          op, args, ret,
+          state
+
+TypeOk == /\ root \in Nodes
+          /\ isLeaf \in [Nodes -> BOOLEAN]
+          /\ keysOf \in [Nodes -> SUBSET Keys]
+          /\ childOf \in [Nodes \X Keys -> Nodes \union {NIL}]
+          /\ lastOf \in [Nodes -> Nodes \union {NIL}]
+          /\ valOf \in [Nodes \X Keys -> Vals \union {NIL}]
+          /\ focus \in Nodes \union {NIL}
+          /\ toSplit \in Seq(Nodes)
+          /\ op \in {"get", "insert", "update", NIL}
+          /\ ret \in Vals \union {"ok", "error", MISSING, NIL}
+          /\ state \in {READY, GET_VALUE, FIND_LEAF_TO_ADD, WHICH_TO_SPLIT, ADD_TO_LEAF, SPLIT_LEAF, SPLIT_INNER, SPLIT_ROOT_LEAF, SPLIT_ROOT_INNER, UPDATE_LEAF}
+
+\* Max element in a set
+Max(xs) == CHOOSE x \in xs : (\A y \in xs \ {x} : x > y)
+
+\* Find the appropriate child node associated with the key
+ChildNodeFor(node, key) ==
+    LET keys == keysOf[node]
+        maxKey == Max(keys)
+        closestKey ==  CHOOSE k \in keys : /\ k>key
+                                           /\ ~(\E j \in keys \ {k} : j>key /\ j<k)
+    IN IF keys = {} \/ key >= maxKey
+       THEN lastOf[node]
+       \* smallest k that's bigger than key
+       ELSE
+       childOf[node, closestKey]
+
+
+\* Identify the leaf node based on key
+\* Find the leaf node associated with a key
+RECURSIVE FindLeafNode(_, _)
+FindLeafNode(node, key) ==
+    IF isLeaf[node] THEN node ELSE FindLeafNode(ChildNodeFor(node, key), key)
+
+AtMaxOccupancy(node) == Cardinality(keysOf[node]) = MaxOccupancy
+
+
+\* We model a "free" (not yet part of the tree) node as one as a leaf with no keys
+IsFree(node) == isLeaf[node] /\ keysOf[node] = {}
+
+ChooseFreeNode == CHOOSE n \in Nodes : IsFree(n)
+
+
+Init == /\ isLeaf = [n \in Nodes |-> TRUE]
+        /\ keysOf = [n \in Nodes |-> {}]
+        /\ childOf = [n \in Nodes, k \in Keys |-> NIL]
+        /\ lastOf = [n \in Nodes |-> NIL]
+        /\ valOf = [n \in Nodes, k \in Keys |-> NIL]
+        /\ root = ChooseFreeNode
+        /\ focus = NIL
+        /\ toSplit = <<>>
+        /\ op = NIL
+        /\ args = NIL
+        /\ ret = NIL
+        /\ state = READY
+
+GetReq(key) == 
+    /\ state = READY
+    /\ op' = "get"
+    /\ args' = <<key>>
+    /\ ret' = NIL
+    /\ state' = GET_VALUE
+    /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit>>
+
+GetValue ==
+    LET key == args[1] 
+        node == FindLeafNode(root, key) IN
+    /\ state = GET_VALUE
+    /\ state' = READY
+    /\ ret' = IF key \in keysOf[node] THEN valOf[node, key] ELSE MISSING
+    /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit, args, op>>
+    
+
+InsertReq(key, val) ==
+    /\ state = READY
+    /\ op' = "insert"
+    /\ args' = <<key, val>>
+    /\ ret' = NIL
+    /\ state' = FIND_LEAF_TO_ADD
+    /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit>>
+
+UpdateReq(key, val) ==
+    LET leaf == FindLeafNode(root, key)
+    IN /\ state = READY
+       /\ op' = "update"
+       /\ args' = <<key, val>>
+       /\ ret' = NIL
+       /\ focus' = leaf
+       /\ state' = UPDATE_LEAF
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, toSplit>>
+
+UpdateLeaf ==
+    LET key == args[1]
+        val == args[2]
+    IN /\ state = UPDATE_LEAF
+       /\ valOf' = IF key \in keysOf[focus] THEN [valOf EXCEPT ![focus, key]=val] ELSE valOf
+       /\ ret' = IF key \in keysOf[focus] THEN "ok" ELSE "error"
+       /\ state' = READY
+       /\ focus' = NIL
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, toSplit, args, op>>
+
+FindLeafToAdd ==
+    LET key == args[1]
+        leaf == FindLeafNode(root, key)
+    IN /\ state = FIND_LEAF_TO_ADD
+       /\ focus' = leaf
+       /\ toSplit' = IF AtMaxOccupancy(leaf) THEN <<leaf>> ELSE <<>>
+       /\ state' = IF AtMaxOccupancy(leaf) THEN WHICH_TO_SPLIT ELSE ADD_TO_LEAF
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, args, op, ret>>
+
+
+ParentOf(n) == CHOOSE p \in Nodes: \/ \E k \in Keys: n = childOf[p, k]
+                                   \/ lastOf[p]=n
+
+WhichToSplit ==
+    LET  node == Head(toSplit)
+         parent == ParentOf(node)
+         splitParent == AtMaxOccupancy(parent)
+         noMoreSplits == ~splitParent  \* if the parent doesn't need splitting, we don't need to consider more nodes for splitting
+    IN /\ state = WHICH_TO_SPLIT
+       /\ toSplit' =
+           CASE node = root   -> toSplit
+             [] splitParent   -> <<parent>> \o toSplit
+             [] OTHER         -> toSplit
+       /\ state' =
+            CASE node # root /\ noMoreSplits /\ isLeaf[node]  -> SPLIT_LEAF
+              [] node # root /\ noMoreSplits /\ ~isLeaf[node] -> SPLIT_INNER
+              [] node = root /\ isLeaf[node]                  -> SPLIT_ROOT_LEAF
+              [] node = root /\ ~isLeaf[node]                 -> SPLIT_ROOT_INNER
+              [] OTHER                                        -> WHICH_TO_SPLIT
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, op, args, ret, focus>>
+
+\* Adding the <<key, val>> pair in args to the node indicated by focus
+\* If the key is already present, this is an error
+AddToLeaf ==
+    LET key == args[1]
+        val == args[2] IN
+       /\ state = ADD_TO_LEAF
+       /\ ret' = IF key \notin keysOf[focus] THEN "ok" ELSE "error"
+       /\ keysOf' = IF key \notin keysOf[focus] THEN [keysOf EXCEPT ![focus]=@ \union {key}] ELSE keysOf
+       /\ valOf' = IF key \notin keysOf[focus] THEN [valOf EXCEPT ![focus,key]=val] ELSE valOf
+       /\ state' = READY
+       /\ UNCHANGED <<root, isLeaf, childOf, lastOf, op, args, focus, toSplit>>
+
+\* Return the pivot (midpoint) of a set of keys. If there are an even number of keys, bias towards the smaller one
+PivotOf(keys) == CHOOSE k \in keys :
+    LET smaller == {x \in keys : x < k}
+        larger == {x \in keys: x > k} IN
+     \/ Cardinality(smaller) = Cardinality(larger)
+     \/ Cardinality(smaller) = Cardinality(larger)+1
+
+SplitRootLeaf ==
+    LET n1 == Head(toSplit)
+        n2 == ChooseFreeNode
+        newRoot == CHOOSE n \in Nodes : IsFree(n) /\ (n # n2)
+        keys == keysOf[n1]
+        pivot == PivotOf(keys)
+        n1Keys == {x \in keys: x<pivot}
+        n2Keys == {x \in keys: x>=pivot} 
+        keyToInsert == args[1] IN
+    /\ state = SPLIT_ROOT_LEAF
+    /\ root' = newRoot
+    /\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=TRUE]
+    /\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
+    /\ childOf' = [childOf EXCEPT ![newRoot, pivot]=n1]
+    /\ lastOf' = [lastOf EXCEPT ![newRoot]=n2]
+    /\ valOf' = [n \in Nodes, k \in Keys |->
+        CASE n=n1 /\ k \in n2Keys -> NIL
+          [] n=n2 /\ k \in n2Keys -> valOf[n1, k]
+          [] OTHER                -> valOf[n, k]]
+    \* No more splits necessary, add the focus to the leaf
+    \* Note that the focus may have changed due to the split
+    /\ state' = ADD_TO_LEAF
+    /\ focus' = IF keyToInsert < pivot THEN n1 ELSE n2
+    /\ UNCHANGED <<op, args, ret, toSplit>>
+
+ParentKeyOf(node) ==
+    LET p == ParentOf(node) IN
+    CHOOSE k \in keysOf[p]: childOf[p, k] = node
+
+IsLastOfParent(node) == lastOf[ParentOf(node)] = node
+
+SplitRootInner ==
+    LET n1 == Head(toSplit)
+        n2 == ChooseFreeNode
+        newRoot == CHOOSE n \in Nodes : IsFree(n) /\ (n # n2)
+        keys == keysOf[n1]
+        pivot == PivotOf(keys)
+        (* when splitting an inner node, pivot does not appear in either node, only in parent *)
+        n1Keys == {x \in keys: x<pivot}
+        n2Keys == {x \in keys: x>pivot} IN
+    /\ state = SPLIT_ROOT_INNER
+    /\ root' = newRoot
+    /\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=FALSE]
+    /\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
+    /\ childOf' = [n \in Nodes, k \in Keys |->
+        CASE n=newRoot /\ k=pivot -> n1
+          [] n=n1 /\ k \in n2Keys -> NIL
+          [] n=n1 /\ k \in n1Keys -> childOf[n1, k]
+          [] n=n2 /\ k \in n2Keys -> childOf[n1, k]
+          [] OTHER                -> childOf[n, k]]
+    /\ lastOf' = [lastOf EXCEPT ![newRoot]=n2, ![n1]=childOf[n1, pivot], ![n2]=lastOf[n1]]
+    /\ toSplit' = <<>>
+    /\ state' = ADD_TO_LEAF
+    /\ UNCHANGED <<op, args, ret, focus, valOf>>
+
+SplitLeaf ==
+    LET n1 == Head(toSplit)
+        n2 == ChooseFreeNode
+        keys == keysOf[n1]
+        pivot == PivotOf(keys)
+        parent == ParentOf(n1)
+        n1Keys == {x \in keys: x<pivot}
+        n2Keys == {x \in keys: x>=pivot}
+        keyToInsert == args[1]
+    IN
+    /\ state = SPLIT_LEAF
+    /\ isLeaf' = [isLeaf EXCEPT ![n2]=TRUE]
+    /\ keysOf' = [keysOf EXCEPT ![parent]=@ \union {pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
+    \* In the parent, point the pivot key to n1, and point the parent key to n2.
+    \* TODO: handle the edge case where n1 was the last element
+    /\ childOf' = IF IsLastOfParent(n1)
+                  THEN [childOf EXCEPT ![parent, pivot]=n1]
+                  ELSE [childOf EXCEPT ![parent, pivot]=n1, ![parent, ParentKeyOf(n1)]=n2]
+    /\ lastOf' = IF IsLastOfParent(n1) THEN [lastOf EXCEPT ![parent]=n2] ELSE lastOf
+    /\ valOf' = [n \in Nodes, k \in Keys |->
+        CASE n=n1 /\ k \in n2Keys -> NIL
+          [] n=n2 /\ k \in n2Keys -> valOf[n1, k]
+          [] OTHER                -> valOf[n, k]]
+    /\ state' = ADD_TO_LEAF
+    /\ focus' = IF keyToInsert < pivot THEN n1 ELSE n2
+    /\ UNCHANGED <<root, toSplit, op, args, ret>>
+
+
+Next == \/ \E key \in Keys, val \in Vals : 
+            \/ InsertReq(key, val)
+            \/ UpdateReq(key, val)
+        \/ \E key \in Keys: GetReq(key)
+        \/ GetValue
+        \/ FindLeafToAdd
+        \/ WhichToSplit
+        \/ AddToLeaf
+        \/ SplitLeaf
+        \/ SplitRootLeaf
+        \/ SplitRootInner
+        \/ UpdateLeaf
+
+vars == <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit, op, args, ret, state>>
+
+Spec == Init /\ [][Next]_vars /\ WF_op(\E key \in Keys: GetReq(key))
+
+\*
+\* Refinement mapping
+\*
+
+Leaves == {n \in Nodes : isLeaf[n]}
+
+Mapping == INSTANCE kvstore
+    WITH dict <- [key \in Keys |-> IF \E leaf \in Leaves : key \in keysOf[leaf] 
+                                 THEN LET leaf == CHOOSE leaf \in Leaves : key \in keysOf[leaf] 
+                                      IN valOf[leaf, key] ELSE MISSING],
+         state <- IF state = READY THEN "ready" ELSE "working"
+
+
+Refinement == Mapping!Spec
+
+\*
+\* Invariants
+\*
+Inners == {n \in Nodes: ~isLeaf[n]}
+
+InnersMustHaveLast == \A n \in Inners : lastOf[n] # NIL
+KeyOrderPreserved == \A n \in Inners : (\A k \in keysOf[n] : (\A kc \in keysOf[childOf[n, k]]: kc < k))
+LeavesCantHaveLast == \A n \in Leaves : lastOf[n] = NIL
+KeysInLeavesAreUnique ==
+    \A n1, n2 \in Leaves : ((keysOf[n1] \intersect keysOf[n2]) # {}) => n1=n2
+FreeNodesRemain == \E n \in Nodes : IsFree(n)
+
+====
\ No newline at end of file
diff --git a/specifications/btree/kvstore.cfg b/specifications/btree/kvstore.cfg
new file mode 100644
index 00000000..b2a7eaa0
--- /dev/null
+++ b/specifications/btree/kvstore.cfg
@@ -0,0 +1,20 @@
+SPECIFICATION Spec
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+CONSTANTS
+    Keys = {"A", "B", "C"}
+    Vals = {X, Y, Z}
+    NIL = NIL
+    MISSING = "missing"
+
+\* INIT Init
+\* NEXT Next
+
+\* PROPERTY
+
+\* Uncomment the previous line and add property names
+
+
+INVARIANT
+TypeOK
\ No newline at end of file
diff --git a/specifications/btree/kvstore.tla b/specifications/btree/kvstore.tla
new file mode 100644
index 00000000..8f21cc9e
--- /dev/null
+++ b/specifications/btree/kvstore.tla
@@ -0,0 +1,140 @@
+(*
+
+# Operations
+
+* get
+* insert
+* update
+* delete
+
+## get
+Return NIL if the key is not in the store
+
+## insert
+Return "ok" on success
+Return "error" if the key already exists
+
+## update
+Return "ok" on success
+Return "error" if the key does not exist
+
+## delete
+
+Always returns "ok"
+
+*)
+---- MODULE kvstore ----
+CONSTANTS Keys, Vals, MISSING, NIL
+
+Ops == {"get", "insert", "delete", "update"}
+
+ASSUME MISSING \notin Vals
+ASSUME NIL \notin Vals \union Ops \union {MISSING}
+
+VARIABLES op,
+    args,
+    ret,
+    state,
+    dict \* tracks mapping of keys to values
+
+TypeOK ==
+    /\ args \in {<<k>>: k \in Keys} \union {<<k,v>>: k \in Keys, v \in Vals} \union {NIL}
+    /\ dict \in [Keys -> Vals \union {MISSING}]
+    /\ op \in Ops \union {NIL} \* initial state for Ops is NIL
+    /\ ret \in Vals \union {"ok", "error", MISSING, NIL}
+    /\ state \in {"ready", "working"}
+
+Init ==
+    /\ op = NIL
+    /\ args = NIL
+    /\ ret = NIL
+    /\ dict = [k \in Keys |-> MISSING]
+    /\ state = "ready"
+
+GetReq(key) ==
+    /\ state = "ready"
+    /\ op' = "get"
+    /\ args' = <<key>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED dict
+
+GetResp == LET key == args[1] IN
+    /\ op = "get"
+    /\ ret' = dict[key]
+    /\ state' = "ready"
+    /\ UNCHANGED <<op, args, dict>>
+
+InsertReq(key, val) ==
+    /\ state = "ready"
+    /\ op' = "insert"
+    /\ args' = <<key, val>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED <<dict>>
+
+Present(key) == dict[key] \in Vals
+Absent(key) == dict[key] = MISSING
+
+InsertResp == LET key == args[1]
+                  val == args[2] IN
+       /\ op = "insert"
+       /\ state = "working"
+       /\ dict' = IF Absent(key)
+                  THEN [dict EXCEPT ![key] = val]
+                  ELSE dict
+       /\ ret' = IF Absent(key) THEN "ok" ELSE "error"
+       /\ state' = "ready"
+       /\ UNCHANGED <<op, args>>
+
+UpdateReq(key, val) ==
+    /\ state = "ready"
+    /\ op' = "update"
+    /\ args' = <<key, val>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED dict
+
+UpdateResp ==
+    LET key == args[1]
+        val == args[2]
+    IN /\ op = "update"
+       /\ ret' = IF Present(key) THEN "ok" ELSE "error"
+       /\ dict' = IF Present(key)
+                  THEN [dict EXCEPT ![key]=val]
+                  ELSE dict
+       /\ state' = "ready"
+       /\ UNCHANGED <<op, args>>
+
+DeleteReq(key) ==
+    /\ state = "ready"
+    /\ op' = "delete"
+    /\ args' = <<key>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED dict
+
+\* we permit deleting keys that aren't there
+DeleteResp ==
+    LET key == args[1]
+    IN /\ op = "delete"
+       /\ ret' = "ok"
+       /\ state' = "ready"
+       /\ dict' = [dict EXCEPT ![key]=MISSING]
+       /\ UNCHANGED <<op, args>>
+
+Next == \/ \E k \in Keys: 
+           \/ GetReq(k)
+           \/ DeleteReq(k)
+           \/ \E v \in Vals: \/ InsertReq(k, v)  
+                             \/ UpdateReq(k, v)
+        \/ GetResp
+        \/ InsertResp
+        \/ UpdateResp
+        \/ DeleteResp
+
+vars == <<op, args, ret, dict, state>>
+
+Spec == Init /\ [][Next]_vars /\ WF_op(\E k \in Keys: DeleteReq(k))
+
+====
\ No newline at end of file
diff --git a/specifications/btree/manifest.json b/specifications/btree/manifest.json
new file mode 100644
index 00000000..e456745d
--- /dev/null
+++ b/specifications/btree/manifest.json
@@ -0,0 +1,51 @@
+{
+  "path": "specifications/btree",
+  "title": "B-trees",
+  "description": "Operations on B-trees. Includes a refinement mapping to a key-value store spec.",
+  "sources": [
+    "https://github.com/lorin/btree-tla",
+    "https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/"
+  ],
+  "authors": [
+    "Lorin Hochstein"
+  ],
+  "tags": [],
+  "modules": [
+    {
+      "path": "specifications/btree/btree.tla",
+      "communityDependencies": [],
+      "tlaLanguageVersion": 2,
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/btree/btree.cfg",
+          "runtime": "00:00:15",
+          "size": "small",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 374727,
+          "totalStates": 2820091,
+          "stateDepth": 40
+        }
+      ]
+    },
+    {
+      "path": "specifications/btree/kvstore.tla",
+      "communityDependencies": [],
+      "tlaLanguageVersion": 2,
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/btree/kvstore.cfg",
+          "runtime": "00:00:01",
+          "size": "small",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 2641,
+          "totalStates": 28585,
+          "stateDepth": 11
+        }
+      ]
+    }
+  ]
+}
\ No newline at end of file
