diff --git a/docs/spec/README.md b/docs/spec/README.md
index 48bc904f..2f6f5c4c 100644
--- a/docs/spec/README.md
+++ b/docs/spec/README.md
@@ -1,9 +1,9 @@
 # Specification
 
 This directory served as location for English and TLA+
-specifications of the Tendermint protocols "fast sync" and "light
+specifications of the CometBFT protocols "fast sync" and "light
 client". The corresponding specification work is not happening in this directory
-anymore but in the [tendermint/spec](https://github.com/tendermint/spec)
-repository. The most recent versions of the specifications can be found
-there.
+anymore but in the [spec](https://github.com/cometbft/cometbft/tree/main/spec)
+directory of the CometBFT repository.
+The most recent versions of the specifications can be found there.
 
diff --git a/docs/spec/fastsync/README.md b/docs/spec/fastsync/README.md
index 2d6335e7..5548de13 100644
--- a/docs/spec/fastsync/README.md
+++ b/docs/spec/fastsync/README.md
@@ -9,7 +9,7 @@ for the most recent version.
 ## Abstract
 
 This directory contains English and TLA+ specifications for the FastSync
-protocol as it is currently implemented in the Tendermint Core codebase.
+protocol as it is currently implemented in the CometBFT Core codebase.
 
 ## English Specification
 
@@ -36,7 +36,7 @@ the redundancies between them, improve their utility to researchers and
 engineers, and to improve their verifiability. For now, they provide a complete
 description of the fast sync protocol in TLA+; especially the
 [scheduler.tla](scheduler.tla), which maps very closely to the current
-implementation of the [scheduler in Go](https://github.com/tendermint/tendermint/blockchain/v2/scheduler.go).
+implementation of the [scheduler in Go](https://github.com/cometbft/cometbft/blockchain/v2/scheduler.go).
 
 The [scheduler.tla](scheduler.tla) can be model checked in TLC with the following
 parameters:
diff --git a/docs/spec/fastsync/Tinychain.tla b/docs/spec/fastsync/Tinychain.tla
index dc30812e..55e5b044 100644
--- a/docs/spec/fastsync/Tinychain.tla
+++ b/docs/spec/fastsync/Tinychain.tla
@@ -3,7 +3,7 @@
 
    https://github.com/tendermint/spec/tree/master/rust-spec/fastsync
 
-   A very abstract model of Tendermint blockchain. Its only purpose is to highlight
+   A very abstract model of CometBFT blockchain. Its only purpose is to highlight
    the relation between validator sets, next validator sets, and last commits.
  *)
 
diff --git a/docs/spec/fastsync/fastsync.md b/docs/spec/fastsync/fastsync.md
index 7cf62b60..e5339f51 100644
--- a/docs/spec/fastsync/fastsync.md
+++ b/docs/spec/fastsync/fastsync.md
@@ -9,25 +9,25 @@ for the most recent version.
 ## Abstract
 
 Fastsync is a protocol that is used by a node to catch-up to the
-current state of a Tendermint blockchain. Its typical use case is a
+current state of a CometBFT blockchain. Its typical use case is a
 node that was disconnected from the system for some time. The
 recovering node locally has a copy of a prefix of the blockchain,
 and the corresponding application state that is slightly outdated. It
 then queries its peers for the blocks that were decided on by the
-Tendermint blockchain during the period the full node was
+CometBFT blockchain during the period the full node was
 disconnected. After receiving these blocks, it executes the
 transactions in the blocks in order to catch-up to the current height
 of the blockchain and the corresponding application state.
 
 In practice it is sufficient to catch-up only close to the current
-height: The Tendermint consensus reactor implements its own catch-up
+height: The CometBFT consensus reactor implements its own catch-up
 functionality and can synchronize a node that is close to the current height,
 perhaps within 10 blocks away from the current height of the blockchain.
 Fastsync should bring a node within this range.
 
 ## Outline
 
-- [Part I](#part-i---tendermint-blockchain): Introduction of Tendermint
+- [Part I](#part-i---cometbft-blockchain): Introduction of CometBFT
 blockchain terms that are relevant for FastSync protocol.
 
 - [Part II](#part-ii---sequential-definition-of-fastsync-problem): Introduction
@@ -84,7 +84,7 @@ In this document we quite extensively use tags in order to be able to
 reference assumptions, invariants, etc. in future communication. In
 these tags we frequently use the following short forms:
 
-- TMBC: Tendermint blockchain
+- TMBC: CometBFT blockchain
 - SEQ: for sequential specifications
 - FS: Fastsync
 - LIVE: liveness
@@ -96,9 +96,9 @@ these tags we frequently use the following short forms:
 - NewFS: refers to improved future Fastsync implementations
 
 
-# Part I - Tendermint Blockchain
+# Part I - CometBFT Blockchain
 
-We will briefly list some of the notions of Tendermint blockchains that are
+We will briefly list some of the notions of CometBFT blockchains that are
 required for this specification. More details can be found [here][block].
 
 #### **[TMBC-HEADER]**:
@@ -111,7 +111,7 @@ headers, rather than a list of blocks.
 
 #### **[TMBC-SEQ]**:
 
-The Tendermint blockchain is a list *chain* of headers.
+The CometBFT blockchain is a list *chain* of headers.
 
 #### **[TMBC-SEQ-GROW]**:
 
@@ -201,7 +201,7 @@ A full node has as input a block of the blockchain at height *h* and
 the corresponding application state (or the prefix of the current
 blockchain until height *h*). It has access to a set *peerIDs* of full
 nodes called *peers* that it knows of.  The full node uses the peers
-to read blocks of the Tendermint blockchain (in a safe way, that is,
+to read blocks of the CometBFT blockchain (in a safe way, that is,
 it checks the soundness conditions), until it has read the most recent
 block and then terminates.
 
@@ -216,7 +216,7 @@ as output (i) a list *L* of blocks starting at height *h* to some height
 *terminationHeight*, and (ii) the application state when applying the
 transactions of the list *L* to *s*.
 
-> In Tendermint, the commit for block of height *h* is contained in block *h + 1*,
+> In CometBFT, the commit for block of height *h* is contained in block *h + 1*,
 > and thus the block of height *h + 1* is needed to verify the block of
 > height *h*. Let us therefore clarify the following on the
 > termination height:
@@ -338,7 +338,7 @@ Initially, the set *peerIDs* contains at least one correct full node.
 > of the blockchain (it might lag behind), the property [FS-SEQ-SAFE-START]
 > cannot be ensured in an unreliable distributed setting. We consider
 > the following relaxation. (Which is typically sufficient for
-> Tendermint, as the consensus reactor then synchronizes from that
+> CometBFT, as the consensus reactor then synchronizes from that
 > height.)
 
 #### **[FS-DIST-SAFE-START]**:
@@ -420,7 +420,7 @@ are structured as finite state machines that receive input events and emit
 output events. The demuxer is responsible for all IO, including translating
 between internal events and IO messages, and routing events between components.
 
-Protocols in Tendermint can be considered to consist of two
+Protocols in CometBFT can be considered to consist of two
 components: a "core" state machine and a "peer" state machine. The core state
 machine refers to the internal state managed by the node, while the peer state
 machine determines what messages to send to peers. In the FastSync design, the
@@ -428,7 +428,7 @@ core and peer state machines correspond to the processor and scheduler,
 respectively.
 
 In the case of FastSync, the core state machine (the processor) is effectively
-just the Tendermint block execution function, while virtually all protocol logic
+just the CometBFT block execution function, while virtually all protocol logic
 is contained in the peer state machine (the scheduler). The processor is
 only implemented as a separate component due to the computationally expensive nature
 of block execution. We therefore focus our specification here on the peer state machine
@@ -548,7 +548,7 @@ type bcBlockResponseMessage struct {
 ```
 
 Remark:
-- `msg.Block` is a Tendermint block as defined in [[block]].
+- `msg.Block` is a CometBFT block as defined in [[block]].
 - `msg.Block` != nil
 
 #### bcStatusRequestMessage
@@ -1142,7 +1142,7 @@ Arguments:
 
 [[block]] Specification of the block data structure.
 
-<!-- [[blockchain]] The specification of the Tendermint blockchain. Tags referring to this specification are labeled [TMBC-*]. -->
+<!-- [[blockchain]] The specification of the CometBFT blockchain. Tags referring to this specification are labeled [TMBC-*]. -->
 
 [block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md
 
diff --git a/docs/spec/fastsync/fastsync.tla b/docs/spec/fastsync/fastsync.tla
index 357daa63..0c54d278 100644
--- a/docs/spec/fastsync/fastsync.tla
+++ b/docs/spec/fastsync/fastsync.tla
@@ -6,7 +6,7 @@
 
  In this document we give the high level specification of the fast sync
  protocol as implemented here:
- https://github.com/tendermint/tendermint/tree/main/blockchain/v2.
+ https://github.com/cometbft/cometbft/tree/main/blockchain/v2.
 
 We assume a system in which one node is trying to sync with the blockchain
 (replicated state machine) by downloading blocks from the set of full nodes
@@ -230,7 +230,7 @@ InitNode ==
 
 \* Remove faulty peers.
 \* Returns new block pool.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222
 RemovePeers(rmPeers, bPool) ==
     LET keepPeers == bPool.peerIds \ rmPeers IN
     LET pHeights ==
@@ -258,7 +258,7 @@ RemovePeers(rmPeers, bPool) ==
     ELSE bPool
 
 \* Add a peer.
-\* see https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198
+\* see https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198
 AddPeer(peer, bPool) ==
     [bPool EXCEPT !.peerIds = bPool.peerIds \union {peer}]
 
@@ -268,7 +268,7 @@ Handle StatusResponse message.
 If valid status response, update peerHeights.
 If invalid (height is smaller than the current), then remove peer.
 Returns new block pool.
-See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667
+See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667
 *)
 HandleStatusResponse(msg, bPool) ==
     LET peerHeight == bPool.peerHeights[msg.peerId] IN
@@ -286,7 +286,7 @@ Handle BlockResponse message.
 If valid block response, update blockStore, pendingBlocks and receivedBlocks.
 If invalid (unsolicited response or malformed block), then remove peer.
 Returns new block pool.
-See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522
+See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522
 *)
 HandleBlockResponse(msg, bPool) ==
     LET h == msg.block.height IN
@@ -308,7 +308,7 @@ HandleBlockResponse(msg, bPool) ==
        
 
 \* Compute max peer height.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440
 MaxPeerHeight(bPool) ==
     IF bPool.peerIds = AsPidSet({})
     THEN 0 \* no peers, just return 0
@@ -317,7 +317,7 @@ MaxPeerHeight(bPool) ==
 
 (* Returns next height for which request should be sent.
    Returns NilHeight in case there is no height for which request can be sent.
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *)
 FindNextRequestHeight(bPool) ==
     LET S == {i \in Heights:
                 /\ i >= bPool.height
@@ -341,7 +341,7 @@ NumOfPendingRequests(bPool, peer) ==
 
 (* Returns peer that can serve block for a given height.
    Returns NilPeer in case there are no such peer.
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *)
 FindPeerToServe(bPool, h) ==
     LET peersThatCanServe == { p \in bPool.peerIds:
                 /\ bPool.peerHeights[p] >= h
@@ -379,23 +379,23 @@ CreateRequest(bPool) ==
 
 
 \* Returns node state, i.e., defines termination condition.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432
 ComputeNextState(bPool) ==
     IF bPool.syncedBlocks = 0  \* corresponds to the syncTimeout in case no progress has been made for a period of time.
     THEN "finished"
     ELSE IF /\ bPool.height > 1
-            /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566
+            /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/cometbft/cometbft/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566
          THEN "finished"
          ELSE "running"
 
 (* Verify if commit is for the given block id and if commit has enough voting power.
-   See https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *)
+   See https://github.com/cometbft/cometbft/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *)
 VerifyCommit(block, lastCommit) ==
     PossibleCommit(block, lastCommit)
 
 (* Tries to execute next block in the pool, i.e., defines block validation logic.
    Returns new block pool (peers that has send invalid blocks are removed).
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *)
 ExecuteBlocks(bPool) ==
     LET bStore == bPool.blockStore IN
     LET block0 == bStore[bPool.height - 1] IN
@@ -426,7 +426,7 @@ ExecuteBlocks(bPool) ==
 
 
 \* Defines logic for pruning peers.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613
 TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
     (* -----------------------------------------------------------------------------------------------------------------------*)
     (* Corresponds to function prunablePeers in scheduler.go file. Note that this function only checks if block has been  *)
@@ -436,7 +436,7 @@ TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
     (* In case of faulty peers, we don't have any guarantee that they will respond.                                           *)
     (* Therefore, we model this with nondeterministic behavior as it could lead to peer removal, for both correct and faulty. *)
     (* See scheduler.go                                                                                                       *)
-    (* https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *)
+    (* https://github.com/cometbft/cometbft/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *)
     LET toRemovePeers == bPool.peerIds \intersect suspectedSet IN
 
     (*
@@ -446,7 +446,7 @@ TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
       correct peers respond timely and reliably. However, if a request is sent to a faulty peer then we 
       might get response on time or not, which is modelled with nondeterministic isTimedOut flag.
       See scheduler.go
-      https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617
+      https://github.com/cometbft/cometbft/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617
     *)
     LET nextHeightPeer == bPool.pendingBlocks[bPool.height] IN
     LET prunablePeers ==
diff --git a/docs/spec/fastsync/scheduler.tla b/docs/spec/fastsync/scheduler.tla
index e66b3bfb..14b2e9d6 100644
--- a/docs/spec/fastsync/scheduler.tla
+++ b/docs/spec/fastsync/scheduler.tla
@@ -6,7 +6,7 @@
 
  A specification of the fast sync scheduler that is introduced in blockchain/v2:
  
- https://github.com/tendermint/tendermint/tree/brapse/blockchain-v2-riri-reactor-2
+ https://github.com/cometbft/cometbft/tree/brapse/blockchain-v2-riri-reactor-2
  
  The model includes:
     - a scheduler that maintains the peers and blocks that it receives from the peers, and
@@ -108,7 +108,7 @@ OutEvents ==
 (* ----------------------------------------------------------------------------------------------*)
 (* The behavior of the scheduler that keeps track of peers, block requests and responses, etc.   *)
 (* See scheduler.go                                                                              *)
-(* https://github.com/tendermint/tendermint/blob/v0.33.3/blockchain/v2/scheduler.go              *)
+(* https://github.com/cometbft/cometbft/blob/v0.33.3/blockchain/v2/scheduler.go              *)
 (* ----------------------------------------------------------------------------------------------*)
 
 addPeer(sc, peerID) == 
@@ -244,7 +244,7 @@ highPeers(sc, minH) == {p \in sc.peers: sc.peerHeights[p] >= minH}
 (* ----------------------------------------------------------------------------------------------*)
 (* The behavior of the scheduler state machine                                                   *)
 (* See scheduler.go                                                                              *)
-(* https://github.com/tendermint/tendermint/tree/brapse/blockchain-v2-riri-reactor-2/scheduler.go*)
+(* https://github.com/cometbft/cometbft/tree/brapse/blockchain-v2-riri-reactor-2/scheduler.go*)
 (* ----------------------------------------------------------------------------------------------*)
 blStateInit(h, start) ==
   IF h <= start THEN
diff --git a/docs/spec/fastsync/verification/Tinychain.tla b/docs/spec/fastsync/verification/Tinychain.tla
index b8a21299..9d3e91a8 100644
--- a/docs/spec/fastsync/verification/Tinychain.tla
+++ b/docs/spec/fastsync/verification/Tinychain.tla
@@ -1,5 +1,5 @@
 -------------------------- MODULE Tinychain ----------------------------------
-(* A very abstract model of Tendermint blockchain. Its only purpose is to highlight
+(* A very abstract model of CometBFT blockchain. Its only purpose is to highlight
    the relation between validator sets, next validator sets, and last commits.
  *)
 
diff --git a/docs/spec/fastsync/verification/fastsync_apalache.tla b/docs/spec/fastsync/verification/fastsync_apalache.tla
index 2322ca44..2dc7c0b2 100644
--- a/docs/spec/fastsync/verification/fastsync_apalache.tla
+++ b/docs/spec/fastsync/verification/fastsync_apalache.tla
@@ -2,7 +2,7 @@
 (*
  In this document we give the high level specification of the fast sync
  protocol as implemented here:
- https://github.com/tendermint/tendermint/tree/main/blockchain/v2.
+ https://github.com/cometbft/cometbft/tree/main/blockchain/v2.
 
 We assume a system in which one node is trying to sync with the blockchain
 (replicated state machine) by downloading blocks from the set of full nodes
@@ -226,7 +226,7 @@ InitNode ==
 
 \* Remove faulty peers.
 \* Returns new block pool.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L222
 RemovePeers(rmPeers, bPool) ==
     LET keepPeers == bPool.peerIds \ rmPeers IN
     LET pHeights ==
@@ -254,7 +254,7 @@ RemovePeers(rmPeers, bPool) ==
     ELSE bPool
 
 \* Add a peer.
-\* see https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198
+\* see https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L198
 AddPeer(peer, bPool) ==
     [bPool EXCEPT !.peerIds = bPool.peerIds \union {peer}]
 
@@ -264,7 +264,7 @@ Handle StatusResponse message.
 If valid status response, update peerHeights.
 If invalid (height is smaller than the current), then remove peer.
 Returns new block pool.
-See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667
+See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L667
 *)
 HandleStatusResponse(msg, bPool) ==
     LET peerHeight == bPool.peerHeights[msg.peerId] IN
@@ -282,7 +282,7 @@ Handle BlockResponse message.
 If valid block response, update blockStore, pendingBlocks and receivedBlocks.
 If invalid (unsolicited response or malformed block), then remove peer.
 Returns new block pool.
-See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522
+See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L522
 *)
 HandleBlockResponse(msg, bPool) ==
     LET h == msg.block.height IN
@@ -304,7 +304,7 @@ HandleBlockResponse(msg, bPool) ==
        
 
 \* Compute max peer height.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L440
 MaxPeerHeight(bPool) ==
     IF bPool.peerIds = AsPidSet({})
     THEN 0 \* no peers, just return 0
@@ -313,7 +313,7 @@ MaxPeerHeight(bPool) ==
 
 (* Returns next height for which request should be sent.
    Returns NilHeight in case there is no height for which request can be sent.
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L454 *)
 FindNextRequestHeight(bPool) ==
     LET S == {i \in Heights:
                 /\ i >= bPool.height
@@ -337,7 +337,7 @@ NumOfPendingRequests(bPool, peer) ==
 
 (* Returns peer that can serve block for a given height.
    Returns NilPeer in case there are no such peer.
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L477 *)
 FindPeerToServe(bPool, h) ==
     LET peersThatCanServe == { p \in bPool.peerIds:
                 /\ bPool.peerHeights[p] >= h
@@ -375,23 +375,23 @@ CreateRequest(bPool) ==
 
 
 \* Returns node state, i.e., defines termination condition.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L432
 ComputeNextState(bPool) ==
     IF bPool.syncedBlocks = 0  \* corresponds to the syncTimeout in case no progress has been made for a period of time.
     THEN "finished"
     ELSE IF /\ bPool.height > 1
-            /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566
+            /\ bPool.height >= MaxPeerHeight(bPool) \* see https://github.com/cometbft/cometbft/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/scheduler.go#L566
          THEN "finished"
          ELSE "running"
 
 (* Verify if commit is for the given block id and if commit has enough voting power.
-   See https://github.com/tendermint/tendermint/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *)
+   See https://github.com/cometbft/cometbft/blob/61057a8b0af2beadee106e47c4616b279e83c920/blockchain/v2/processor_context.go#L12 *)
 VerifyCommit(block, lastCommit) ==
     PossibleCommit(block, lastCommit)
 
 (* Tries to execute next block in the pool, i.e., defines block validation logic.
    Returns new block pool (peers that has send invalid blocks are removed).
-   See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *)
+   See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/processor.go#L135 *)
 ExecuteBlocks(bPool) ==
     LET bStore == bPool.blockStore IN
     LET block0 == bStore[bPool.height - 1] IN
@@ -422,7 +422,7 @@ ExecuteBlocks(bPool) ==
 
 
 \* Defines logic for pruning peers.
-\* See https://github.com/tendermint/tendermint/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613
+\* See https://github.com/cometbft/cometbft/blob/dac030d6daf4d3e066d84275911128856838af4e/blockchain/v2/scheduler.go#L613
 TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
     (* -----------------------------------------------------------------------------------------------------------------------*)
     (* Corresponds to function prunablePeers in scheduler.go file. Note that this function only checks if block has been  *)
@@ -432,7 +432,7 @@ TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
     (* In case of faulty peers, we don't have any guarantee that they will respond.                                           *)
     (* Therefore, we model this with nondeterministic behavior as it could lead to peer removal, for both correct and faulty. *)
     (* See scheduler.go                                                                                                       *)
-    (* https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *)
+    (* https://github.com/cometbft/cometbft/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L335 *)
     LET toRemovePeers == bPool.peerIds \intersect suspectedSet IN
 
     (*
@@ -442,7 +442,7 @@ TryPrunePeer(bPool, suspectedSet, isTimedOut) ==
       correct peers respond timely and reliably. However, if a request is sent to a faulty peer then we 
       might get response on time or not, which is modelled with nondeterministic isTimedOut flag.
       See scheduler.go
-      https://github.com/tendermint/tendermint/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617
+      https://github.com/cometbft/cometbft/blob/4298bbcc4e25be78e3c4f21979d6aa01aede6e87/blockchain/v2/scheduler.go#L617
     *)
     LET nextHeightPeer == bPool.pendingBlocks[bPool.height] IN
     LET prunablePeers ==
diff --git a/docs/spec/lightclient/README.md b/docs/spec/lightclient/README.md
index 779de85f..8c16bc49 100644
--- a/docs/spec/lightclient/README.md
+++ b/docs/spec/lightclient/README.md
@@ -3,7 +3,7 @@
 ## Disclaimer
 
 This specification is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/)
 for the most recent version.
 
 ## Abstract
@@ -11,8 +11,8 @@ for the most recent version.
 
 This directory contains work-in-progress English and TLA+ specifications for the Light Client
 protocol. Implementations of the light client can be found in
-[Rust](https://github.com/informalsystems/tendermint-rs/tree/main/light-client) and
-[Go](https://github.com/tendermint/tendermint/tree/main/light).
+[Rust](https://github.com/cometbft/cometbft-rs/tree/main/light-client) and
+[Go](https://github.com/cometbft/cometbft/tree/main/light).
 
 Light clients are assumed to be initialized once from a trusted source 
 with a trusted header and validator set. The light client
@@ -29,9 +29,9 @@ The light client is decomposed into three components:
 
 The [English specification](verification/verification.md) describes the light client
 commit verification problem in terms of the temporal properties
-[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/main/docs/spec/lightclient/verification/verification.md#lcv-dist-safe1) and 
-[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/main/docs/spec/lightclient/verification/verification.md#lcv-dist-live1). 
-Commit verification is assumed to operate within the Tendermint Failure Model, where +2/3 of validators are correct for some time period and
+[LCV-DIST-SAFE.1](https://github.com/cometbft/cometbft-rs/blob/main/docs/spec/lightclient/verification/verification.md#lcv-dist-safe1) and 
+[LCV-DIST-LIVE.1](https://github.com/cometbft/cometbft-rs/blob/main/docs/spec/lightclient/verification/verification.md#lcv-dist-live1). 
+Commit verification is assumed to operate within the CometBFT Failure Model, where +2/3 of validators are correct for some time period and
 validator sets can change arbitrarily at each height.
 
 A light client protocol is also provided, including all checks that
diff --git a/docs/spec/lightclient/attacks/evidence-handling.md b/docs/spec/lightclient/attacks/evidence-handling.md
index 688177b3..46c50bb2 100644
--- a/docs/spec/lightclient/attacks/evidence-handling.md
+++ b/docs/spec/lightclient/attacks/evidence-handling.md
@@ -1,7 +1,7 @@
 # Disclaimer
 
 This specification is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/)
 for the most recent version.
 
 
@@ -25,7 +25,7 @@ detects an attack, it needs to send to a witness only missing data (common heigh
 and conflicting light block) as it has its trace. Keeping light client attack data of constant size 
 saves bandwidth and reduces an attack surface. As we will explain below, although in the context of 
 light client core 
-[verification](https://github.com/informalsystems/tendermint-rs/tree/main/docs/spec/lightclient/verification) 
+[verification](https://github.com/cometbft/cometbft-rs/tree/main/docs/spec/lightclient/verification) 
 the roles of primary and witness are clearly defined, 
 in case of the attack, we run the same attack detection procedure twice where the roles are swapped. 
 The rationale is that the light client does not know what peer is correct (on a right main branch) 
@@ -76,7 +76,7 @@ The following invariant holds for the primary trace:
 ### Witness with a conflicting header
 
 The verified header at height `h` is cross-checked with every witness as part of 
-[detection](https://github.com/informalsystems/tendermint-rs/tree/main/docs/spec/lightclient/detection). 
+[detection](https://github.com/cometbft/cometbft-rs/tree/main/docs/spec/lightclient/detection). 
 If a witness returns the conflicting header at the height `h` the following procedure is executed to verify 
 if the conflicting header comes from the valid trace and if that's the case to create an attack evidence:
 
@@ -143,7 +143,7 @@ func DetectLightClientAttack(trace []LightBlock, peer PeerID) (LightClientAttack
 As part of on chain evidence handling, full nodes identifies misbehaving processes and informs
 the application, so they can be slashed. Note that only bonded validators should 
 be reported to the application. There are three types of attacks that can be executed against 
-Tendermint light client: 
+CometBFT light client: 
   - lunatic attack
   - equivocation attack and 
   - amnesia attack.  
diff --git a/docs/spec/lightclient/detection/README.md b/docs/spec/lightclient/detection/README.md
index 244af7ed..5e01137a 100644
--- a/docs/spec/lightclient/detection/README.md
+++ b/docs/spec/lightclient/detection/README.md
@@ -1,10 +1,10 @@
 
-# Tendermint fork detection and IBC fork detection
+# CometBFT fork detection and IBC fork detection
 
 ## Disclaimer
 
 This directory is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/detection/)
 for the most recent version.
 
 
@@ -12,7 +12,7 @@ for the most recent version.
 
 This is a work in progress.
 This directory captures the ongoing work and discussion on fork
-detection both in the context of a Tendermint light node and in the
+detection both in the context of a CometBFT light node and in the
 context of IBC. It contains the following files
 
 ### [detection.md](./detection.md)
@@ -36,7 +36,7 @@ A collection of ideas and intuitions from recent discussions
 
 - a collection of requirements for fork detection in the IBC
   context. In particular it contains a section "Required Changes in
-  ICS 007" with necessary updates to ICS 007 to support Tendermint
+  ICS 007" with necessary updates to ICS 007 to support CometBFT
   fork detection
 
 
@@ -62,18 +62,18 @@ We decided to merge the files while there are still open points to
 address to record the current state an move forward. In particular,
 the following points need to be addressed:
 
-- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466504876
+- https://github.com/cometbft/cometbft-rs/pull/479#discussion_r466504876
 
-- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466493900
+- https://github.com/cometbft/cometbft-rs/pull/479#discussion_r466493900
   
-- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466489045
+- https://github.com/cometbft/cometbft-rs/pull/479#discussion_r466489045
   
-- https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466491471
+- https://github.com/cometbft/cometbft-rs/pull/479#discussion_r466491471
   
 Most likely we will write a specification on the light client
 supervisor along the outcomes of
   
-- https://github.com/informalsystems/tendermint-rs/pull/509
+- https://github.com/cometbft/cometbft-rs/pull/509
 
 that also addresses initialization
 
diff --git a/docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection/detection.md
index 7149c886..18a17c8e 100644
--- a/docs/spec/lightclient/detection/detection.md
+++ b/docs/spec/lightclient/detection/detection.md
@@ -2,7 +2,7 @@
 # Disclaimer
 
 This specification is  an unfinished draft and not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/detection/)
 for the most recent version.
 
 
@@ -10,7 +10,7 @@ for the most recent version.
 # Fork detector
 
 A detector (or detector for short) is a mechanism that expects as
-input a header with some height *h*, connects to different Tendermint
+input a header with some height *h*, connects to different CometBFT
 full nodes, requests the header of height *h* from them, and then
 cross-checks the headers and the input header.
 
@@ -44,12 +44,12 @@ node) to the future.
 ## Context of this document
 
 The light client verification specification [[verification]] is
-designed for the Tendermint failure model (1/3 assumption)
+designed for the CometBFT failure model (1/3 assumption)
 [TMBC-FM-2THIRDS]. It is safe under this assumption, and live
 if it can reliably (that is, no message loss, no duplication, and
 eventually delivered) and timely communicate with a correct full node. If
 this assumption is violated, the light client can be fooled to trust a
-header that was not generated by Tendermint consensus.
+header that was not generated by CometBFT consensus.
 
 This specification, the fork detector, is a "second line of defense",
 in case the 1/3 assumption is violated. Its goal is to detect fork (conflicting headers) and collect
@@ -67,7 +67,7 @@ with the primary, and then cross-checks the header with the
 secondaries using this specification.
 
 
-### Tendermint Consensus and Forks
+### CometBFT Consensus and Forks
 
 #### **[TMBC-GENESIS.1]**
 Let *Genesis* be the agreed-upon initial block (file).
@@ -88,7 +88,7 @@ Let *b* and *c* be two light blocks. We define **supports(b,c,t)**
 
 
 > The following formalizes that *b* was properly generated by
-> Tendermint; *b* can be traced back to genesis
+> CometBFT; *b* can be traced back to genesis
 
 #### **[TMBC-SEQ-ROOTED.1]**
 Let *b* be a light block. 
@@ -113,7 +113,7 @@ time t there exists an *h* and a sequence *a(1)*, ... *a(h)* s.t.
 
 > **TODO:** I believe the following definition
 > corresponds to **Slashable fork** in
-> [forks][tendermintfork]. Please confirm!  
+> [forks][cometbftfork]. Please confirm!  
 > Observe that sign-skip-match  is even defined if there is a fork on
 > the chain.
 
@@ -144,9 +144,9 @@ We say we have **a fork at height** *b.Header.Height*.
 
 > **TODO:** I think the following definition is
 > the intuition behind **main chain forks**
-> in the document on [forks][tendermintfork]. However, main chain
+> in the document on [forks][cometbftfork]. However, main chain
 > forks were defined more operational "forks that are observed by
-> full nodes as part of normal Tendermint consensus protocol". Please
+> full nodes as part of normal CometBFT consensus protocol". Please
 > confirm! 
   
 #### **[TMBC-SIGN-UNIQUE.1]**
@@ -706,7 +706,7 @@ func ForkDetector(ls LightStore, PoFs PoFStore)
 
 [[verification]] The specification of the light client verification.
 
-[[tendermintfork]] Tendermint fork detection and accountability
+[[cometbftfork]] CometBFT fork detection and accountability
 
 [[accountability]] Fork accountability
 
@@ -723,8 +723,8 @@ func ForkDetector(ls LightStore, PoFs PoFStore)
 
 [verificationVDD]: https://github.com/informalsystems/VDD/blob/master/lightclient/failuredetector.md
 
-[verification]: https://github.com/informalsystems/tendermint-rs/blob/main/docs/spec/lightclient/verification.md
+[verification]: https://github.com/cometbft/cometbft-rs/blob/main/docs/spec/lightclient/verification.md
 
 [accountability]: https://github.com/tendermint/spec/blob/master/spec/consensus/light-client/accountability.md
 
-[tendermintfork]: https://docs.google.com/document/d/1xjyp5JOPt7QfHem1AFEaowBH2Plk0IHACWtYFXFvO7E/edit#heading=h.th2369ptc2ve
+[cometbftfork]: https://docs.google.com/document/d/1xjyp5JOPt7QfHem1AFEaowBH2Plk0IHACWtYFXFvO7E/edit#heading=h.th2369ptc2ve
diff --git a/docs/spec/lightclient/detection/discussions.md b/docs/spec/lightclient/detection/discussions.md
index 2cfcabb9..1b0ea50a 100644
--- a/docs/spec/lightclient/detection/discussions.md
+++ b/docs/spec/lightclient/detection/discussions.md
@@ -1,7 +1,7 @@
 ## Disclaimer
 
 This document is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/)
+[tendermint/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/detection/)
 for the most recent version.
 
 
diff --git a/docs/spec/lightclient/detection/draft-functions.md b/docs/spec/lightclient/detection/draft-functions.md
index 4c8a7ad5..4b036966 100644
--- a/docs/spec/lightclient/detection/draft-functions.md
+++ b/docs/spec/lightclient/detection/draft-functions.md
@@ -4,7 +4,7 @@
 ## Disclaimer
 
 This specification is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/detection/)
 for the most recent version.
 
 ## Abstract
diff --git a/docs/spec/lightclient/detection/req-ibc-detection.md b/docs/spec/lightclient/detection/req-ibc-detection.md
index 1010bce5..b6404f2f 100644
--- a/docs/spec/lightclient/detection/req-ibc-detection.md
+++ b/docs/spec/lightclient/detection/req-ibc-detection.md
@@ -3,7 +3,7 @@
 ## Disclaimer
 
 This specification is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/detection/)
 for the most recent version.
 
 ## What you need to know about IBC
@@ -14,13 +14,13 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics
 
 ### Components and their interface
 
-#### Tendermint Blockchains
+#### CometBFT Blockchains
 
 > I assume you know what that is.
 
-#### An IBC/Tendermint correspondence
+#### An IBC/CometBFT correspondence
 
-| IBC Term | Tendermint-RS Spec Term | Comment |
+| IBC Term | CometBFT-RS Spec Term | Comment |
 |----------|-------------------------| --------|
 | `CommitmentRoot` | AppState | app hash |
 | `ConsensusState` | Lightblock | not all fields are there. NextValidator is definitely needed |
@@ -68,7 +68,7 @@ https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics
 - ICS 002 states w.r.t. `queryChainConsensusState` that "Note that
   retrieval of past consensus states by height (as opposed to just the
   current consensus state) is convenient but not required." For
-  Tendermint fork detection, this seems to be a necessity.
+  CometBFT fork detection, this seems to be a necessity.
   
 - `Header` should become a lightblock
 
@@ -99,7 +99,7 @@ A blockchain runs a **handler** that passively collects information about
 type checkValidityAndUpdateState = (Header) => Void
 ```
 
-  For Tendermint, it will perform
+  For CometBFT, it will perform
   `ValidandVerified`, that is, it does the trusting period check and the
   +1/3 check (+2/3 for sequential headers).
   If it verifies a header, it adds it to its lightstore,
@@ -273,7 +273,7 @@ validators of some smaller height.
 
 In principle everyone can detect a fork
 
-- ./detection talks about the Tendermint light client with a focus on
+- ./detection talks about the CometBFT light client with a focus on
   light nodes. A relayer runs such light clients and may detect
   forks in this way
 
diff --git a/docs/spec/lightclient/verification/Blockchain_A_1.tla b/docs/spec/lightclient/verification/Blockchain_A_1.tla
index 65de6aa4..1832893d 100644
--- a/docs/spec/lightclient/verification/Blockchain_A_1.tla
+++ b/docs/spec/lightclient/verification/Blockchain_A_1.tla
@@ -3,9 +3,9 @@
 
  * This specification is not maintained anymore. The most recent version can be found at:
 
- * https://github.com/tendermint/spec/tree/master/rust-spec/lightclient/verification
+ * https://github.com/cometbft/cometbft/tree/main/spec/light-client/verification
 
-  This is a high-level specification of Tendermint blockchain
+  This is a high-level specification of CometBFT blockchain
   that is designed specifically for the light client.
   Validators have the voting power of one. If you like to model various
   voting powers, introduce multiple copies of the same validator
@@ -106,7 +106,7 @@ IsCorrectPower(pFaultyNodes, pVS) ==
     \* CP + FP = TP is the total voting power, so we write CP > 2.0 / 3 * TP as follows:
     CP > 2 * FP \* Note: when FP = 0, this implies CP > 0.
     
-(* This is what we believe is the assumption about failures in Tendermint *)     
+(* This is what we believe is the assumption about failures in CometBFT *)     
 FaultAssumption(pFaultyNodes, pNow, pBlockchain) ==
     \A h \in Heights:
       pBlockchain[h].time + TRUSTING_PERIOD > pNow =>
@@ -148,7 +148,7 @@ InitToHeight ==
              ] \******
        
 
-(* is the blockchain in the faulty zone where the Tendermint security model does not apply *)
+(* is the blockchain in the faulty zone where the CometBFT security model does not apply *)
 InFaultyZone ==
   ~FaultAssumption(Faulty, now, blockchain)       
 
diff --git a/docs/spec/lightclient/verification/Lightclient_A_1.tla b/docs/spec/lightclient/verification/Lightclient_A_1.tla
index 64d3fc6a..4adb49e8 100644
--- a/docs/spec/lightclient/verification/Lightclient_A_1.tla
+++ b/docs/spec/lightclient/verification/Lightclient_A_1.tla
@@ -2,11 +2,11 @@
 (**
  * This specification is not maintained anymore. The most recent version can be found at:
 
- * https://github.com/tendermint/spec/tree/master/rust-spec/lightclient/verification
+ * https://github.com/cometbft/cometbft/tree/main/spec/light-client/verification
 
  * A state-machine specification of the lite client, following the English spec:
  *
- * https://github.com/informalsystems/tendermint-rs/blob/main/docs/spec/lightclient/verification.md
+ * https://github.com/cometbft/cometbft-rs/blob/main/docs/spec/lightclient/verification.md
  *) 
 
 EXTENDS Integers, FiniteSets
@@ -304,7 +304,7 @@ NeverFinishPositive ==
   Correctness states that all the obtained headers are exactly like in the blockchain.
  
   It is always the case that every verified header in LightStore was generated by
-  an instance of Tendermint consensus.
+  an instance of CometBFT consensus.
   
   [LCV-DIST-SAFE.1::CORRECTNESS-INV.1]
  *)  
@@ -399,7 +399,7 @@ SuccessOnCorrectPrimaryAndChainOfTrust ==
       state = "finishedSuccess"     
 
 \* Lite Client Completeness: If header h was correctly generated by an instance
-\* of Tendermint consensus (and its age is less than the trusting period),
+\* of CometBFT consensus (and its age is less than the trusting period),
 \* then the lite client should eventually set trust(h) to true.
 \*
 \* Note that Completeness assumes that the lite client communicates with a correct full node.
diff --git a/docs/spec/lightclient/verification/verification.md b/docs/spec/lightclient/verification/verification.md
index b1920422..abb75567 100644
--- a/docs/spec/lightclient/verification/verification.md
+++ b/docs/spec/lightclient/verification/verification.md
@@ -3,7 +3,7 @@
 ## Disclaimer
 
 This specification is not maintained. See
-[tendermint/spec](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/)
+[cometbft/spec](https://github.com/cometbft/cometbft/tree/main/spec/light-client/verification/)
 for the most recent version.
 
 ## Abstract
@@ -13,7 +13,7 @@ The light client implements a read operation of a
 communicating with full nodes.  As some full nodes may be faulty, this
 functionality must be implemented in a fault-tolerant way.
 
-In the Tendermint blockchain, the validator set may change with every
+In the CometBFT blockchain, the validator set may change with every
 new block.  The staking and unbonding mechanism induces a [security
 model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the
 [header][TMBC-HEADER-link],
@@ -47,8 +47,8 @@ in computing more efficiently the proof of fork).
 
 # Outline
 
-- [Part I](#part-i---tendermint-blockchain): Introduction of
- relevant terms of the Tendermint
+- [Part I](#part-i---cometbft-blockchain): Introduction of
+ relevant terms of the CometBFT
 blockchain.
 
 - [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction
@@ -107,7 +107,7 @@ In this document we quite extensively use tags in order to be able to
 reference assumptions, invariants, etc. in future communication. In
 these tags we frequently use the following short forms:
 
-- TMBC: Tendermint blockchain
+- TMBC: CometBFT blockchain
 - SEQ: for sequential specifications
 - LCV: Lightclient Verification
 - LIVE: liveness
@@ -118,7 +118,7 @@ these tags we frequently use the following short forms:
 
 
 
-# Part I - Tendermint Blockchain
+# Part I - CometBFT Blockchain
 
 
 ## Header Fields necessary for the Light Client
@@ -153,7 +153,7 @@ A header contains the following fields:
 
 #### **[TMBC-SEQ.1]**:
 
-The Tendermint blockchain is a list *chain* of headers.
+The CometBFT blockchain is a list *chain* of headers.
 
 
 #### **[TMBC-VALIDATOR-PAIR.1]**:
@@ -191,7 +191,7 @@ message contains the following fields
 A commit is a set of `precommit` message.
 
 
-## Tendermint Failure Model
+## CometBFT Failure Model
 
 #### **[TMBC-AUTH-BYZ.1]**:
 
@@ -204,7 +204,7 @@ messages.
 
 #### **[TMBC-TIME-PARAMS.1]**:
 
-A Tendermint blockchain has the following configuration parameters:
+A CometBFT blockchain has the following configuration parameters:
  - *unbondingPeriod*: a time duration.
  - *trustingPeriod*: a time duration smaller than *unbondingPeriod*.
 
@@ -296,7 +296,7 @@ In this document we specify the light client verification component,
 called *Core Verification*.  The *Core Verification* communicates with
 a full node.  As full nodes may be faulty, it cannot trust the
 received information, but the light client has to check whether the
-header it receives coincides with the one generated by Tendermint
+header it receives coincides with the one generated by CometBFT
 consensus.
 
 The two 
@@ -317,7 +317,7 @@ contains a correct node using *tb*.
 
 Given a height *targetHeight* as an input, the *Verifier* eventually
 stores a header *h* of height *targetHeight* locally.  This header *h*
-is generated by the Tendermint [blockchain][block]. In
+is generated by the CometBFT [blockchain][block]. In
 particular, a header that was not generated by the blockchain should
 never be stored.
 
@@ -339,7 +339,7 @@ The *Verifier* never stores a header which is not in the blockchain.
 
 Faulty full nodes may benefit from lying to the light client, by making the
 light client accept a block that deviates (e.g., contains additional
-transactions) from the one generated by Tendermint consensus.
+transactions) from the one generated by CometBFT consensus.
 Users using the light client might be harmed by accepting a forged header.
 
 The [fork detector][fork-detector] of the light client may help the
@@ -368,7 +368,7 @@ procedure calls to ensure that the response of a correct peer arrives
 before the timeout expires.
 
 #### **[LCV-A-TFM.1]**:
-The Tendermint blockchain satisfies the Tendermint failure model [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link].
+The CometBFT blockchain satisfies the CometBFT failure model [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link].
 
 #### **[LCV-A-VAL.1]**:
 The system satisfies [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] and
@@ -411,13 +411,13 @@ record whether it is verified.
 
 #### **[LCV-DIST-INIT.1]**:
 *LightStore* is initialized with a header *trustedHeader* that was correctly
-generated by the Tendermint consensus. We say *trustedHeader* is verified.
+generated by the CometBFT consensus. We say *trustedHeader* is verified.
 
 ### Temporal Properties
 
 #### **[LCV-DIST-SAFE.1]**:
 It is always the case that every verified header in *LightStore* was
-generated by an instance of Tendermint consensus.
+generated by an instance of CometBFT consensus.
 
 #### **[LCV-DIST-LIVE.1]**:
 
@@ -618,7 +618,7 @@ It is always the case that *LightStore.LatestTrusted.Header.Time > now - trustin
 ### Used Remote Functions
 
 We use the functions `commit` and `validators` that are provided
-by the [RPC client for Tendermint][RPC].
+by the [RPC client for CometBFT][RPC].
 
 
 ```go
@@ -995,7 +995,7 @@ If on the blockchain the validator set of the block at height
 # Part V - Supporting the IBC Relayer
 
 The above specification focuses on the most common case, which also
-constitutes the most challenging task: using the Tendermint [security
+constitutes the most challenging task: using the CometBFT [security
 model][TMBC-FM-2THIRDS-link] to verify light blocks without
 downloading all intermediate blocks. To focus on this challenge, above
 we have restricted ourselves to the case where  *targetHeight* is
@@ -1170,7 +1170,7 @@ func Main (primary PeerID, lightStore LightStore, targetHeight Height)
 
 [[block]] Specification of the block data structure.
 
-[[RPC]] RPC client for Tendermint
+[[RPC]] RPC client for CometBFT
 
 [[fork-detector]] The specification of the light client fork detector.
 
@@ -1180,7 +1180,7 @@ func Main (primary PeerID, lightStore LightStore, targetHeight Height)
 
 [[lightclient]] The light client ADR [77d2651 on Dec 27, 2019].
 
-[RPC]: https://docs.tendermint.com/v0.34/rpc/
+[RPC]: https://docs.cometbft.com/v1/rpc/
 
 [block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md
 
@@ -1195,7 +1195,7 @@ func Main (primary PeerID, lightStore LightStore, targetHeight Height)
 [TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1
 
 [lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md
-[fork-detector]: https://github.com/informalsystems/tendermint-rs/blob/main/docs/spec/lightclient/detection.md
+[fork-detector]: https://github.com/cometbft/cometbft-rs/blob/main/docs/spec/lightclient/detection.md
 [fullnode]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md
 
 [ibc-rs]:https://github.com/informalsystems/ibc-rs