diff --git a/modules/src/ics02_client/msgs/create_client.rs b/modules/src/ics02_client/msgs/create_client.rs
index 114e2e30c4..35280124a8 100644
--- a/modules/src/ics02_client/msgs/create_client.rs
+++ b/modules/src/ics02_client/msgs/create_client.rs
@@ -22,9 +22,9 @@ pub const TYPE_URL: &str = "/ibc.core.client.v1.MsgCreateClient";
 /// A type of message that triggers the creation of a new on-chain (IBC) client.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct MsgCreateAnyClient {
-    client_state: AnyClientState,
-    consensus_state: AnyConsensusState,
-    signer: AccountId,
+    pub client_state: AnyClientState,
+    pub consensus_state: AnyConsensusState,
+    pub signer: AccountId,
 }
 
 impl MsgCreateAnyClient {
diff --git a/modules/tests/README.md b/modules/tests/README.md
new file mode 100644
index 0000000000..54e6491585
--- /dev/null
+++ b/modules/tests/README.md
@@ -0,0 +1,63 @@
+## Model-based tests for IBC modules
+
+### The model
+
+This directory contains the model-based tests for the IBC modules. They are "model-based" because they are generated from a `TLA+` model of the IBC modules (see [IBC.tla](support/model_based/IBC.tla)).
+
+To instantiate the model, we define in [IBC.cfg](support/model_based/IBC.cfg) the following model constants:
+    - `ChainIds = {"chain-A", "chain-B"}`, indicating that two chains, `chain-A` and `chain-B`, will be created
+    - `MaxClientsPerChain = 1`, indicating that at most 1 client per chain will be created
+    - `MaxClientHeight = 2`, indicating that clients will reach at most height 2
+
+The [IBC.cfg](support/model_based/IBC.cfg) file also defines two simple invariants:
+```tla
+INVARIANTS
+    TypeOK
+    ModelNeverErrors
+```
+
+Then, we can ask [`Apalache`](https://apalache.informal.systems), a model checker for `TLA+`, to check that these invariants hold:
+```bash
+apalache-mc check --inv=ICS02UpdateOKTestNeg IBC.tla
+```
+
+The above command automatically reads what we have defined in [IBC.cfg](support/model_based/IBC.cfg).
+
+### The tests
+
+Tests are `TLA+` assertions that describe the desired shape of the test (see [IBCTests.tla](support/model_based/IBCTests.tla)). One of the assertions in [IBCTests.tla](support/model_based/IBCTests.tla) is the following:
+
+```tla
+ICS02UpdateOKTest ==
+    /\ actionOutcome = "ICS02UpdateOK"
+```
+
+This very simple assertion describes a test where the [model](support/model_based/IBC.tla) variable `actionOutcome` reaches the value `"ICS02UpdateOK"`, which occurs when a client is successfully updated to a new height (see [ICS02.tla](support/model_based/ICS02.tla)).
+
+To generate a test from the `ICS02UpdateOKTest` assertion, we first define an invariant negating it:
+```tla
+ICS02UpdateOKTestNeg == ~ICS02UpdateOKTest
+```
+
+Then, we ask `Apalache`, to prove it:
+
+```bash
+apalache-mc check --inv=ICS02UpdateOKTestNeg IBCTests.tla
+```
+
+(Again, the above command automatically reads what we have defined in [IBCTests.cfg](support/model_based/IBCTests.cfg).)
+
+Because the invariant is wrong, `Apalache` will find a counterexample showing that it is indeed possible that a client is sucessfully updated to a new height. This counterexample is our test.
+
+### Current limitations
+
+The counterexamples currently produced by `Apalache` are not easy to parse and have traditionally required tools like [`jsonatr`](https://github.com/informalsystems/jsonatr). Fortunately, [that will change soon](https://github.com/informalsystems/apalache/issues/530), and `Apalache` will be able to produce counterexamples like those in [support/model_based/tests/](support/model_based/tests/).
+These are currently generated manually, but can be easily mapped to Rust (see [step.rs](step.rs)).
+
+### Running the model-based tests
+
+The model-based tests can be run with the following command:
+ 
+```bash
+cargo test -p ibc --features mocks -- model_based
+```
diff --git a/modules/tests/model_based.rs b/modules/tests/model_based.rs
new file mode 100644
index 0000000000..5f11385afd
--- /dev/null
+++ b/modules/tests/model_based.rs
@@ -0,0 +1,269 @@
+mod modelator;
+mod step;
+
+use ibc::ics02_client::client_def::{AnyClientState, AnyConsensusState, AnyHeader};
+use ibc::ics02_client::client_type::ClientType;
+use ibc::ics02_client::error::Kind as ICS02ErrorKind;
+use ibc::ics02_client::msgs::create_client::MsgCreateAnyClient;
+use ibc::ics02_client::msgs::update_client::MsgUpdateAnyClient;
+use ibc::ics02_client::msgs::ClientMsg;
+use ibc::ics18_relayer::context::ICS18Context;
+use ibc::ics18_relayer::error::{Error as ICS18Error, Kind as ICS18ErrorKind};
+use ibc::ics24_host::identifier::{ChainId, ClientId};
+use ibc::ics26_routing::error::{Error as ICS26Error, Kind as ICS26ErrorKind};
+use ibc::ics26_routing::msgs::ICS26Envelope;
+use ibc::mock::client_state::{MockClientState, MockConsensusState};
+use ibc::mock::context::MockContext;
+use ibc::mock::header::MockHeader;
+use ibc::mock::host::HostType;
+use ibc::Height;
+use std::collections::HashMap;
+use std::error::Error;
+use std::fmt::{Debug, Display};
+use step::{ActionOutcome, ActionType, Chain, Step};
+use tendermint::account::Id as AccountId;
+
+#[derive(Debug)]
+struct IBCTestExecutor {
+    // mapping from chain identifier to its context
+    contexts: HashMap<ChainId, MockContext>,
+}
+
+impl IBCTestExecutor {
+    fn new() -> Self {
+        Self {
+            contexts: Default::default(),
+        }
+    }
+
+    /// Create a `MockContext` for a given `chain_id`.
+    /// Panic if a context for `chain_id` already exists.
+    fn init_chain_context(&mut self, chain_id: String, initial_height: u64) {
+        let chain_id = Self::chain_id(chain_id);
+        let max_history_size = 1;
+        let ctx = MockContext::new(
+            chain_id.clone(),
+            HostType::Mock,
+            max_history_size,
+            Height::new(Self::revision(), initial_height),
+        );
+        assert!(self.contexts.insert(chain_id, ctx).is_none());
+    }
+
+    /// Returns a reference to the `MockContext` of a given `chain_id`.
+    /// Panic if the context for `chain_id` is not found.
+    fn chain_context(&self, chain_id: String) -> &MockContext {
+        self.contexts
+            .get(&Self::chain_id(chain_id))
+            .expect("chain context should have been initialized")
+    }
+
+    /// Returns a mutable reference to the `MockContext` of a given `chain_id`.
+    /// Panic if the context for `chain_id` is not found.
+    fn chain_context_mut(&mut self, chain_id: String) -> &mut MockContext {
+        self.contexts
+            .get_mut(&Self::chain_id(chain_id))
+            .expect("chain context should have been initialized")
+    }
+
+    fn extract_handler_error_kind<K>(ics18_result: Result<(), ICS18Error>) -> K
+    where
+        K: Clone + Debug + Display + Into<anomaly::BoxError> + 'static,
+    {
+        let ics18_error = ics18_result.expect_err("ICS18 error expected");
+        assert!(matches!(
+            ics18_error.kind(),
+            ICS18ErrorKind::TransactionFailed
+        ));
+        let ics26_error = ics18_error
+            .source()
+            .expect("expected source in ICS18 error")
+            .downcast_ref::<ICS26Error>()
+            .expect("ICS18 source should be an ICS26 error");
+        assert!(matches!(
+            ics26_error.kind(),
+            ICS26ErrorKind::HandlerRaisedError,
+        ));
+        ics26_error
+            .source()
+            .expect("expected source in ICS26 error")
+            .downcast_ref::<anomaly::Error<K>>()
+            .expect("ICS26 source should be an handler error")
+            .kind()
+            .clone()
+    }
+
+    fn chain_id(chain_id: String) -> ChainId {
+        ChainId::new(chain_id, Self::revision())
+    }
+
+    fn revision() -> u64 {
+        0
+    }
+
+    fn client_id(client_id: u64) -> ClientId {
+        ClientId::new(ClientType::Mock, client_id)
+            .expect("it should be possible to create the client identifier")
+    }
+
+    fn height(height: u64) -> Height {
+        Height::new(Self::revision(), height)
+    }
+
+    fn mock_header(height: u64) -> MockHeader {
+        MockHeader(Self::height(height))
+    }
+
+    fn header(height: u64) -> AnyHeader {
+        AnyHeader::Mock(Self::mock_header(height))
+    }
+
+    fn client_state(height: u64) -> AnyClientState {
+        AnyClientState::Mock(MockClientState(Self::mock_header(height)))
+    }
+
+    fn consensus_state(height: u64) -> AnyConsensusState {
+        AnyConsensusState::Mock(MockConsensusState(Self::mock_header(height)))
+    }
+
+    fn signer() -> AccountId {
+        AccountId::new([0; 20])
+    }
+
+    /// Check that chain heights match the ones in the model.
+    fn check_chain_heights(&self, chains: HashMap<String, Chain>) -> bool {
+        chains.into_iter().all(|(chain_id, chain)| {
+            let ctx = self.chain_context(chain_id);
+            ctx.query_latest_height() == Self::height(chain.height)
+        })
+    }
+}
+
+impl modelator::TestExecutor<Step> for IBCTestExecutor {
+    fn initial_step(&mut self, step: Step) -> bool {
+        assert_eq!(
+            step.action.action_type,
+            ActionType::None,
+            "unexpected action type"
+        );
+        assert_eq!(
+            step.action_outcome,
+            ActionOutcome::None,
+            "unexpected action outcome"
+        );
+        // initiliaze all chains
+        for (chain_id, chain) in step.chains {
+            self.init_chain_context(chain_id, chain.height);
+        }
+        true
+    }
+
+    fn next_step(&mut self, step: Step) -> bool {
+        let outcome_matches = match step.action.action_type {
+            ActionType::None => panic!("unexpected action type"),
+            ActionType::ICS02CreateClient => {
+                // get action parameters
+                let chain_id = step
+                    .action
+                    .chain_id
+                    .expect("create client action should have a chain identifier");
+                let client_height = step
+                    .action
+                    .client_height
+                    .expect("create client action should have a client height");
+
+                // get chain's context
+                let ctx = self.chain_context_mut(chain_id);
+
+                // create ICS26 message and deliver it
+                let msg = ICS26Envelope::ICS2Msg(ClientMsg::CreateClient(MsgCreateAnyClient {
+                    client_state: Self::client_state(client_height),
+                    consensus_state: Self::consensus_state(client_height),
+                    signer: Self::signer(),
+                }));
+                let result = ctx.deliver(msg);
+
+                // check the expected outcome: client create always succeeds
+                match step.action_outcome {
+                    ActionOutcome::ICS02CreateOK => {
+                        // the implementaion matches the model if no error occurs
+                        result.is_ok()
+                    }
+                    action => panic!("unexpected action outcome {:?}", action),
+                }
+            }
+            ActionType::ICS02UpdateClient => {
+                // get action parameters
+                let chain_id = step
+                    .action
+                    .chain_id
+                    .expect("update client action should have a chain identifier");
+                let client_id = step
+                    .action
+                    .client_id
+                    .expect("update client action should have a client identifier");
+                let client_height = step
+                    .action
+                    .client_height
+                    .expect("update client action should have a client height");
+
+                // get chain's context
+                let ctx = self.chain_context_mut(chain_id);
+
+                // create ICS26 message and deliver it
+                let msg = ICS26Envelope::ICS2Msg(ClientMsg::UpdateClient(MsgUpdateAnyClient {
+                    client_id: Self::client_id(client_id),
+                    header: Self::header(client_height),
+                    signer: Self::signer(),
+                }));
+                let result = ctx.deliver(msg);
+
+                // check the expected outcome
+                match step.action_outcome {
+                    ActionOutcome::ICS02UpdateOK => {
+                        // the implementaion matches the model if no error occurs
+                        result.is_ok()
+                    }
+                    ActionOutcome::ICS02ClientNotFound => {
+                        let handler_error_kind =
+                            Self::extract_handler_error_kind::<ICS02ErrorKind>(result);
+                        // the implementaion matches the model if there's an
+                        // error matching the expected outcome
+                        matches!(
+                            handler_error_kind,
+                            ICS02ErrorKind::ClientNotFound(error_client_id)
+                            if error_client_id == Self::client_id(client_id)
+                        )
+                    }
+                    ActionOutcome::ICS02HeaderVerificationFailure => {
+                        let handler_error_kind =
+                            Self::extract_handler_error_kind::<ICS02ErrorKind>(result);
+                        // the implementaion matches the model if there's an
+                        // error matching the expected outcome
+                        handler_error_kind == ICS02ErrorKind::HeaderVerificationFailure
+                    }
+                    action => panic!("unexpected action outcome {:?}", action),
+                }
+            }
+        };
+        // also check that chain heights match
+        outcome_matches && self.check_chain_heights(step.chains)
+    }
+}
+
+const TESTS_DIR: &str = "tests/support/model_based/tests";
+
+#[test]
+fn model_based() {
+    let tests = vec!["ICS02UpdateOKTest", "ICS02HeaderVerificationFailureTest"];
+
+    for test in tests {
+        let test = format!("{}/{}.json", TESTS_DIR, test);
+        let executor = IBCTestExecutor::new();
+        // we should be able to just return the `Result` once the following issue
+        // is fixed: https://github.com/rust-lang/rust/issues/43301
+        if let Err(e) = modelator::test(&test, executor) {
+            panic!("{:?}", e);
+        }
+    }
+}
diff --git a/modules/tests/modelator.rs b/modules/tests/modelator.rs
new file mode 100644
index 0000000000..cbd15b18e3
--- /dev/null
+++ b/modules/tests/modelator.rs
@@ -0,0 +1,69 @@
+use serde::de::DeserializeOwned;
+use std::fmt::Debug;
+use std::fs::File;
+use std::io::BufReader;
+use thiserror::Error;
+
+#[derive(Error, Debug)]
+pub enum ModelatorError<Executor: Debug, Step: Debug> {
+    #[error("test '{path}' not found: {error}")]
+    TestNotFound { path: String, error: String },
+    #[error("test '{path}' could not be deserialized: {error}")]
+    InvalidTest { path: String, error: String },
+    #[error("test '{path}' failed on step {step_index}/{step_count}:\nstep:\n{step:#?}\nexecutor:\n{executor:#?}")]
+    FailedTest {
+        path: String,
+        step_index: usize,
+        step_count: usize,
+        step: Step,
+        executor: Executor,
+    },
+}
+pub trait TestExecutor<S> {
+    fn initial_step(&mut self, step: S) -> bool;
+    fn next_step(&mut self, step: S) -> bool;
+}
+
+pub fn test<Executor, State>(
+    path: &str,
+    mut executor: Executor,
+) -> Result<(), ModelatorError<Executor, State>>
+where
+    Executor: TestExecutor<State> + Debug,
+    State: DeserializeOwned + Debug + Clone,
+{
+    // open test file
+    let file = File::open(path).map_err(|error| ModelatorError::TestNotFound {
+        path: path.to_string(),
+        error: error.to_string(),
+    })?;
+    let reader = BufReader::new(file);
+
+    // parse test file
+    let steps: Vec<State> =
+        serde_json::de::from_reader(reader).map_err(|error| ModelatorError::InvalidTest {
+            path: path.to_string(),
+            error: error.to_string(),
+        })?;
+    let step_count = steps.len();
+
+    for (i, step) in steps.into_iter().enumerate() {
+        // check the step
+        let ok = if i == 0 {
+            executor.initial_step(step.clone())
+        } else {
+            executor.next_step(step.clone())
+        };
+
+        if !ok {
+            return Err(ModelatorError::FailedTest {
+                path: path.to_string(),
+                step_index: i + 1,
+                step_count,
+                step,
+                executor,
+            });
+        }
+    }
+    Ok(())
+}
diff --git a/modules/tests/step.rs b/modules/tests/step.rs
new file mode 100644
index 0000000000..98c831e050
--- /dev/null
+++ b/modules/tests/step.rs
@@ -0,0 +1,49 @@
+use serde::Deserialize;
+use std::collections::HashMap;
+use std::fmt::Debug;
+
+#[derive(Debug, Clone, Deserialize)]
+pub struct Step {
+    pub action: Action,
+
+    #[serde(alias = "actionOutcome")]
+    pub action_outcome: ActionOutcome,
+
+    pub chains: HashMap<String, Chain>,
+}
+
+#[derive(Debug, Clone, Deserialize)]
+pub struct Action {
+    #[serde(alias = "type")]
+    pub action_type: ActionType,
+
+    #[serde(alias = "chainId")]
+    pub chain_id: Option<String>,
+
+    #[serde(alias = "clientId")]
+    pub client_id: Option<u64>,
+
+    #[serde(alias = "clientHeight")]
+    pub client_height: Option<u64>,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub enum ActionType {
+    None,
+    ICS02CreateClient,
+    ICS02UpdateClient,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub enum ActionOutcome {
+    None,
+    ICS02CreateOK,
+    ICS02UpdateOK,
+    ICS02ClientNotFound,
+    ICS02HeaderVerificationFailure,
+}
+
+#[derive(Debug, Clone, PartialEq, Deserialize)]
+pub struct Chain {
+    pub height: u64,
+}
diff --git a/modules/tests/support/model_based/.gitignore b/modules/tests/support/model_based/.gitignore
new file mode 100644
index 0000000000..a8ddd534bf
--- /dev/null
+++ b/modules/tests/support/model_based/.gitignore
@@ -0,0 +1,9 @@
+*.out
+states/
+x/
+detailed.log
+bfs.csv
+log0.smt
+profile-rules.txt
+counterexample.json
+counterexample.tla
diff --git a/modules/tests/support/model_based/IBC.cfg b/modules/tests/support/model_based/IBC.cfg
new file mode 100644
index 0000000000..73976184c4
--- /dev/null
+++ b/modules/tests/support/model_based/IBC.cfg
@@ -0,0 +1,11 @@
+CONSTANTS
+    ChainIds = {"chainA-0", "chainB-0"}
+    MaxClientsPerChain = 1
+    MaxClientHeight = 2
+
+INIT Init
+NEXT Next
+
+INVARIANTS
+    TypeOK
+    ModelNeverErrors
diff --git a/modules/tests/support/model_based/IBC.tla b/modules/tests/support/model_based/IBC.tla
new file mode 100644
index 0000000000..7586626558
--- /dev/null
+++ b/modules/tests/support/model_based/IBC.tla
@@ -0,0 +1,188 @@
+--------------------------------- MODULE IBC ----------------------------------
+
+EXTENDS Integers, FiniteSets, ICS02
+
+\* ids of existing chains
+CONSTANT ChainIds
+\* max number of client to be created per chain
+CONSTANT MaxClientsPerChain
+ASSUME MaxClientsPerChain >= 0
+\* max height which clients can reach
+CONSTANT MaxClientHeight
+ASSUME MaxClientHeight >= 0
+
+\* mapping from chain id to its data
+VARIABLE chains
+\* last action performed
+VARIABLE action
+\* string with the outcome of the last operation
+VARIABLE actionOutcome
+vars == <<chains, action, actionOutcome>>
+
+(********************** TYPE ANNOTATIONS FOR APALACHE ************************)
+\* operator for type annotations
+a <: b == a
+
+ActionType == [
+    type |-> STRING,
+    chainId |-> STRING,
+    clientHeight |-> Int,
+    clientId |-> Int
+]
+AsAction(a) == a <: ActionType
+(******************* END OF TYPE ANNOTATIONS FOR APALACHE ********************)
+
+\* set of possible chain heights
+ChainHeights == Int
+\* set of possible client identifiers
+ClientIds == 0..(MaxClientsPerChain - 1)
+\* set of possible client heights
+ClientHeights == 1..MaxClientHeight
+
+\* data kept per cliennt
+Client == [
+    height: ClientHeights \union {HeightNone}
+]
+\* mapping from client identifier to its height
+Clients == [
+    ClientIds -> Client
+]
+\* data kept per chain
+Chain == [
+    height: ChainHeights,
+    clients: Clients,
+    clientIdCounter: 0..MaxClientsPerChain
+]
+\* mapping from chain identifier to its data
+Chains == [
+    ChainIds -> Chain
+]
+
+\* set of possible actions
+NoneActions == [
+    type: {"None"}
+] <: {ActionType}
+CreateClientActions == [
+    type: {"ICS02CreateClient"},
+    chainId: ChainIds,
+    clientHeight: ClientHeights
+] <: {ActionType}
+UpdateClientActions == [
+    type: {"ICS02UpdateClient"},
+    chainId: ChainIds,
+    clientHeight: ClientHeights,
+    clientId: ClientIds
+] <: {ActionType}
+Actions ==
+    NoneActions \union
+    CreateClientActions \union
+    UpdateClientActions
+
+\* set of possible action outcomes
+ActionOutcomes == {
+    "None",
+    "ModelError",
+    \* ICS02_CreateClient outcomes:
+    "ICS02CreateOK",
+    \* ICS02_UpdateClient outcomes:
+    "ICS02UpdateOK",
+    "ICS02ClientNotFound",
+    "ICS02HeaderVerificationFailure"
+}
+
+(***************************** Specification *********************************)
+
+\* update chain height if outcome was ok
+UpdateChainHeight(height, outcome, okOutcome) ==
+    IF outcome = okOutcome THEN height + 1 ELSE height
+
+CreateClient(chainId, clientHeight) ==
+    LET chain == chains[chainId] IN
+    LET clients == chain.clients IN
+    LET clientIdCounter == chain.clientIdCounter IN
+    LET result == ICS02_CreateClient(clients, clientIdCounter, clientHeight) IN
+    \* update the chain
+    LET updatedChain == [chain EXCEPT
+        !.height = UpdateChainHeight(@, result.outcome, "ICS02CreateOK"),
+        !.clients = result.clients,
+        !.clientIdCounter = result.clientIdCounter
+    ] IN
+    \* update `chains`, set the `action` and its `actionOutcome`
+    /\ chains' = [chains EXCEPT ![chainId] = updatedChain]
+    /\ action' = AsAction([
+        type |-> "ICS02CreateClient",
+        chainId |-> chainId,
+        clientHeight |-> clientHeight])
+    /\ actionOutcome' = result.outcome
+
+UpdateClient(chainId, clientId, clientHeight) ==
+    LET chain == chains[chainId] IN
+    LET clients == chain.clients IN
+    LET result == ICS02_UpdateClient(clients, clientId, clientHeight) IN
+    \* update the chain
+    LET updatedChain == [chain EXCEPT
+        !.height = UpdateChainHeight(@, result.outcome, "ICS03CreateOK"),
+        !.clients = result.clients
+    ] IN
+    \* update `chains`, set the `action` and its `actionOutcome`
+    /\ chains' = [chains EXCEPT ![chainId] = updatedChain]
+    /\ action' = AsAction([
+        type |-> "ICS02UpdateClient",
+        chainId |-> chainId,
+        clientId |-> clientId,
+        clientHeight |-> clientHeight])
+    /\ actionOutcome' = result.outcome
+
+CreateClientAction ==
+    \* select a chain id
+    \E chainId \in ChainIds:
+    \* select a height for the client to be created at
+    \E clientHeight \in ClientHeights:
+        \* only create client if the model constant `MaxClientsPerChain` allows
+        \* it
+        IF chains[chainId].clientIdCounter \in ClientIds THEN
+            CreateClient(chainId, clientHeight)
+        ELSE
+            UNCHANGED vars
+
+UpdateClientAction ==
+    \* select a chain id
+    \E chainId \in ChainIds:
+    \* select a client to be updated (which may not exist)
+    \E clientId \in ClientIds:
+    \* select a height for the client to be updated
+    \E clientHeight \in ClientHeights:
+        UpdateClient(chainId, clientId, clientHeight)
+
+Init ==
+    \* create a client with none values
+    LET clientNone == [
+        height |-> HeightNone
+    ] IN
+    \* create an empty chain
+    LET emptyChain == [
+        height |-> 0,
+        clients |-> [clientId \in ClientIds |-> clientNone],
+        clientIdCounter |-> 0
+    ] IN
+    /\ chains = [chainId \in ChainIds |-> emptyChain]
+    /\ action = AsAction([type |-> "None"])
+    /\ actionOutcome = "None"
+
+Next ==
+    \/ CreateClientAction
+    \/ UpdateClientAction
+    \/ UNCHANGED vars
+
+(******************************** Invariants *********************************)
+
+TypeOK ==
+    /\ chains \in Chains
+    /\ action \in Actions
+    /\ actionOutcome \in ActionOutcomes
+
+\* the model never erros
+ModelNeverErrors ==
+    actionOutcome /= "ModelError"
+
+===============================================================================
diff --git a/modules/tests/support/model_based/IBCDefinitions.tla b/modules/tests/support/model_based/IBCDefinitions.tla
new file mode 100644
index 0000000000..0d5e8e2385
--- /dev/null
+++ b/modules/tests/support/model_based/IBCDefinitions.tla
@@ -0,0 +1,12 @@
+--------------------------- MODULE IBCDefinitions -----------------------------
+
+EXTENDS Integers, FiniteSets
+
+\* if a client identifier is not set then it is -1
+ClientIdNone == -1
+\* if a client identifier is not set then it is -1
+HeightNone == -1
+\* if a connection identifier is not set then it is -1
+ConnectionIdNone == -1
+
+===============================================================================
diff --git a/modules/tests/support/model_based/IBCTests.cfg b/modules/tests/support/model_based/IBCTests.cfg
new file mode 100644
index 0000000000..e4c28bc288
--- /dev/null
+++ b/modules/tests/support/model_based/IBCTests.cfg
@@ -0,0 +1,7 @@
+CONSTANTS
+    ChainIds = {"chainA-0", "chainB-0"}
+    MaxClientsPerChain = 1
+    MaxClientHeight = 2
+
+INIT Init
+NEXT Next
diff --git a/modules/tests/support/model_based/IBCTests.tla b/modules/tests/support/model_based/IBCTests.tla
new file mode 100644
index 0000000000..245461c3c9
--- /dev/null
+++ b/modules/tests/support/model_based/IBCTests.tla
@@ -0,0 +1,22 @@
+------------------------------ MODULE IBCTests --------------------------------
+
+EXTENDS IBC
+
+ICS02CreateOKTest ==
+    /\ actionOutcome = "ICS02CreateOK"
+
+ICS02UpdateOKTest ==
+    /\ actionOutcome = "ICS02UpdateOK"
+
+ICS02ClientNotFoundTest ==
+    /\ actionOutcome = "ICS02ClientNotFound"
+
+ICS02HeaderVerificationFailureTest ==
+    /\ actionOutcome = "ICS02HeaderVerificationFailure"
+
+ICS02CreateOKTestNeg == ~ICS02CreateOKTest
+ICS02UpdateOKTestNeg == ~ICS02UpdateOKTest
+ICS02ClientNotFoundTestNeg == ~ICS02ClientNotFoundTest
+ICS02HeaderVerificationFailureTestNeg == ~ICS02HeaderVerificationFailureTest
+
+===============================================================================
diff --git a/modules/tests/support/model_based/ICS02.tla b/modules/tests/support/model_based/ICS02.tla
new file mode 100644
index 0000000000..84fa0c4727
--- /dev/null
+++ b/modules/tests/support/model_based/ICS02.tla
@@ -0,0 +1,71 @@
+------------------------------- MODULE ICS02 ----------------------------------
+
+EXTENDS Integers, FiniteSets, IBCDefinitions
+
+\* retrieves `clientId`'s data
+ICS02_GetClient(clients, clientId) ==
+    clients[clientId]
+
+\* check if `clientId` exists
+ICS02_ClientExists(clients, clientId) ==
+    ICS02_GetClient(clients, clientId).height /= HeightNone
+
+\* update `clientId`'s data
+ICS02_SetClient(clients, clientId, client) ==
+    [clients EXCEPT ![clientId] = client]
+
+ICS02_CreateClient(clients, clientIdCounter, clientHeight) ==
+    \* check if the client exists (it shouldn't)
+    IF ICS02_ClientExists(clients, clientIdCounter) THEN
+        \* if the client to be created already exists,
+        \* then there's an error in the model
+        [
+            clients |-> clients,
+            clientIdCounter |-> clientIdCounter,
+            outcome |-> "ModelError"
+        ]
+    ELSE
+        \* if it doesn't, create it
+        LET client == [
+            height |-> clientHeight
+        ] IN
+        \* return result with updated state
+        [
+            clients |-> ICS02_SetClient(clients, clientIdCounter, client),
+            clientIdCounter |-> clientIdCounter + 1,
+            outcome |-> "ICS02CreateOK"
+        ]
+
+ICS02_UpdateClient(clients, clientId, clientHeight) ==
+    \* check if the client exists
+    IF ICS02_ClientExists(clients, clientId) THEN
+        \* if the client exists, check its height
+        LET client == ICS02_GetClient(clients, clientId) IN
+        IF client.height < clientHeight THEN
+            \* if the client's height is lower than the one being updated to
+            \* then, update the client
+            LET updatedClient == [client EXCEPT
+                !.height = clientHeight
+            ] IN
+            \* return result with updated state
+            [
+                clients |-> ICS02_SetClient(clients, clientId, updatedClient),
+                outcome |-> "ICS02UpdateOK"
+            ]
+        ELSE
+            \* if the client's height is at least as high as the one being
+            \* updated to, then set an error outcome
+            [
+                clients |-> clients,
+                outcome |-> "ICS02HeaderVerificationFailure"
+            ]
+    ELSE
+        \* if the client does not exist, then set an error outcome
+        [
+            clients |-> clients,
+            outcome |-> "ICS02ClientNotFound"
+        ]
+        \* TODO: distinguish between client state and consensus state to also be
+        \*       able to return a `ConsensusStateNotFound` error outcome
+
+===============================================================================
diff --git a/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json b/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json
new file mode 100644
index 0000000000..32a85c138a
--- /dev/null
+++ b/modules/tests/support/model_based/tests/ICS02HeaderVerificationFailureTest.json
@@ -0,0 +1,49 @@
+[
+    {
+        "action": {
+            "type": "None"
+        },
+        "actionOutcome": "None",
+        "chains": {
+            "chainA-0": {
+                "height": 0
+            },
+            "chainB-0": {
+                "height": 0
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainB-0",
+            "clientHeight": 1,
+            "type": "ICS02CreateClient"
+        },
+        "actionOutcome": "ICS02CreateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 0
+            },
+            "chainB-0": {
+                "height": 1
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainB-0",
+            "clientHeight": 1,
+            "clientId": 0,
+            "type": "ICS02UpdateClient"
+        },
+        "actionOutcome": "ICS02HeaderVerificationFailure",
+        "chains": {
+            "chainA-0": {
+                "height": 0
+            },
+            "chainB-0": {
+                "height": 1
+            }
+        }
+    }
+]
diff --git a/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json b/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json
new file mode 100644
index 0000000000..5275bfcda3
--- /dev/null
+++ b/modules/tests/support/model_based/tests/ICS02UpdateOKTest.json
@@ -0,0 +1,115 @@
+[
+    {
+        "action": {
+            "type": "None"
+        },
+        "actionOutcome": "None",
+        "chains": {
+            "chainA-0": {
+                "height": 0
+            },
+            "chainB-0": {
+                "height": 0
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainB-0",
+            "clientHeight": 1,
+            "type": "ICS02CreateClient"
+        },
+        "actionOutcome": "ICS02CreateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 0
+            },
+            "chainB-0": {
+                "height": 1
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainB-0",
+            "clientHeight": 2,
+            "clientId": 0,
+            "type": "ICS02UpdateClient"
+        },
+        "actionOutcome": "ICS02UpdateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 0
+            },
+            "chainB-0": {
+                "height": 2
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainA-0",
+            "clientHeight": 1,
+            "type": "ICS02CreateClient"
+        },
+        "actionOutcome": "ICS02CreateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 1
+            },
+            "chainB-0": {
+                "height": 2
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainA-0",
+            "clientHeight": 2,
+            "clientId": 0,
+            "type": "ICS02UpdateClient"
+        },
+        "actionOutcome": "ICS02UpdateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 2
+            },
+            "chainB-0": {
+                "height": 2
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainA-0",
+            "clientHeight": 1,
+            "type": "ICS02CreateClient"
+        },
+        "actionOutcome": "ICS02CreateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 3
+            },
+            "chainB-0": {
+                "height": 2
+            }
+        }
+    },
+    {
+        "action": {
+            "chainId": "chainA-0",
+            "clientHeight": 2,
+            "clientId": 1,
+            "type": "ICS02UpdateClient"
+        },
+        "actionOutcome": "ICS02UpdateOK",
+        "chains": {
+            "chainA-0": {
+                "height": 4
+            },
+            "chainB-0": {
+                "height": 2
+            }
+        }
+    }
+]