diff --git a/docs/spec/README.md b/docs/spec/README.md
index 4f3e71fec9..6adf6bb24d 100644
--- a/docs/spec/README.md
+++ b/docs/spec/README.md
@@ -1,5 +1,7 @@
 # Specification and verification of IBC protocols 
 
- * [relayer](./relayer) comprises TLA+ specification for the IBC relayer algorithms (ICS 018).
+ * [tla](./tla) comprises TLA+ specification for the IBC specification.
 
- * [connection-handshake](./connection-handshake) contains English and TLA+ specifications for the IBC Connection Handshake Protocol (ICS 003).
+ * [connection-handshake](./connection-handshake) [Deprecated] contains English and TLA+ specifications for the IBC Connection Handshake Protocol (ICS 003).
+
+ * [relayer](./relayer) contains English specification of the relayer. 
diff --git a/docs/spec/fungible-token-transfer/Bank.tla b/docs/spec/tla/fungible-token-transfer/Bank.tla
similarity index 100%
rename from docs/spec/fungible-token-transfer/Bank.tla
rename to docs/spec/tla/fungible-token-transfer/Bank.tla
diff --git a/docs/spec/fungible-token-transfer/Chain.tla b/docs/spec/tla/fungible-token-transfer/Chain.tla
similarity index 100%
rename from docs/spec/fungible-token-transfer/Chain.tla
rename to docs/spec/tla/fungible-token-transfer/Chain.tla
diff --git a/docs/spec/fungible-token-transfer/IBCTokenTransfer.tla b/docs/spec/tla/fungible-token-transfer/IBCTokenTransfer.tla
similarity index 100%
rename from docs/spec/fungible-token-transfer/IBCTokenTransfer.tla
rename to docs/spec/tla/fungible-token-transfer/IBCTokenTransfer.tla
diff --git a/docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla b/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla
similarity index 100%
rename from docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla
rename to docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla
diff --git a/docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla b/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla
similarity index 100%
rename from docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla
rename to docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla
diff --git a/docs/spec/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla b/docs/spec/tla/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla
similarity index 100%
rename from docs/spec/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla
rename to docs/spec/tla/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla
diff --git a/docs/spec/fungible-token-transfer/README.md b/docs/spec/tla/fungible-token-transfer/README.md
similarity index 100%
rename from docs/spec/fungible-token-transfer/README.md
rename to docs/spec/tla/fungible-token-transfer/README.md
diff --git a/docs/spec/relayer/tla/Chain.tla b/docs/spec/tla/ibc-core/Chain.tla
similarity index 100%
rename from docs/spec/relayer/tla/Chain.tla
rename to docs/spec/tla/ibc-core/Chain.tla
diff --git a/docs/spec/relayer/tla/IBCCore.tla b/docs/spec/tla/ibc-core/IBCCore.tla
similarity index 100%
rename from docs/spec/relayer/tla/IBCCore.tla
rename to docs/spec/tla/ibc-core/IBCCore.tla
diff --git a/docs/spec/relayer/tla/IBCCoreDefinitions.tla b/docs/spec/tla/ibc-core/IBCCoreDefinitions.tla
similarity index 100%
rename from docs/spec/relayer/tla/IBCCoreDefinitions.tla
rename to docs/spec/tla/ibc-core/IBCCoreDefinitions.tla
diff --git a/docs/spec/relayer/tla/ICS02ClientHandlers.tla b/docs/spec/tla/ibc-core/ICS02ClientHandlers.tla
similarity index 100%
rename from docs/spec/relayer/tla/ICS02ClientHandlers.tla
rename to docs/spec/tla/ibc-core/ICS02ClientHandlers.tla
diff --git a/docs/spec/relayer/tla/ICS03ConnectionHandlers.tla b/docs/spec/tla/ibc-core/ICS03ConnectionHandlers.tla
similarity index 100%
rename from docs/spec/relayer/tla/ICS03ConnectionHandlers.tla
rename to docs/spec/tla/ibc-core/ICS03ConnectionHandlers.tla
diff --git a/docs/spec/relayer/tla/ICS04ChannelHandlers.tla b/docs/spec/tla/ibc-core/ICS04ChannelHandlers.tla
similarity index 100%
rename from docs/spec/relayer/tla/ICS04ChannelHandlers.tla
rename to docs/spec/tla/ibc-core/ICS04ChannelHandlers.tla
diff --git a/docs/spec/relayer/tla/ICS04PacketHandlers.tla b/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla
similarity index 100%
rename from docs/spec/relayer/tla/ICS04PacketHandlers.tla
rename to docs/spec/tla/ibc-core/ICS04PacketHandlers.tla
diff --git a/docs/spec/relayer/tla/ICS18Environment.cfg b/docs/spec/tla/ibc-core/ICS18Environment.cfg
similarity index 100%
rename from docs/spec/relayer/tla/ICS18Environment.cfg
rename to docs/spec/tla/ibc-core/ICS18Environment.cfg
diff --git a/docs/spec/relayer/tla/ICS18Environment_apalache.tla b/docs/spec/tla/ibc-core/ICS18Environment_apalache.tla
similarity index 100%
rename from docs/spec/relayer/tla/ICS18Environment_apalache.tla
rename to docs/spec/tla/ibc-core/ICS18Environment_apalache.tla
diff --git a/docs/spec/relayer/tla/ICS18Relayer.tla b/docs/spec/tla/ibc-core/ICS18Relayer.tla
similarity index 100%
rename from docs/spec/relayer/tla/ICS18Relayer.tla
rename to docs/spec/tla/ibc-core/ICS18Relayer.tla
diff --git a/docs/spec/relayer/tla/README.md b/docs/spec/tla/ibc-core/README.md
similarity index 100%
rename from docs/spec/relayer/tla/README.md
rename to docs/spec/tla/ibc-core/README.md