diff --git a/examples/ctf-01/.cargo/config b/examples/ctf-01/.cargo/config
new file mode 100644
index 0000000..af5698e
--- /dev/null
+++ b/examples/ctf-01/.cargo/config
@@ -0,0 +1,4 @@
+[alias]
+wasm = "build --release --lib --target wasm32-unknown-unknown"
+unit-test = "test --lib"
+schema = "run --bin schema"
diff --git a/examples/ctf-01/.editorconfig b/examples/ctf-01/.editorconfig
new file mode 100644
index 0000000..3d36f20
--- /dev/null
+++ b/examples/ctf-01/.editorconfig
@@ -0,0 +1,11 @@
+root = true
+
+[*]
+indent_style = space
+indent_size = 2
+charset = utf-8
+trim_trailing_whitespace = true
+insert_final_newline = true
+
+[*.rs]
+indent_size = 4
diff --git a/examples/ctf-01/Cargo.toml b/examples/ctf-01/Cargo.toml
new file mode 100644
index 0000000..534ac9b
--- /dev/null
+++ b/examples/ctf-01/Cargo.toml
@@ -0,0 +1,58 @@
+[package]
+name = "oaksecurity-cosmwasm-ctf-01"
+version = "0.1.0"
+authors = ["Oak Security <info@oaksecurity.io>"]
+edition = "2021"
+
+exclude = [
+  # Those files are rust-optimizer artifacts. You might want to commit them for convenience but they should not be part of the source code publication.
+  "contract.wasm",
+  "hash.txt",
+]
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[lib]
+crate-type = ["cdylib", "rlib"]
+
+[profile.release]
+opt-level = 3
+debug = false
+rpath = false
+lto = true
+debug-assertions = false
+codegen-units = 1
+panic = 'abort'
+incremental = false
+overflow-checks = true
+
+[features]
+# for more explicit tests, cargo test --features=backtraces
+backtraces = ["cosmwasm-std/backtraces"]
+# use library feature to disable all instantiate/execute/query exports
+library = []
+
+[package.metadata.scripts]
+optimize = """docker run --rm -v "$(pwd)":/code \
+  --mount type=volume,source="$(basename "$(pwd)")_cache",target=/code/target \
+  --mount type=volume,source=registry_cache,target=/usr/local/cargo/registry \
+  cosmwasm/rust-optimizer:0.12.10
+"""
+
+[dependencies]
+cosmwasm-schema = "1.1.3"
+cosmwasm-std = "1.1.3"
+cosmwasm-storage = "1.1.3"
+cw-storage-plus = "1.0.1"
+cw-utils = "1.0.1"
+cw2 = "1.0.1"
+schemars = "0.8.10"
+serde = { version = "1.0.145", default-features = false, features = ["derive"] }
+thiserror = { version = "1.0.31" }
+
+[dev-dependencies]
+anyhow = "1.0.83"
+cw-multi-test = "0.16.2"
+itf = "0.2.4"
+num-bigint = "0.4.4"
+num-traits = "0.2.17"
diff --git a/examples/ctf-01/LICENSE b/examples/ctf-01/LICENSE
new file mode 100644
index 0000000..d645695
--- /dev/null
+++ b/examples/ctf-01/LICENSE
@@ -0,0 +1,202 @@
+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/examples/ctf-01/NOTICE b/examples/ctf-01/NOTICE
new file mode 100644
index 0000000..8fcffd7
--- /dev/null
+++ b/examples/ctf-01/NOTICE
@@ -0,0 +1,13 @@
+Copyright 2023 Oak Security <info@oaksecurity.io>
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
diff --git a/examples/ctf-01/README.md b/examples/ctf-01/README.md
new file mode 100644
index 0000000..97243f2
--- /dev/null
+++ b/examples/ctf-01/README.md
@@ -0,0 +1,480 @@
+# Walk-through to capturing the flag on CTF 01
+
+This is a walk-through on how we can find the bug in the CTF 01 contract using
+[Quint](https://github.com/informalsystems/quint) with
+[cosmwasm-to-quint](https://github.com/informalsystems/cosmwasm-to-quint). See
+[quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt](./quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt)
+for the final model and
+[tests/mbt_oaksecurity_cosmwasm_ctf_01.rs](./tests/mbt_oaksecurity_cosmwasm_ctf_01.rs)
+for a generated test example.
+
+## 1. Setup
+
+First of all, we need to set up our tools. We should, if we haven't already,
+install Rust and
+[Quint](https://github.com/informalsystems/quint?tab=readme-ov-file#installation),
+and clone the [cosmwasm-ctf](https://github.com/oak-security/cosmwasm-ctf/) repo
+to access the challenge.
+
+We also need to [install
+cosmwasm-to-quint](https://github.com/informalsystems/cosmwasm-to-quint/?tab=readme-ov-file#setup-and-generation)
+and follow the instructions to configure our project (CTF 01):
+
+```bash
+cd /path/to/cosmwasm-ctf/ctf-01
+
+# Install and use a nightly version
+rustup toolchain add nightly-2024-01-06
+rustup override set nightly-2024-01-06
+# Add components and target
+rustup component add clippy rust-src rustc-dev llvm-tools-preview
+rustup target add wasm32-unknown-unknown
+# Update dependencies on Cargo.lock to match the new tool chain
+cargo update
+```
+
+We should also add all dev dependencies required to run the generated tests, as instructed in cosmwasm-to-quint readme:
+```bash
+cargo add cw-multi-test@0.16.2 --dev
+cargo add itf@0.2.4 --dev
+cargo add anyhow@1.0.83 --dev
+cargo add num-bigint@0.4.4 --dev
+cargo add num-traits@0.2.17 --dev
+```
+
+## 2. Generation
+
+We can now generate the model stubs and tests for the CTF contract by running:
+```bash
+cargo clean && cargo cosmwasm-to-quint
+```
+
+which should print a message like this at the end:
+```
+Sucessfully generated files. Quint files are inside quint/ and test files are inside tests/.
+```
+
+And now we have the generated files in their respective folders:
+```bash
+$ tree quint tests
+quint
+├── lib
+│   ├── bank.qnt
+│   ├── basicSpells.qnt
+│   ├── BoundedUInt.qnt
+│   ├── cw_types.qnt
+│   ├── cw_utils.qnt
+│   └── messaging.qnt
+└── oaksecurity_cosmwasm_ctf_01_stubs.qnt
+tests
+└── mbt_oaksecurity_cosmwasm_ctf_01.rs
+
+3 directories, 8 files
+```
+
+We can now try to run `cargo test`: this should give us an error like:
+```
+couldn't read tests/../quint/test.itf.json: No such file or directory
+```
+
+That makes sense: we need a trace from the model in order to run our model-based
+test.
+
+## 3. Obtaining some trace
+
+To obtain some random trace, we can run quint simulator with a single sample (`--max-samples=1`):
+```
+quint run quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt --mbt --out-itf=quint/test.itf.json --max-samples=1
+```
+
+And then we should be able to run the tests with `cargo test`. However, we get a test failure:
+```
+Action unexpectedly failed [...]
+Caused by:
+    Unauthorized
+```
+
+That's because our model is still made of stubs and doesn't have any of the
+"business logic" of the contract. So the tests that should ensure model and
+implementation match are expected to fail - all good!
+
+## 4. Getting the model and the implementation to match
+
+This is the part that takes the most effort: we need to replace the `// TODO Update body` placeholders with the actual definition for the body. Here's a diff for what we need to add for the CTF-01 contract: the instantiate, deposit and withdraw entrypoint bodies.
+```diff
+30,31c30
+<     // TODO: Update body
+<     (Ok(Response_new), state)
+---
+>     (Ok(Response_new.add_attribute("action", FromStr("instantiate"))), state)
+40,41c39,62
+<     // TODO: Update body
+<     (Ok(Response_new), state)
+---
+>     match must_pay(info, DENOM) {
+>       | Err(s) => (Err(s), state)
+>       | Ok(amount) => {
+>         if(amount < MINIMUM_DEPOSIT_AMOUNT) {
+>           (Err("Unauthorized"), state)
+>         } else {
+>           val id = state.last_id
+>           val release_timestamp = env.block.time + LOCK_PERIOD
+>           val lock = {
+>             id: id,
+>             owner: info.sender,
+>             amount: amount,
+>             release_timestamp: release_timestamp
+>           }
+>           val new_state = { ...state, lockups: { state.lockups.put(id, lock) }, last_id: id + 1 }
+>           (Ok(Response_new.add_attribute("action", FromStr("deposit"))
+>                           .add_attribute("id", FromInt(id))
+>                           .add_attribute("owner", FromStr(lock.owner))
+>                           .add_attribute("amout", FromInt(amount))
+>                           .add_attribute("release_timestamp", FromInt(release_timestamp))
+>              ), new_state)
+>         }
+>       }
+>     }
+53,54c74,98
+<     // TODO: Update body
+<     (Ok(Response_new), state)
+---
+>      val lockups = ids.listMap(id => state.lockups.get(id))
+>
+>     if (lockups.toSet().exists(lockup => lockup.owner != info.sender or env.block.time < lockup.release_timestamp)) {
+>       (Err("Unauthorized"), state)
+>     } else {
+>       val total_amount = lockups.foldl(0, (acc, lockup) => {
+>         acc + lockup.amount
+>       })
+>       val new_state = lockups.foldl(state, (acc, lockup) => {
+>         { ...acc, lockups: acc.lockups.mapRemove(lockup.id) }
+>       })
+>
+>       val msg = BankMsg_Send({
+>         to_address: info.sender,
+>         amount: [{
+>           denom: DENOM,
+>           amount: total_amount,
+>         }]
+>       })
+>
+>       (Ok(Response_new.add_attribute("action", FromStr("withdraw"))
+>                       .add_attribute("ids", FromListInt(ids))
+>                       .add_attribute("total_amount", FromInt(total_amount))
+>                       .add_message(CosmosMsg_Bank(msg))), new_state)
+>     }
+```
+
+Now, we need to run the simulator again to get a new trace for the updated model:
+```bash
+quint run quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt --mbt --out-itf=quint/test.itf.json --max-samples=1
+```
+
+But there's an issue with our model, and we get the following error:
+```bash
+error: [QNT507] quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt:74:38 - error: Called 'get' with a non-existing key
+74:      val lockups = ids.listMap(id => state.lockups.get(id))
+                                         ^^^^^^^^^^^^^^^^^^^^^
+
+error: Runtime error
+```
+
+Seems like we are trying to withdraw non-existent lockups. To fix the error, we
+need to ensure this never happens. So let's change two things:
+1. `withdraw_action` should only be possible if there are any lockups
+2. The value for `message_ids` (the field of the withdraw message) should have elements from the set of existing lockups, and it should be a non-empty list.
+```diff
+101c101,102
+<   action withdraw_action = {
+---
+>   action withdraw_action = all {
+>     contract_state.lockups.keys().size() > 0,
+104,105c105,106
+<     nondet message_ids: List[int] = 0.to(MAX_AMOUNT).allListsUpTo(2).oneOf()
+<     pure val message: ExecuteMsg = ExecuteMsg_Withdraw({ ids: message_ids })
+---
+>     nondet message_ids: List[int] = contract_state.lockups.keys().allListsUpTo(2).filter(l => l.length() > 0).oneOf()
+>     val message: ExecuteMsg = ExecuteMsg_Withdraw({ ids: message_ids })
+```
+
+This might seem a bit complicated for now, but it should become fairly
+straightforward after you learn a bit of Quint.
+
+After this fix, we can successfully generate a new trace
+```bash
+quint run quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt --mbt --out-itf=quint/test.itf.json --max-samples=1
+```
+
+And then we can try running `cargo test` again. But we get another error!
+```bash
+Step number: Some(1)
+Result from trace: Err("Wrong Denom")
+Message: Deposit
+Sender: Addr("sender1")
+Funds: [Coin { 111 "d1" }]
+thread 'tests::model_test' panicked at src/contract.rs:42:41:
+called `Result::unwrap()` on an `Err` value: MissingDenom("uawesome")
+```
+PS: your error might look a bit different since has information about the randomly generated trace.
+
+Well, this is not exactly a problem: both the contract and the model (trace) have complained about the denom. In the funds, we can see that the denom was "d1" while the contract expects "uawesome". The problem is that the contract panics in this scenario, and we can't continue testing. So we need to prevent this panic - by preventing the model to generate traces with incorrect funds:
+```diff
+20c20
+<   pure val DENOMS = Set("d1", "uawesome")
+---
+>   pure val DENOMS = Set("uawesome")
+```
+
+And yet again, we generate a trace:
+```bash
+quint run quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt --mbt --out-itf=quint/test.itf.json --max-samples=1
+```
+
+But now we got it! Running `cargo test` now succeeds. This means our model is
+currently matching our implementation. At least, for a random trace. We can be
+more sure by re-generating the trace a few times and checking that `cargo test`
+succeeds for each of them.
+
+## 5. Obtaining a trace for the challenge's goal
+
+Now we can start trying to solve the challenge. The goal for CTF 01 is: >
+Demonstrate how an unprivileged user can drain all funds inside the contract.
+
+Let's write an invariant for that. We can actually simplify this a bit by defining that the contract should not be drained, that is, its balance should never be less than what it was at the start.
+```bluespec
+val contract_balance_ok = bank.get(CONTRACT_ADDRESS).get(DENOM) >= 200 // initial balance
+```
+
+This invariant is written in Quint, and we need to add it to our Quint file. We
+usually define the invariants at the very end of the module.
+
+Let's try to find a counterexample for this invariant:
+```bash
+quint run quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt --mbt --out-itf=quint/test.itf.json --invariant=contract_balance_ok
+```
+
+That doesn't really work. We should see an "Invariant violated" message on
+STDOUT, but we don't see that. This means the invariant was not violated, so we
+couldn't find the scenario we wanted. Let's run it again without the `--out-itf`
+argument, so we can examine the pretty output.
+
+```
+$ quint run quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt --mbt --invariant=contract_balance_ok
+An example execution:
+
+[State 0]
+{
+  action_taken: "q::init",
+  bank:
+    Map(
+      "contract0" -> Map("uawesome" -> 200),
+      "sender1" -> Map("uawesome" -> 200),
+      "sender2" -> Map("uawesome" -> 200),
+      "sender3" -> Map("uawesome" -> 200)
+    ),
+  contract_state: { last_id: 0, lockups: Map() },
+  nondet_picks: { amount: Some(0), denom: Some("uawesome"), message_ids: None, sender: Some("admin") },
+  result:
+    Ok({
+      attributes: [{ key: "action", value: FromStr("instantiate") }],
+      data: None,
+      events: [],
+      messages: []
+    }),
+  time: 0
+}
+
+[State 1]
+{
+  action_taken: "deposit_action",
+  bank:
+    Map(
+      "contract0" -> Map("uawesome" -> 200),
+      "sender1" -> Map("uawesome" -> 200),
+      "sender2" -> Map("uawesome" -> 200),
+      "sender3" -> Map("uawesome" -> 200)
+    ),
+  contract_state: { last_id: 0, lockups: Map() },
+  nondet_picks: { amount: Some(193), denom: Some("uawesome"), message_ids: None, sender: Some("sender1") },
+  result: Err("Unauthorized"),
+  time: 1
+}
+
+[State 2]
+{
+  action_taken: "deposit_action",
+  bank:
+    Map(
+      "contract0" -> Map("uawesome" -> 200),
+      "sender1" -> Map("uawesome" -> 200),
+      "sender2" -> Map("uawesome" -> 200),
+      "sender3" -> Map("uawesome" -> 200)
+    ),
+  contract_state: { last_id: 0, lockups: Map() },
+  nondet_picks: { amount: Some(134), denom: Some("uawesome"), message_ids: None, sender: Some("sender3") },
+  result: Err("Unauthorized"),
+  time: 2
+}
+
+[...]
+```
+
+The actual trace has 20 states, but is more of the same: by examining the trace
+a bit, we can see that `action_taken` is always `deposit_action`, and the
+`result` is always `Unauthorized` or some other error. We must be doing
+something wrong in the validation of the deposit action, let's take a look at
+the part of the model responsible for this `Unauthorized` response:
+
+```bluespec
+if (amount < MINIMUM_DEPOSIT_AMOUNT) {
+  (Err("Unauthorized"), state)
+} else {
+  // ...
+}
+```
+
+From this, we can figure out that there might be something wrong with the amounts. And there is. While the `MINIMUM_DEPOSIT_AMOUNT` of the contract is `10_000`, the model's `MAX_AMOUNT`, used to generate integer inputs, is `200`. That is, there will never be a deposit action with a sufficient amount to go to the `else` branch. In order to fix that, we can either reduce the `MINIMUM_DEPOSIT_AMOUNT` or increase the `MAX_AMOUNT`. Let's do the former:
+On the model:
+```diff
+110c110
+<   pure val MINIMUM_DEPOSIT_AMOUNT = 10000
+---
+>   pure val MINIMUM_DEPOSIT_AMOUNT = 100
+```
+
+On the contract:
+```diff
+diff --git a/ctf-01/src/contract.rs b/ctf-01/src/contract.rs
+index ad9b617..4532e24 100644
+--- a/ctf-01/src/contract.rs
++++ b/ctf-01/src/contract.rs
+@@ -10,7 +10,7 @@ use crate::state::{Lockup, LAST_ID, LOCKUPS};
+ use cw_utils::must_pay;
+
+ pub const DENOM: &str = "uawesome";
+-pub const MINIMUM_DEPOSIT_AMOUNT: Uint128 = Uint128::new(10_000);
++pub const MINIMUM_DEPOSIT_AMOUNT: Uint128 = Uint128::new(100);
+ pub const LOCK_PERIOD: u64 = 60 * 60 * 24;
+
+ #[cfg_attr(not(feature = "library"), entry_point)]
+```
+
+Again, no invariant violation. Let's repeat the process (run without `--out-itf`) and inspect the trace. We can see that all of our `withdraw` actions look like this:
+```
+[State 19]
+{
+  action_taken: "withdraw_action",
+  bank:
+    Map(
+      "contract0" -> Map("uawesome" -> 543),
+      "sender1" -> Map("uawesome" -> 14),
+      "sender2" -> Map("uawesome" -> 200),
+      "sender3" -> Map("uawesome" -> 43)
+    ),
+  contract_state:
+    {
+      last_id: 4,
+      lockups:
+        Map(
+          0 -> { amount: 186, id: 0, owner: "sender1", release_timestamp: 86403 },
+          1 -> { amount: 101, id: 1, owner: "contract0", release_timestamp: 86408 },
+          2 -> { amount: 157, id: 2, owner: "sender3", release_timestamp: 86413 },
+          3 -> { amount: 172, id: 3, owner: "contract0", release_timestamp: 86417 }
+        )
+    },
+  nondet_picks:
+    { amount: Some(169), denom: Some("uawesome"), message_ids: Some([3, 1]), sender: Some("contract0") },
+  result: Err("Unauthorized"),
+  time: 19
+}
+```
+
+Again, let's try to figure out why we are getting so much `Unauthorized`.
+```bluespec
+if (lockups.toSet().exists(lockup => lockup.owner != info.sender or env.block.time < lockup.release_timestamp)) {
+  (Err("Unauthorized"), state)
+} else {
+  // ...
+}
+```
+
+We can investigate for a bit, but we'll find that we are not properly handling timestamps. On the trace, the time is `19`, while our `LOCK_PERIOD` for lockups is `60 * 60 * 24`. By default, the generated model and test tick in intervals of 1 second, so it would take a really long trace to get a lockup to be release. Let's change that by increasing our `TICK` to `LOCK_PERIOD`:
+On the model:
+```diff
+180c180
+<   action advance_time = time' = time + 1
+---
+>   action advance_time = time' = time + LOCK_PERIOD
+```
+
+On the test file:
+```diff
+88c88
+<     pub const TICK: u64 = 1;
+---
+>     pub const TICK: u64 = contract::LOCK_PERIOD;
+```
+
+Now let's try again, and we finally got a violated invariant. We can also run without `--out-itf` to see the trace that achieves the goal:
+```bash
+[State 14]
+{
+  action_taken: "withdraw_action",
+  bank:
+    Map(
+      "contract0" -> Map("uawesome" -> 170),
+      "sender1" -> Map("uawesome" -> 200),
+      "sender2" -> Map("uawesome" -> 230),
+      "sender3" -> Map("uawesome" -> 200)
+    ),
+  contract_state: { last_id: 2, lockups: Map() },
+  nondet_picks:
+    { amount: Some(78), denom: Some("uawesome"), message_ids: Some([0, 0]), sender: Some("sender2") },
+  result:
+    Ok({
+      attributes:
+        [
+          { key: "action", value: FromStr("withdraw") },
+          { key: "ids", value: FromListInt([0, 0]) },
+          { key: "total_amount", value: FromInt(216) }
+        ],
+      data: None,
+      events: [],
+      messages: []
+    }),
+  time: 1209600
+}
+```
+
+Looks like the contract got drained after an withdraw of ids `[0, 0]`.
+
+Now let's replay this trace in the implementation by running `cargo test`. Unexpectedly, we get an error:
+```
+Step number: Some(2)
+Result from trace: Err("Unauthorized")
+Message: Withdraw { ids: [0] }
+Sender: Addr("sender1")
+Funds: [Coin { 15 "uawesome" }]
+thread 'tests::model_test' panicked at src/contract.rs:83:60:
+called `Result::unwrap()` on an `Err` value: NotFound
+```
+
+Seems like the implementation broke when we tried to withdraw id 0. Somehow, the model and the implementation are not matching. This might actually be due to a minor issue in the CTF contract: although the instantiate message includes a `count` field, this is never used. So even we are configuring both the model and the implementation with an initial count of 0, the implementation has a hard-coded 1. Let's update our model to match this:
+```diff
+119c119
+<     last_id: 0,
+---
+>     last_id: 1,
+```
+
+We can now generate a violation trace one more time and run `cargo test` to see the test finally succeeds! This means we were able to reproduce steps leading to the challenge's goal in the actual implementation. If we want to be sure, we can run `cargo test -- --nocapture` to see the printed information. On the last state, we'll see something like this:
+```bash
+Contract balance (Addr("contract0")) for uawesome: Uint128(114) vs Uint128(114)
+```
+Which means that our contract has `114` uawesome tokens, which is less than it's start amount of `200`.
+
+Although this doesn't really work at the first attempt, it's usually
+straightforward to find the issues and fix them, and we learn a lot about
+details and ambiguities while doing it.
+
diff --git a/examples/ctf-01/challenge-README.md b/examples/ctf-01/challenge-README.md
new file mode 100644
index 0000000..2059c79
--- /dev/null
+++ b/examples/ctf-01/challenge-README.md
@@ -0,0 +1,40 @@
+# Awesomwasm 2023 CTF
+
+## Challenge 01: *Mjolnir*
+
+Smart contract that allows user deposit for a locked period before unlocking them.
+
+### Execute entry points:
+```rust
+pub enum ExecuteMsg {
+    Deposit {},
+    Withdraw { ids: Vec<u64> },
+}
+```
+
+Please check the challenge's [integration_tests](./src/integration_test.rs) for expected usage examples. You can use these tests as a base to create your exploit Proof of Concept.
+
+**:house: Base scenario:**
+- The contract contains initial funds.
+- `USER` deposits funds into the contract.
+
+**:star: Goal for the challenge:**
+- Demonstrate how an unprivileged user can drain all funds inside the contract.
+
+## Scoring
+
+This challenge has been assigned a total of **90** points: 
+- **20** points will be awarded for a proper description of the finding that allows you to achieve the **Goal** above.
+- **25** points will be awarded for a proper recommendation that fixes the issue.
+- If the report is deemed valid, the remaining **45** additional points will be awarded for a working Proof of Concept exploit of the vulnerability.
+
+
+:exclamation: The usage of [`cw-multi-test`](https://github.com/CosmWasm/cw-multi-test) is **mandatory** for the PoC, please take the approach of the provided integration tests as a suggestion.
+
+:exclamation: Remember that insider threats and centralization concerns are out of the scope of the CTF.
+
+## Any questions?
+
+If you are unsure about the contract's logic or expected behavior, drop your question on the [official Telegram channel](https://t.me/+8ilY7qeG4stlYzJi) and one of our team members will reply to you as soon as possible. 
+
+Please remember that only questions about the functionality from the point of view of a standard user will be answered. Potential solutions, vulnerabilities, threat analysis or any other "attacker-minded" questions should never be discussed publicly in the channel and will not be answered.
diff --git a/examples/ctf-01/quint/lib/BoundedUInt.qnt b/examples/ctf-01/quint/lib/BoundedUInt.qnt
new file mode 100644
index 0000000..e4060b0
--- /dev/null
+++ b/examples/ctf-01/quint/lib/BoundedUInt.qnt
@@ -0,0 +1,470 @@
+// -*- mode: Bluespec; -*-
+
+module BoundedUInt {
+  /// The size of this integer type in bits.
+  const BITS: int
+
+  /// The smallest value that can be represented by this integer type.
+  pure val MIN = 0
+
+  /// The largest value that can be represented by this integer type.
+  pure val MAX = (2^BITS) - 1
+  
+  /// Representation of an unsigned, bounded integer.
+  ///
+  /// - `UInt_Ok(v)` represents the integer `v`, such that `MIN <= v <= MAX`.
+  /// - `UInt_Err(msg)` holds a message explaining the out of bounds error.
+  ///
+  /// NOTE: values of this type must only be constructed using `UInt`,
+  /// and never via `Ok` or `Err` directly.
+  // TODO: Replace with polymorphic result type, once that is available
+  //       See https://github.com/informalsystems/quint/issues/1073
+  type UIntT = UInt_Ok(int) | UInt_Err(str)
+
+  /// Given an integer `x`, returns true iff `x` lies in the `[MIN, MAX]` interval.
+  pure def isInRange(x: int): bool = MIN <= x and x <= MAX
+
+  /// `UInt(x)` is a bounded unsigned integer if `x` is inside the `[MIN, MAX]` interval,
+  /// otherwise it is an `"out of range"` error.
+  pure def UInt(x: int): UIntT = if (isInRange(x)) UInt_Ok(x) else UInt_Err("out of range")
+
+  /// `u.bind(x => f(x))` is `f(x)` iff `u` is `UInt_Ok(x)`, i.e., if `u` is a valid bounded int wrapping `x`,
+  /// otherwise, when `u` is `UInt_Err(msg)`, it is `u`.
+  ///
+  /// ## Example
+  ///
+  /// ```
+  /// def checkedIncr(u: UintT): UintT = checkedAdd(u, UIntT(1))
+  /// run incr_UintT_twice_test = assert(UInt(0).bind(checkedIncr).bind(checkedIncr) = UInt(2))
+  /// ```
+  def bind(u: UIntT, f: (int => UIntT)): UIntT = match u {
+    | UInt_Ok(i) => f(i)
+    | UInt_Err(_) => u
+  }
+
+  /// `f.app(u, v, msg)` is `UInt(f(x,y))` if `u` is `UInt_Ok(x)` and `v` is `UInt_Ok(y)`.
+  /// If `UInt(f(x,y))` is out of range, it is `UInt_Err(msg)`.
+  pure def app(op: (int, int) => int, lhs: UIntT, rhs:UIntT, errMsg: str): UIntT =
+    lhs.bind(x => rhs.bind(y =>
+      val res = op(x, y)
+      if (isInRange(res)) UInt_Ok(res) else UInt_Err(errMsg)))
+
+  /// Computes the absolute difference between lhs and rhs.
+  pure def absDiff(lhs: UIntT, rhs: UIntT): UIntT = {
+    ((x, y) => {
+      val res = x - y
+      if (res < 0) -res else res
+    }).app(lhs, rhs,
+      "impossible")
+  }
+
+    ////////////////////////
+   // CHECKED OPERATIONS //
+  ////////////////////////
+
+  // TODO: In the following we have to eta-expand calls to `ifoo` builtins
+  // due to https://github.com/informalsystems/quint/issues/1332
+  // We should simplify those once this issue with the simulator is fixed.
+
+  /// Checked integer addition.
+  /// Errors with "overflow"
+  pure def checkedAdd(lhs: UIntT, rhs: UIntT): UIntT = ((x,y) => iadd(x,y)).app(lhs, rhs, "overflow")
+
+  /// Checked integer subtraction.
+  /// Errors with "underflow".
+  pure def checkedSub(lhs: UIntT, rhs: UIntT): UIntT = ((x,y) => isub(x,y)).app(lhs, rhs, "underflow")
+
+  /// Checked integer multiplication.
+  /// Errors with "overflow".
+  pure def checkedMul(lhs: UIntT, rhs: UIntT): UIntT = ((x,y) => imul(x,y)).app(lhs, rhs, "overflow")
+
+  /// Checked integer division.
+  /// Errors with "division by zero".
+  pure def checkedDiv(lhs: UIntT, rhs: UIntT): UIntT =
+    lhs.bind(
+      l => rhs.bind(
+      r =>
+        if (r == 0)
+          UInt_Err("division by zero")
+        else
+          UInt_Ok(l / r)))
+
+  /// Checked integer modulo.
+  /// Errors with "division by zero".
+  pure def checkedRem(lhs: UIntT, rhs: UIntT): UIntT =
+    lhs.bind(
+      l => rhs.bind(
+      r =>
+        if (r == 0)
+          UInt_Err("division by zero")
+        else
+          UInt_Ok(l % r)))
+
+  /// Checked exponentiation.
+  /// Errors with "overflow".
+  pure def checkedPow(lhs: UIntT, rhs: UIntT): UIntT =
+    lhs.bind(
+      l => rhs.bind(
+      r =>
+        if (l == r and l == 0)
+          UInt_Err("undefined")
+        else
+          ((x,y) => ipow(x,y)).app(lhs, rhs, "overflow")))
+
+
+    ///////////////////////////
+   // SATURATING OPERATIONS //
+  ///////////////////////////
+
+  /// Saturating integer addition.
+  /// Computes `lhs + rhs`, saturating at the numeric bounds instead of overflowing.
+  pure def saturatingAdd(lhs: UIntT, rhs: UIntT): UIntT =
+    ((x, y) =>
+      val res = x + y
+      if (res < MAX) res else MAX)
+    .app(lhs, rhs, "impossible")
+
+  /// Saturating integer subtraction.
+  /// Computes `lhs - rhs`, saturating at the numeric bounds instead of overflowing.
+  pure def saturatingSub(lhs: UIntT, rhs: UIntT): UIntT =
+    ((x, y) =>
+      val res = x - y
+      if (res > MIN) res else MIN)
+    .app(lhs, rhs, "impossible")
+
+  /// Saturating integer subtraction.
+  /// Computes `lhs * rhs`, saturating at the numeric bounds instead of overflowing.
+  pure def saturatingMul(lhs: UIntT, rhs: UIntT): UIntT =
+    ((x, y) =>
+      val res = x * y
+      if (res < MAX) res else MAX)
+    .app(lhs, rhs, "impossible")
+
+  /// Saturating exponentiation.
+  /// Computes `lhs ^ rhs`, saturating at the numeric bounds instead of overflowing.
+  pure def saturatingPow(lhs: UIntT, rhs: UIntT): UIntT =
+    lhs.bind(
+      l => rhs.bind(
+      r =>
+      if (l == r and l == 0)
+        UInt_Err("undefined")
+      else
+        val res = l ^ r
+        UInt_Ok(if (res < MAX) res else MAX)))
+
+    /////////////////////////
+   // WRAPPING OPERATIONS //
+  /////////////////////////
+
+  /// Wrapping integer addition.
+  /// Computes `lhs + rhs`, wrapping around at the boundary of the type.
+  pure def wrappingAdd(lhs: UIntT, rhs: UIntT): UIntT =
+    ((x, y) => (x + y) % (MAX + 1)).app(lhs, rhs, "impossible")
+
+  pure def wrappingSubInt(x: int, y: int): int = {
+    val res = x - y
+    val adjusted = if (res < MIN) (res + (MAX + 1)) else res
+    adjusted % (MAX + 1)
+  }
+
+  /// Wrapping integer subtraction.
+  /// Computes `lhs - rhs`, wrapping around at the boundary of the type.
+  pure def wrappingSub(lhs: UIntT, rhs: UIntT): UIntT = wrappingSubInt.app(lhs, rhs, "impossible")
+
+  /// Wrapping integer multiplication.
+  /// Computes `lhs * rhs`, wrapping around at the boundary of the type.
+  pure def wrappingMul(lhs: UIntT, rhs: UIntT): UIntT =
+    ((x, y) => (x * y) % (MAX + 1)).app(lhs, rhs, "impossible")
+
+  /// Wrapping integer division.
+  /// Computes `lhs / rhs`. Wrapped division on unsigned types is just normal division. 
+  /// There’s no way wrapping could ever happen. 
+  /// This operator exists, so that all operations are accounted for in the wrapping operations.
+  pure def wrappingDiv(lhs: UIntT, rhs: UIntT): UIntT = checkedDiv(lhs, rhs)
+
+  /// Wrapping integer remainder.
+  /// Computes `lhs % rhs`. Wrapped remainder on unsigned types is just normal remainder. 
+  /// There’s no way wrapping could ever happen. 
+  /// This operator exists, so that all operations are accounted for in the wrapping operations.
+  pure def wrappingRem(lhs: UIntT, rhs: UIntT): UIntT = checkedRem(lhs, rhs)
+
+  /// Wrapping exponentiation.
+  /// Computes `lhs ^ rhs`, wrapping around at the boundary of the type.
+  pure def wrappingPow(lhs: UIntT, rhs: UIntT): UIntT =
+    lhs.bind(
+      l => rhs.bind(
+      r =>
+      if (l == r and l == 0)
+        UInt_Err("undefined")
+      else
+        UInt_Ok((l ^ r) % (MAX + 1))))
+}
+
+module BoundedUInt_Test {
+  import BoundedUInt.*
+
+  // Sanity check, tests become degenerate when BITS = 1 (even moreso if <= 0)
+  pure val BitsTest = assert(BITS > 1)
+
+  /////////////
+  // CHECKED //
+  /////////////
+
+  // Checked add
+  pure val CAddInvsTest = and {
+    assert(checkedAdd(UInt(0), UInt(0)) == UInt_Ok(0)),
+    assert(checkedAdd(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(checkedAdd(UInt(MAX - 1), UInt(0)) == UInt_Ok(MAX - 1)),
+    assert(checkedAdd(UInt(MAX), UInt(0)) == UInt_Ok(MAX)),
+    assert(checkedAdd(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(checkedAdd(UInt(0), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(checkedAdd(UInt(1), UInt(MAX)) == UInt_Err("overflow")),
+    assert(checkedAdd(UInt(MAX - 1), UInt(MAX)) == UInt_Err("overflow")),
+    assert(checkedAdd(UInt(MAX), UInt(MAX)) == UInt_Err("overflow")),
+    assert(checkedAdd(UInt(MAX), UInt(MAX + 1)) == UInt_Err("out of range")),
+  }
+
+  // Checked sub
+  pure val CSubInvsTest = and {
+    assert(checkedSub(UInt(0), UInt(0)) == UInt_Ok(0)),
+    assert(checkedSub(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(checkedSub(UInt(MAX - 1), UInt(0)) == UInt_Ok(MAX - 1)),
+    assert(checkedSub(UInt(MAX), UInt(0)) == UInt_Ok(MAX)),
+    assert(checkedSub(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(checkedSub(UInt(0), UInt(MAX)) == UInt_Err("underflow")),
+    assert(checkedSub(UInt(1), UInt(MAX)) ==  UInt_Err("underflow")),
+    assert(checkedSub(UInt(MAX - 1), UInt(MAX)) ==  UInt_Err("underflow")),
+    assert(checkedSub(UInt(MAX), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedSub(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range")),
+  }
+
+  // Checked mul
+  pure val CMulInvsTest = and {
+    assert(checkedMul(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(checkedMul(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(checkedMul(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(checkedMul(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(checkedMul(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(checkedMul(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedMul(UInt(1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(checkedMul(UInt(MAX - 1), UInt(MAX)) == UInt_Err("overflow")),
+    assert(checkedMul(UInt(MAX), UInt(MAX)) == UInt_Err("overflow")),
+    assert(checkedMul(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range")),
+  }
+
+  // Checked div
+  pure val CDivInvsTest = and {
+    assert(checkedDiv(UInt(0), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedDiv(UInt(1), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedDiv(UInt(MAX - 1), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedDiv(UInt(MAX), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedDiv(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(checkedDiv(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(checkedDiv(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(checkedDiv(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(checkedDiv(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(checkedDiv(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(checkedDiv(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedDiv(UInt(1), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedDiv(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedDiv(UInt(MAX), UInt(MAX)) == UInt_Ok(1)),
+    assert(checkedDiv(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Checked rem
+  pure val CRemInvsTest = and {
+    assert(checkedRem(UInt(0), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedRem(UInt(1), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedRem(UInt(MAX - 1), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedRem(UInt(MAX), UInt(0)) == UInt_Err("division by zero")),
+    assert(checkedRem(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(checkedRem(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(checkedRem(UInt(1), UInt(1)) == UInt_Ok(0)),
+    assert(checkedRem(UInt(MAX - 1), UInt(1)) == UInt_Ok(0)),
+    assert(checkedRem(UInt(MAX), UInt(1)) == UInt_Ok(0)),
+    assert(checkedRem(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(checkedRem(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedRem(UInt(1), UInt(MAX)) == UInt_Ok(1)),
+    assert(checkedRem(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(MAX - 1)),
+    assert(checkedRem(UInt(MAX), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedRem(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Checked Pow
+  pure val CPowInvsTest = and {
+    assert(checkedPow(UInt(0), UInt(0)) == UInt_Err("undefined")),
+    assert(checkedPow(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(checkedPow(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(checkedPow(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(checkedPow(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(checkedPow(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(checkedPow(UInt(MAX), UInt(0)) == UInt_Ok(1)),
+    assert(checkedPow(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(checkedPow(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(checkedPow(UInt(1), UInt(MAX)) == UInt_Ok(1)),
+    assert(checkedPow(UInt(2), UInt(BITS - 1)) == UInt_Ok(2^(BITS - 1))),
+    assert(checkedPow(UInt(2), UInt(BITS)) == UInt_Err("overflow")),
+    assert(checkedPow(UInt(2), UInt(BITS + 1)) == UInt_Err("overflow")),
+  }
+
+  ////////////////
+  // SATURATING //
+  ////////////////
+
+  // Saturating add
+  pure val SAddInvsTest = and {
+    assert(saturatingAdd(UInt(0), UInt(0)) == UInt_Ok(0)),
+    assert(saturatingAdd(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(saturatingAdd(UInt(MAX - 1), UInt(0)) == UInt_Ok(MAX - 1)),
+    assert(saturatingAdd(UInt(MAX), UInt(0)) == UInt_Ok(MAX)),
+    assert(saturatingAdd(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(saturatingAdd(UInt(0), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingAdd(UInt(1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingAdd(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingAdd(UInt(MAX), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingAdd(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Saturating sub
+  pure val SSubInvsTest = and {
+    assert(saturatingSub(UInt(0), UInt(0)) == UInt_Ok(0)),
+    assert(saturatingSub(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(saturatingSub(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(saturatingSub(UInt(MAX - 1), UInt(0)) == UInt_Ok(MAX - 1)),
+    assert(saturatingSub(UInt(MAX), UInt(0)) == UInt_Ok(MAX)),
+    assert(saturatingSub(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(saturatingSub(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(saturatingSub(UInt(1), UInt(MAX)) == UInt_Ok(0)),
+    assert(saturatingSub(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(0)),
+    assert(saturatingSub(UInt(MAX), UInt(MAX)) == UInt_Ok(0)),
+    assert(saturatingSub(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Saturating mul
+  pure val SMulInvsTest = and {
+    assert(saturatingMul(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(saturatingMul(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(saturatingMul(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(saturatingMul(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(saturatingMul(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(saturatingMul(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(saturatingMul(UInt(1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingMul(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingMul(UInt(MAX), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(saturatingMul(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Saturating pow
+  pure val SPowInvsTest = and {
+    assert(saturatingPow(UInt(0), UInt(0)) == UInt_Err("undefined")),
+    assert(saturatingPow(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(saturatingPow(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(saturatingPow(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(saturatingPow(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(saturatingPow(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(saturatingPow(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(saturatingPow(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(saturatingPow(UInt(1), UInt(MAX)) == UInt_Ok(1)),
+    assert(saturatingPow(UInt(2), UInt(BITS - 1)) == UInt_Ok(2^(BITS - 1))),
+    assert(saturatingPow(UInt(2), UInt(BITS)) == UInt_Ok(MAX)),
+    assert(saturatingPow(UInt(2), UInt(BITS + 1)) == UInt_Ok(MAX)),
+  }
+
+  //////////////
+  // WRAPPING //
+  //////////////
+
+  // Wrapping add
+  pure val WAddInvsTest = and {
+    assert(wrappingAdd(UInt(0), UInt(0)) == UInt_Ok(0)),
+    assert(wrappingAdd(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(wrappingAdd(UInt(MAX - 1), UInt(0)) == UInt_Ok(MAX - 1)),
+    assert(wrappingAdd(UInt(MAX), UInt(0)) == UInt_Ok(MAX)),
+    assert(wrappingAdd(UInt(MAX), UInt(1)) == UInt_Ok(0)),
+    assert(wrappingAdd(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(wrappingAdd(UInt(0), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(wrappingAdd(UInt(1), UInt(MAX)) == UInt_Ok(0)),
+    assert(wrappingAdd(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(MAX - 2)),
+    assert(wrappingAdd(UInt(MAX), UInt(MAX)) == UInt_Ok(MAX - 1)),
+    assert(wrappingAdd(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Wrapping sub
+  pure val WSubInvsTest = and {
+    assert(wrappingSub(UInt(0), UInt(0)) == UInt_Ok(0)),
+    assert(wrappingSub(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(wrappingSub(UInt(0), UInt(1)) == UInt_Ok(MAX)),
+    assert(wrappingSub(UInt(1), UInt(1)) == UInt_Ok(0)),
+    assert(wrappingSub(UInt(MAX - 1), UInt(0)) == UInt_Ok(MAX - 1)),
+    assert(wrappingSub(UInt(MAX), UInt(0)) == UInt_Ok(MAX)),
+    assert(wrappingSub(UInt(MAX + 1), UInt(0)) == UInt_Err("out of range")),
+    assert(wrappingSub(UInt(0), UInt(MAX)) == UInt_Ok(1)),
+    assert(wrappingSub(UInt(1), UInt(MAX)) == UInt_Ok(2)),
+    assert(wrappingSub(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(wrappingSub(UInt(MAX), UInt(MAX)) == UInt_Ok(0)),
+    assert(wrappingSub(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Wrapping mul
+  pure val WMulInvsTest = and {
+    assert(wrappingMul(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(wrappingMul(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(wrappingMul(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(wrappingMul(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(wrappingMul(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(wrappingMul(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(wrappingMul(UInt(1), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(wrappingMul(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(2)),
+    assert(wrappingMul(UInt(MAX), UInt(MAX)) == UInt_Ok(1)),
+    assert(wrappingMul(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+  // Wrapping div == checked div
+  // Wrapping rem == checked rem
+  
+  // Wrapping Pow
+  pure val WPowInvsTest = and {
+    assert(wrappingPow(UInt(0), UInt(0)) == UInt_Err("undefined")),
+    assert(wrappingPow(UInt(0), UInt(1)) == UInt_Ok(0)),
+    assert(wrappingPow(UInt(1), UInt(0)) == UInt_Ok(1)),
+    assert(wrappingPow(UInt(1), UInt(1)) == UInt_Ok(1)),
+    assert(wrappingPow(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(wrappingPow(UInt(MAX), UInt(1)) == UInt_Ok(MAX)),
+    assert(wrappingPow(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(wrappingPow(UInt(0), UInt(MAX)) == UInt_Ok(0)),
+    assert(wrappingPow(UInt(1), UInt(MAX)) == UInt_Ok(1)),
+    assert(wrappingPow(UInt(2), UInt(BITS - 1)) == UInt_Ok(2^(BITS - 1))),
+    assert(wrappingPow(UInt(2), UInt(BITS)) == UInt_Ok(0)),
+    assert(wrappingPow(UInt(2), UInt(BITS + 1)) == UInt_Ok(0)),
+  }
+
+  //////////////
+  // ABS DIFF //
+  //////////////
+
+  pure val AbsDiffTest = and {
+    assert(absDiff(UInt(0), UInt(1)) == UInt_Ok(1)),
+    assert(absDiff(UInt(1), UInt(1)) == UInt_Ok(0)),
+    assert(absDiff(UInt(MAX - 1), UInt(1)) == UInt_Ok(MAX - 2)),
+    assert(absDiff(UInt(MAX), UInt(1)) == UInt_Ok(MAX - 1)),
+    assert(absDiff(UInt(MAX + 1), UInt(1)) == UInt_Err("out of range")),
+    assert(absDiff(UInt(0), UInt(MAX)) == UInt_Ok(MAX)),
+    assert(absDiff(UInt(1), UInt(MAX)) == UInt_Ok(MAX - 1)),
+    assert(absDiff(UInt(MAX - 1), UInt(MAX)) == UInt_Ok(1)),
+    assert(absDiff(UInt(MAX), UInt(MAX)) == UInt_Ok(0)),
+    assert(absDiff(UInt(MAX + 1), UInt(MAX)) == UInt_Err("out of range"))
+  }
+
+}
+
+module BoundedUInt8Test {
+  import BoundedUInt_Test(BITS = 8).*
+}
+
+module BoundedUInt16Test {
+  import BoundedUInt_Test(BITS = 16).*
+}
+
+module BoundedUInt32Test {
+  import BoundedUInt_Test(BITS = 32).*
+}
diff --git a/examples/ctf-01/quint/lib/bank.qnt b/examples/ctf-01/quint/lib/bank.qnt
new file mode 100644
index 0000000..814d840
--- /dev/null
+++ b/examples/ctf-01/quint/lib/bank.qnt
@@ -0,0 +1,25 @@
+// -*- mode: Bluespec; -*-
+
+module bank {
+  import cw_types.* from "./cw_types"
+  type Bank = Addr -> Denom -> int
+
+  pure def send(bank: Bank, source_addr: Addr, msg: { to_address: Addr, amount: List[Coin] }): Result[Bank, ContractError] = {
+    // FIXME: consider multiple coins
+    pure val amount = msg.amount[0].amount
+    pure val denom = msg.amount[0].denom
+    if (amount >= 0 and bank.get(source_addr).get(denom) >= amount) {
+      val new_bank = bank
+        .setBy(source_addr, balances => balances.setBy(denom, balance => balance - amount))
+        .setBy(msg.to_address, balances => balances.setBy(denom, balance => balance + amount))
+
+      Ok(new_bank)
+    } else {
+      Err("Not enough balance")
+    }
+  }
+
+  pure def query_balance(bank: Bank, address: Addr, denom: Denom): Coin = {
+    { amount: bank.get(address).get(denom), denom: denom }
+  }
+}
diff --git a/examples/ctf-01/quint/lib/basicSpells.qnt b/examples/ctf-01/quint/lib/basicSpells.qnt
new file mode 100644
index 0000000..f7588e4
--- /dev/null
+++ b/examples/ctf-01/quint/lib/basicSpells.qnt
@@ -0,0 +1,185 @@
+// -*- mode: Bluespec; -*-
+/**
+ * This module collects definitions that are ubiquitous.
+ * One day they will become the standard library of Quint.
+ */
+module basicSpells {
+  type Option[a] = Some(a) | None
+
+  /// An annotation for writing preconditions.
+  /// - @param __cond condition to check
+  /// - @returns true if and only if __cond evaluates to true
+  pure def require(__cond: bool): bool = __cond
+
+  run requireTest = all {
+    assert(require(4 > 3)),
+    assert(not(require(false))),
+  }
+
+  /// A convenience operator that returns a string error code,
+  ///  if the condition does not hold true.
+  ///
+  /// - @param __cond condition to check
+  /// - @param __error a non-empty error message
+  /// - @returns "", when __cond holds true; otherwise __error
+  pure def requires(__cond: bool, __error: str): str = {
+    if (__cond) "" else __error
+  }
+
+  run requiresTest = all {
+    assert(requires(4 > 3, "4 > 3") == ""),
+    assert(requires(4 < 3, "false: 4 < 3") == "false: 4 < 3"),
+  }
+
+
+  /// Compute the maximum of two integers.
+  ///
+  /// - @param __i first integer
+  /// - @param __j second integer
+  /// - @returns the maximum of __i and __j
+  pure def max(__i: int, __j: int): int = {
+    if (__i > __j) __i else __j
+  }
+
+  run maxTest = all {
+    assert(max(3, 4) == 4),
+    assert(max(6, 3) == 6),
+    assert(max(10, 10) == 10),
+    assert(max(-3, -5) == -3),
+    assert(max(-5, -3) == -3),
+  }
+
+  /// Compute the absolute value of an integer
+  ///
+  /// - @param __i : an integer whose absolute value we are interested in
+  /// - @returns |__i|, the absolute value of __i
+  pure def abs(__i: int): int = {
+    if (__i < 0) -__i else __i
+  }
+
+  run absTest = all {
+    assert(abs(3) == 3),
+    assert(abs(-3) == 3),
+    assert(abs(0) == 0),
+  }
+
+  /// Remove a set element.
+  ///
+  /// - @param __set a set to remove an element from
+  /// - @param __elem an element to remove
+  /// - @returns a new set that contains all elements of __set but __elem
+  pure def setRemove(__set: Set[a], __elem: a): Set[a] = {
+    __set.exclude(Set(__elem))
+  }
+
+  run setRemoveTest = all {
+    assert(Set(2, 4) == Set(2, 3, 4).setRemove(3)),
+    assert(Set() == Set().setRemove(3)),
+  }
+
+  /// Test whether a key is present in a map
+  ///
+  /// - @param __map a map to query
+  /// - @param __key the key to look for
+  /// - @returns true if and only __map has an entry associated with __key
+  pure def has(__map: a -> b, __key: a): bool = {
+    __map.keys().contains(__key)
+  }
+
+  run hasTest = all {
+    assert(Map(2 -> 3, 4 -> 5).has(2)),
+    assert(not(Map(2 -> 3, 4 -> 5).has(6))),
+  }
+
+  /// Get the map value associated with a key, or the default,
+  /// if the key is not present.
+  ///
+  /// - @param __map the map to query
+  /// - @param __key the key to search for
+  /// - @returns the value associated with the key, if __key is
+  ///   present in the map, and __default otherwise
+  pure def getOrElse(__map: a -> b, __key: a, __default: b): b = {
+    if (__map.has(__key)) {
+      __map.get(__key)
+    } else {
+      __default
+    }
+  }
+
+  run getOrElseTest = all {
+    assert(Map(2 -> 3, 4 -> 5).getOrElse(2, 0) == 3),
+    assert(Map(2 -> 3, 4 -> 5).getOrElse(7, 11) == 11),
+  }
+
+  /// Remove a map entry.
+  ///
+  /// - @param __map a map to remove an entry from
+  /// - @param __key the key of an entry to remove
+  /// - @returns a new map that contains all entries of __map
+  ///          that do not have the key __key
+  pure def mapRemove(__map: a -> b, __key: a): a -> b = {
+    __map.keys().setRemove(__key).mapBy(__k => __map.get(__k))
+  }
+
+  run mapRemoveTest = all {
+    assert(Map(3 -> 4, 7 -> 8) == Map(3 -> 4, 5 -> 6, 7 -> 8).mapRemove(5)),
+    assert(Map() == Map().mapRemove(3)),
+  }
+
+  /// Removes a set of map entries.
+  ///
+  /// - @param __map a map to remove entries from
+  /// - @param __keys a set of keys for entries to remove from the map
+  /// - @returns a new map that contains all entries of __map
+  ///          that do not have a key in __keys
+  pure def mapRemoveAll(__map: a -> b, __keys: Set[a]): a -> b = {
+      __map.keys().exclude(__keys).mapBy(__k => __map.get(__k))
+  }
+
+  run mapRemoveAllTest =
+      val m = Map(3 -> 4, 5 -> 6, 7 -> 8)
+      all {
+          assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)),
+          assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)),
+      }
+
+  /// Get the set of values of a map.
+  ///
+  /// - @param __map a map from type a to type b
+  /// - @returns the set of all values in the map
+  pure def values(__map: a -> b): Set[b] = {
+    __map.keys().map(k => __map.get(k))
+  }
+
+  run valuesTest = all {
+    assert(values(Map()) == Set()),
+    assert(values(Map(1 -> 2, 2 -> 3)) == Set(2, 3)),
+    assert(values(Map(1 -> 2, 2 -> 3, 3 -> 2)) == Set(2, 3)),
+  }
+
+  /// Whether a set is empty
+  ///
+  /// - @param s a set of any type
+  /// - @returns true iff the set is the empty set
+  pure def empty(s: Set[a]): bool = s == Set()
+
+  run emptyTest = all {
+    assert(empty(Set()) == true),
+    assert(empty(Set(1, 2)) == false),
+    assert(empty(Set(Set())) == false),
+  }
+
+  pure def listFilter(l: List[a], f: (a) => bool): List[a] =
+    l.foldl([], (acc, e) => if (f(e)) acc.append(e) else acc)
+
+  pure def listMap(l: List[a], f: (a) => b): List[b] =
+    l.foldl([], (acc, e) => acc.append(f(e)))
+
+  //// Returns a set of the elements in the list.
+  ////
+  //// - @param l a list
+  //// - @returns a set of the elements in l
+  pure def toSet(l: List[a]): Set[a] = {
+      l.foldl(Set(), (s, e) => s.union(Set(e)))
+  }
+}
diff --git a/examples/ctf-01/quint/lib/cw_types.qnt b/examples/ctf-01/quint/lib/cw_types.qnt
new file mode 100644
index 0000000..38614a1
--- /dev/null
+++ b/examples/ctf-01/quint/lib/cw_types.qnt
@@ -0,0 +1,152 @@
+// -*- mode: Bluespec; -*-
+
+module cw_types {
+  import basicSpells.* from "./basicSpells"
+
+  type Addr = str
+  type Denom = str
+
+  type TODO = str
+  type ContractError = str
+
+  type ReplyOn =
+    | ReplyOn_Always
+    | ReplyOn_Error
+    | ReplyOn_Success
+    | ReplyOn_Never
+
+  type SubMsg = { id: int, msg: CosmosMsg, reply_on: ReplyOn, gas_limit: Option[int] }
+  type Attribute = { key: str, value: CW_Serialized }
+  type Event = { ty: str, attributes: List[Attribute] }
+
+  type Response = {
+    messages: List[SubMsg],
+    attributes: List[Attribute],
+    events: List[Event],
+    data: Option[str],
+  }
+
+  type CosmosMsg =
+    | CosmosMsg_Wasm(WasmMsg)
+    | CosmosMsg_Bank(BankMsg)
+    // | CosmosMsg_Custom(T)
+    // | CosmosMsg_Staking(StakingMsg)
+    // | CosmosMsg_Distribution(DistributionMsg)
+
+  type WasmMsg =
+    | WasmMsg_Instantiate({
+        admin: Option[str],
+        code_id: int,
+        // msg is the JSON-encoded InstantiateMsg struct (as raw Binary)
+        // msg: InstantiateMsg, // TODO: we need polymorphism
+        funds: List[Coin],
+        // A human-readable label for the contract.
+        //
+        // Valid values should:
+        // - not be empty
+        // - not be bigger than 128 bytes (or some chain-specific limit)
+        // - not start / end with whitespace
+        label: str,
+    })
+    // | Execute(...)
+
+  type BankMsg =
+    | BankMsg_Send({ to_address: str, amount: List[Coin] })
+
+  pure val Response_new = { messages: [], attributes: [], events: [], data: None }
+
+  /// This is used for cases when we use ReplyOn::Never and the id doesn't matter
+  pure val UNUSED_MSG_ID = 0
+
+  pure def SubMsg_new(msg: CosmosMsg): SubMsg = {
+    id: UNUSED_MSG_ID,
+    msg: msg,
+    reply_on: ReplyOn_Never,
+    gas_limit: None,
+  }
+
+  pure def SubMsg_reply_on_sucess(msg: CosmosMsg, id: int): SubMsg = {
+    __reply_on(msg, id, ReplyOn_Success)
+  }
+
+  pure def SubMsg_reply_on_error(msg: CosmosMsg, id: int): SubMsg = {
+    __reply_on(msg, id, ReplyOn_Error)
+  }
+
+  pure def SubMsg_reply_always(msg: CosmosMsg, id: int): SubMsg = {
+    __reply_on(msg, id, ReplyOn_Always)
+  }
+
+  pure def with_gas_limit(msg: SubMsg, limit: int): SubMsg = {
+    { ...msg, gas_limit: Some(limit) }
+  }
+
+  pure def __reply_on(msg: CosmosMsg, id: int, reply_on: ReplyOn): SubMsg = {
+    {
+      id: id,
+      msg: msg,
+      reply_on: reply_on,
+      gas_limit: None,
+    }
+  }
+
+  def should_reply_on_success(r) = match r {
+    | ReplyOn_Always => true
+    | ReplyOn_Success => true
+    | _ => false
+  }
+
+  def should_reply_on_error(r: ReplyOn): bool = match r {
+    | ReplyOn_Always => true
+    | ReplyOn_Error => true
+    | _ => false
+  }
+
+  type SubMsgResponse = {
+    events: List[Event],
+    data: Option[CW_Serialized]
+  }
+
+  type Reply = {
+    id: int,
+    result: Result[SubMsgResponse, ContractError],
+  }
+
+  pure def add_attribute(r: Response, k: str, v: CW_Serialized): Response = {
+    val attribute = { key: k, value: v }
+    { ...r, attributes: r.attributes.append(attribute) }
+  }
+
+  pure def add_message(r: Response, m: CosmosMsg): Response = {
+    { ...r, messages: r.messages.append(SubMsg_new(m)) }
+  }
+
+  pure def add_submessage(r: Response, m: SubMsg): Response = {
+    { ...r, messages: r.messages.append(m) }
+  }
+
+  type Result[ok, err] = Ok(ok) | Err(err)
+
+  type Deps = {
+    storage: TODO,
+    api: TODO,
+    querier: TODO,
+  }
+
+  type Env = { block: { time: int /*, height: int */ } } // TODO
+
+  type Coin = {
+    denom: str,
+    amount: int
+  }
+
+  type MessageInfo = {
+    sender: str,
+    funds: List[Coin]
+  }
+
+  type CW_Serialized =
+    | FromStr(str)
+    | FromInt(int)
+    | FromListInt(List[int])
+}
diff --git a/examples/ctf-01/quint/lib/cw_utils.qnt b/examples/ctf-01/quint/lib/cw_utils.qnt
new file mode 100644
index 0000000..e662dbe
--- /dev/null
+++ b/examples/ctf-01/quint/lib/cw_utils.qnt
@@ -0,0 +1,34 @@
+// -*- mode: Bluespec; -*-
+
+// https://docs.rs/cw-utils/0.13.4/src/cw_utils/payment.rs.html#32-39
+module cw_utils {
+  import cw_types.* from "./cw_types"
+
+  def one_coin(info: MessageInfo): Result[Coin, ContractError] = {
+    if (info.funds.indices().size() == 0) {
+      Err("No funds")
+    } else if (info.funds.indices().size() == 1) {
+      val coin = info.funds[0]
+      if (coin.amount == 0) {
+        Err("Zero funds")
+      } else {
+        Ok(coin)
+      }
+    } else {
+      Err("Multiple Denoms")
+    }
+  }
+
+  def must_pay(info: MessageInfo, denom: str): Result[int, ContractError] = {
+    match one_coin(info) {
+      | Err(err) => Err(err)
+      | Ok(coin) => {
+        if (coin.denom != denom) {
+          Err("Wrong Denom")
+        } else {
+          Ok(coin.amount)
+        }
+      }
+    }
+  }
+}
diff --git a/examples/ctf-01/quint/lib/messaging.qnt b/examples/ctf-01/quint/lib/messaging.qnt
new file mode 100644
index 0000000..b0ef7dc
--- /dev/null
+++ b/examples/ctf-01/quint/lib/messaging.qnt
@@ -0,0 +1,47 @@
+// -*- mode: Bluespec; -*-
+
+module messaging {
+  import cw_types.* from "./cw_types"
+  import bank from "./bank"
+  import basicSpells.* from "./basicSpells"
+
+  pure def get_message(result_val: Result[Response, ContractError]): (Result[Response, ContractError], Option[SubMsg]) = {
+    match result_val {
+      | Ok(response) =>
+        if (response.messages.indices().size() > 0) {
+          val submsg = response.messages.head()
+          val new_result = Ok({ ...response, messages: response.messages.listFilter(m => m != submsg) })
+          (new_result, Some(submsg))
+        } else {
+          (result_val, None)
+        }
+
+      | _ => (result_val, None)
+    }
+  }
+
+  pure def process_message(state, env, contract_address, submsg, reply) = {
+    match submsg.msg {
+      | CosmosMsg_Wasm(wasm_msg) => state // FIXME
+      | CosmosMsg_Bank(bank_msg) =>
+        match bank_msg {
+          | BankMsg_Send(msg) => match bank::send(state.bank, contract_address, msg) {
+            | Ok(new_bank) =>
+               if (should_reply_on_success(submsg.reply_on)) {
+                 val reply_result = reply(state.contract_state, env, { id: submsg.id, result: Ok({ events: [/* TODO */], data: None }) })
+                 { bank: new_bank, result: reply_result._1, contract_state: reply_result._2 }
+               } else {
+                 { ...state, bank: new_bank }
+               }
+            | Err(err) =>
+               if (should_reply_on_error(submsg.reply_on)) {
+                 val reply_result = reply(state.contract_state, env, { id: submsg.id, result: Err(err) })
+                 { ...state, result: reply_result._1, contract_state: reply_result._2 }
+               } else {
+                  { ...state, result: Err(err) }
+               }
+           }
+        }
+    }
+  }
+}
diff --git a/examples/ctf-01/quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt b/examples/ctf-01/quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt
new file mode 100644
index 0000000..ef9d6b4
--- /dev/null
+++ b/examples/ctf-01/quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt
@@ -0,0 +1,203 @@
+// -*- mode: Bluespec; -*-
+module oaksecurity_cosmwasm_ctf_01 {
+  
+  import basicSpells.* from "./lib/basicSpells"
+  import cw_types.* from "./lib/cw_types"
+  import cw_utils.* from "./lib/cw_utils"
+  import messaging.* from "./lib/messaging"
+  import bank from "./lib/bank"
+
+  
+  var contract_state: ContractState
+  var result: Result
+  var bank: bank::Bank
+  var time: int
+
+  
+  pure val CONTRACT_ADDRESS = "contract0"
+
+  
+  pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS)
+  pure val DENOMS = Set("uawesome")
+  pure val MAX_AMOUNT = 200
+
+
+  type InstantiateMsg = { count: int }
+  type Lockup = { id: int, owner: Addr, amount: int, release_timestamp: int }
+  type ExecuteMsg =
+    | ExecuteMsg_Deposit
+    | ExecuteMsg_Withdraw({ ids: List[int] })
+  pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = {
+    (Ok(Response_new.add_attribute("action", FromStr("instantiate"))), state)
+  }
+
+  pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg {
+    | ExecuteMsg_Deposit(__r) => deposit(state, env, info)
+    | ExecuteMsg_Withdraw(__r) => withdraw(state, env, info, __r.ids)
+  }
+
+  pure def deposit(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = {
+    match must_pay(info, DENOM) {
+      | Err(s) => (Err(s), state)
+      | Ok(amount) => {
+        if(amount < MINIMUM_DEPOSIT_AMOUNT) {
+          (Err("Unauthorized"), state)
+        } else {
+          val id = state.last_id
+          val release_timestamp = env.block.time + LOCK_PERIOD
+          val lock = {
+            id: id,
+            owner: info.sender,
+            amount: amount,
+            release_timestamp: release_timestamp
+          }
+          val new_state = { ...state, lockups: { state.lockups.put(id, lock) }, last_id: id + 1 }
+          (Ok(Response_new.add_attribute("action", FromStr("deposit"))
+                          .add_attribute("id", FromInt(id))
+                          .add_attribute("owner", FromStr(lock.owner))
+                          .add_attribute("amout", FromInt(amount))
+                          .add_attribute("release_timestamp", FromInt(release_timestamp))
+             ), new_state)
+        }
+      }
+    }
+  }
+                            
+  action deposit_action = {
+    // TODO: Change next line according to fund expectations
+    pure val max_funds = MAX_AMOUNT
+    
+    pure val message: ExecuteMsg = ExecuteMsg_Deposit
+    execute_message(message, max_funds)
+  }
+
+  pure def withdraw(state: ContractState, env: Env, info: MessageInfo, ids: List[int]): (Result[Response, ContractError], ContractState) = {
+     val lockups = ids.listMap(id => state.lockups.get(id))
+
+    if (lockups.toSet().exists(lockup => lockup.owner != info.sender or env.block.time < lockup.release_timestamp)) {
+      (Err("Unauthorized"), state)
+    } else {
+      val total_amount = lockups.foldl(0, (acc, lockup) => {
+        acc + lockup.amount
+      })
+      val new_state = lockups.foldl(state, (acc, lockup) => {
+        { ...acc, lockups: acc.lockups.mapRemove(lockup.id) }
+      })
+
+      val msg = BankMsg_Send({
+        to_address: info.sender,
+        amount: [{
+          denom: DENOM,
+          amount: total_amount,
+        }]
+      })
+
+      (Ok(Response_new.add_attribute("action", FromStr("withdraw"))
+                      .add_attribute("ids", FromListInt(ids))
+                      .add_attribute("total_amount", FromInt(total_amount))
+                      .add_message(CosmosMsg_Bank(msg))), new_state)
+    }
+  }
+                            
+  action withdraw_action = all {
+    contract_state.lockups.keys().size() > 0,
+    // TODO: Change next line according to fund expectations
+    pure val max_funds = MAX_AMOUNT
+    nondet message_ids: List[int] = contract_state.lockups.keys().allListsUpTo(2).filter(l => l.length() > 0).oneOf()
+    val message: ExecuteMsg = ExecuteMsg_Withdraw({ ids: message_ids })
+    execute_message(message, max_funds)
+  }
+  pure val DENOM = "uawesome"
+  pure val MINIMUM_DEPOSIT_AMOUNT = 100
+  pure val LOCK_PERIOD = 60 * 60 * 24
+
+  type ContractState = {
+    last_id: int,
+    lockups: int -> Lockup
+  }
+
+  pure val init_contract_state = {
+    last_id: 1,
+    lockups: Map()
+  }
+
+  action execute_step = all {
+    any {
+      deposit_action,
+      withdraw_action
+    },
+    advance_time,
+  }
+
+  pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state)
+
+
+  pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT))
+
+  val env_val = { block: { time: time } }
+
+  action init = {
+    // TODO: Change next line according to fund expectations
+    pure val max_funds = 0
+
+    nondet sender = Set("admin").oneOf()
+    nondet denom = DENOMS.oneOf()
+    nondet amount = 0.to(max_funds).oneOf()
+    val funds = [{ denom: denom, amount: amount }]
+    val info = { sender: sender, funds: funds }
+
+    pure val message: InstantiateMsg = { count: 0 }
+    pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message)
+
+    all {
+      contract_state' = r._2,
+      bank' = init_bank_state,
+      result' = r._1,
+      time' = 0,
+    }
+  }
+
+
+  action execute_message(message, max_funds) = {
+    nondet sender = ADDRESSES.oneOf()
+    nondet denom = DENOMS.oneOf()
+    nondet amount = 0.to(max_funds).oneOf()
+    val funds = [{ denom: denom, amount: amount }]
+    val info = { sender: sender, funds: funds }
+
+    val r = execute(contract_state, env_val, info, message)
+    all {
+      bank.get(sender).get(denom) >= amount,
+      match r._1 {
+        | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount))
+                               .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount))
+        | Err(_) => bank' = bank
+      },
+      result' = r._1,
+      contract_state' = r._2,
+    }
+  }
+
+  action advance_time = time' = time + LOCK_PERIOD
+
+  action step = {
+    val message_getting = get_message(result)
+    val new_result = message_getting._1
+    val opt_message = message_getting._2
+    match opt_message {
+      | Some(submsg) => {
+          val current_state = { bank: bank, result: new_result, contract_state: contract_state }
+          val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply)
+          all {
+            bank' = new_state.bank,
+            result' = new_state.result,
+            contract_state' = new_state.contract_state,
+            advance_time,
+          }
+      }
+      | None => execute_step
+    }
+  }
+
+  val contract_balance_ok = bank.get(CONTRACT_ADDRESS).get(DENOM) >= 200 // initial balance
+}
diff --git a/examples/ctf-01/quint/test.itf.json b/examples/ctf-01/quint/test.itf.json
new file mode 100644
index 0000000..18709dd
--- /dev/null
+++ b/examples/ctf-01/quint/test.itf.json
@@ -0,0 +1 @@
+{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"quint/oaksecurity_cosmwasm_ctf_01_stubs.qnt","status":"violation","description":"Created by Quint on Wed Jun 05 2024 15:38:35 GMT-0300 (Brasilia Standard Time)","timestamp":1717612715803},"vars":["time","bank","result","contract_state"],"states":[{"#meta":{"index":0},"action_taken":"q::init","bank":{"#map":[["contract0",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender1",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender2",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender3",{"#map":[["uawesome",{"#bigint":"200"}]]}]]},"contract_state":{"last_id":{"#bigint":"1"},"lockups":{"#map":[]}},"nondet_picks":{"amount":{"tag":"Some","value":{"#bigint":"0"}},"denom":{"tag":"Some","value":"uawesome"},"message_ids":{"tag":"None","value":{"#tup":[]}},"sender":{"tag":"Some","value":"admin"}},"result":{"tag":"Ok","value":{"attributes":[{"key":"action","value":{"tag":"FromStr","value":"instantiate"}}],"data":{"tag":"None","value":{"#tup":[]}},"events":[],"messages":[]}},"time":{"#bigint":"0"}},{"#meta":{"index":1},"action_taken":"deposit_action","bank":{"#map":[["contract0",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender1",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender2",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender3",{"#map":[["uawesome",{"#bigint":"200"}]]}]]},"contract_state":{"last_id":{"#bigint":"1"},"lockups":{"#map":[]}},"nondet_picks":{"amount":{"tag":"Some","value":{"#bigint":"57"}},"denom":{"tag":"Some","value":"uawesome"},"message_ids":{"tag":"None","value":{"#tup":[]}},"sender":{"tag":"Some","value":"sender3"}},"result":{"tag":"Err","value":"Unauthorized"},"time":{"#bigint":"86400"}},{"#meta":{"index":2},"action_taken":"deposit_action","bank":{"#map":[["contract0",{"#map":[["uawesome",{"#bigint":"365"}]]}],["sender1",{"#map":[["uawesome",{"#bigint":"35"}]]}],["sender2",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender3",{"#map":[["uawesome",{"#bigint":"200"}]]}]]},"contract_state":{"last_id":{"#bigint":"2"},"lockups":{"#map":[[{"#bigint":"1"},{"amount":{"#bigint":"165"},"id":{"#bigint":"1"},"owner":"sender1","release_timestamp":{"#bigint":"172800"}}]]}},"nondet_picks":{"amount":{"tag":"Some","value":{"#bigint":"165"}},"denom":{"tag":"Some","value":"uawesome"},"message_ids":{"tag":"None","value":{"#tup":[]}},"sender":{"tag":"Some","value":"sender1"}},"result":{"tag":"Ok","value":{"attributes":[{"key":"action","value":{"tag":"FromStr","value":"deposit"}},{"key":"id","value":{"tag":"FromInt","value":{"#bigint":"1"}}},{"key":"owner","value":{"tag":"FromStr","value":"sender1"}},{"key":"amout","value":{"tag":"FromInt","value":{"#bigint":"165"}}},{"key":"release_timestamp","value":{"tag":"FromInt","value":{"#bigint":"172800"}}}],"data":{"tag":"None","value":{"#tup":[]}},"events":[],"messages":[]}},"time":{"#bigint":"172800"}},{"#meta":{"index":3},"action_taken":"withdraw_action","bank":{"#map":[["contract0",{"#map":[["uawesome",{"#bigint":"365"}]]}],["sender1",{"#map":[["uawesome",{"#bigint":"35"}]]}],["sender2",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender3",{"#map":[["uawesome",{"#bigint":"200"}]]}]]},"contract_state":{"last_id":{"#bigint":"2"},"lockups":{"#map":[[{"#bigint":"1"},{"amount":{"#bigint":"165"},"id":{"#bigint":"1"},"owner":"sender1","release_timestamp":{"#bigint":"172800"}}]]}},"nondet_picks":{"amount":{"tag":"Some","value":{"#bigint":"100"}},"denom":{"tag":"Some","value":"uawesome"},"message_ids":{"tag":"Some","value":[{"#bigint":"1"}]},"sender":{"tag":"Some","value":"contract0"}},"result":{"tag":"Err","value":"Unauthorized"},"time":{"#bigint":"259200"}},{"#meta":{"index":4},"action_taken":"withdraw_action","bank":{"#map":[["contract0",{"#map":[["uawesome",{"#bigint":"394"}]]}],["sender1",{"#map":[["uawesome",{"#bigint":"6"}]]}],["sender2",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender3",{"#map":[["uawesome",{"#bigint":"200"}]]}]]},"contract_state":{"last_id":{"#bigint":"2"},"lockups":{"#map":[]}},"nondet_picks":{"amount":{"tag":"Some","value":{"#bigint":"29"}},"denom":{"tag":"Some","value":"uawesome"},"message_ids":{"tag":"Some","value":[{"#bigint":"1"},{"#bigint":"1"}]},"sender":{"tag":"Some","value":"sender1"}},"result":{"tag":"Ok","value":{"attributes":[{"key":"action","value":{"tag":"FromStr","value":"withdraw"}},{"key":"ids","value":{"tag":"FromListInt","value":[{"#bigint":"1"},{"#bigint":"1"}]}},{"key":"total_amount","value":{"tag":"FromInt","value":{"#bigint":"330"}}}],"data":{"tag":"None","value":{"#tup":[]}},"events":[],"messages":[{"gas_limit":{"tag":"None","value":{"#tup":[]}},"id":{"#bigint":"0"},"msg":{"tag":"CosmosMsg_Bank","value":{"tag":"BankMsg_Send","value":{"amount":[{"amount":{"#bigint":"330"},"denom":"uawesome"}],"to_address":"sender1"}}},"reply_on":{"tag":"ReplyOn_Never","value":{"#tup":[]}}}]}},"time":{"#bigint":"345600"}},{"#meta":{"index":5},"action_taken":"withdraw_action","bank":{"#map":[["contract0",{"#map":[["uawesome",{"#bigint":"64"}]]}],["sender1",{"#map":[["uawesome",{"#bigint":"336"}]]}],["sender2",{"#map":[["uawesome",{"#bigint":"200"}]]}],["sender3",{"#map":[["uawesome",{"#bigint":"200"}]]}]]},"contract_state":{"last_id":{"#bigint":"2"},"lockups":{"#map":[]}},"nondet_picks":{"amount":{"tag":"Some","value":{"#bigint":"29"}},"denom":{"tag":"Some","value":"uawesome"},"message_ids":{"tag":"Some","value":[{"#bigint":"1"},{"#bigint":"1"}]},"sender":{"tag":"Some","value":"sender1"}},"result":{"tag":"Ok","value":{"attributes":[{"key":"action","value":{"tag":"FromStr","value":"withdraw"}},{"key":"ids","value":{"tag":"FromListInt","value":[{"#bigint":"1"},{"#bigint":"1"}]}},{"key":"total_amount","value":{"tag":"FromInt","value":{"#bigint":"330"}}}],"data":{"tag":"None","value":{"#tup":[]}},"events":[],"messages":[]}},"time":{"#bigint":"432000"}}]}
\ No newline at end of file
diff --git a/examples/ctf-01/src/bin/schema.rs b/examples/ctf-01/src/bin/schema.rs
new file mode 100644
index 0000000..f328e4d
--- /dev/null
+++ b/examples/ctf-01/src/bin/schema.rs
@@ -0,0 +1 @@
+fn main() {}
diff --git a/examples/ctf-01/src/contract.rs b/examples/ctf-01/src/contract.rs
new file mode 100644
index 0000000..4532e24
--- /dev/null
+++ b/examples/ctf-01/src/contract.rs
@@ -0,0 +1,125 @@
+#[cfg(not(feature = "library"))]
+use cosmwasm_std::entry_point;
+use cosmwasm_std::{
+    to_binary, BankMsg, Binary, Coin, Deps, DepsMut, Env, MessageInfo, Response, StdResult, Uint128,
+};
+
+use crate::error::ContractError;
+use crate::msg::{ExecuteMsg, InstantiateMsg, QueryMsg};
+use crate::state::{Lockup, LAST_ID, LOCKUPS};
+use cw_utils::must_pay;
+
+pub const DENOM: &str = "uawesome";
+pub const MINIMUM_DEPOSIT_AMOUNT: Uint128 = Uint128::new(100);
+pub const LOCK_PERIOD: u64 = 60 * 60 * 24;
+
+#[cfg_attr(not(feature = "library"), entry_point)]
+pub fn instantiate(
+    _deps: DepsMut,
+    _env: Env,
+    _info: MessageInfo,
+    _msg: InstantiateMsg,
+) -> Result<Response, ContractError> {
+    Ok(Response::new().add_attribute("action", "instantiate"))
+}
+
+#[cfg_attr(not(feature = "library"), entry_point)]
+pub fn execute(
+    deps: DepsMut,
+    env: Env,
+    info: MessageInfo,
+    msg: ExecuteMsg,
+) -> Result<Response, ContractError> {
+    match msg {
+        ExecuteMsg::Deposit {} => deposit(deps, env, info),
+        ExecuteMsg::Withdraw { ids } => withdraw(deps, env, info, ids),
+    }
+}
+
+/// Deposit entry point for users
+pub fn deposit(deps: DepsMut, env: Env, info: MessageInfo) -> Result<Response, ContractError> {
+    // check minimum amount and denom
+    let amount = must_pay(&info, DENOM).unwrap();
+
+    if amount < MINIMUM_DEPOSIT_AMOUNT {
+        return Err(ContractError::Unauthorized {});
+    }
+
+    // increment lock id
+    let id = LAST_ID.load(deps.storage).unwrap_or(1);
+    LAST_ID.save(deps.storage, &(id + 1)).unwrap();
+
+    // create lockup
+    let lock = Lockup {
+        id,
+        owner: info.sender,
+        amount,
+        release_timestamp: env.block.time.plus_seconds(LOCK_PERIOD),
+    };
+
+    // save lockup
+    LOCKUPS.save(deps.storage, id, &lock).unwrap();
+
+    Ok(Response::new()
+        .add_attribute("action", "deposit")
+        .add_attribute("id", lock.id.to_string())
+        .add_attribute("owner", lock.owner)
+        .add_attribute("amount", lock.amount)
+        .add_attribute("release_timestamp", lock.release_timestamp.to_string()))
+}
+
+/// Withdrawal entry point for users
+pub fn withdraw(
+    deps: DepsMut,
+    env: Env,
+    info: MessageInfo,
+    ids: Vec<u64>,
+) -> Result<Response, ContractError> {
+    let mut lockups: Vec<Lockup> = vec![];
+    let mut total_amount = Uint128::zero();
+
+    // fetch vaults to process
+    for lockup_id in ids.clone() {
+        let lockup = LOCKUPS.load(deps.storage, lockup_id).unwrap();
+        lockups.push(lockup);
+    }
+
+    for lockup in lockups {
+        // validate owner and time
+        if lockup.owner != info.sender || env.block.time < lockup.release_timestamp {
+            return Err(ContractError::Unauthorized {});
+        }
+
+        // increase total amount
+        total_amount += lockup.amount;
+
+        // remove from storage
+        LOCKUPS.remove(deps.storage, lockup.id);
+    }
+
+    let msg = BankMsg::Send {
+        to_address: info.sender.to_string(),
+        amount: vec![Coin {
+            denom: DENOM.to_string(),
+            amount: total_amount,
+        }],
+    };
+
+    Ok(Response::new()
+        .add_attribute("action", "withdraw")
+        .add_attribute("ids", format!("{:?}", ids))
+        .add_attribute("total_amount", total_amount)
+        .add_message(msg))
+}
+
+#[cfg_attr(not(feature = "library"), entry_point)]
+pub fn query(deps: Deps, _env: Env, msg: QueryMsg) -> StdResult<Binary> {
+    match msg {
+        QueryMsg::GetLockup { id } => to_binary(&get_lockup(deps, id)?),
+    }
+}
+
+/// Returns lockup information for a specified id
+pub fn get_lockup(deps: Deps, id: u64) -> StdResult<Lockup> {
+    Ok(LOCKUPS.load(deps.storage, id).unwrap())
+}
diff --git a/examples/ctf-01/src/error.rs b/examples/ctf-01/src/error.rs
new file mode 100644
index 0000000..dc19f10
--- /dev/null
+++ b/examples/ctf-01/src/error.rs
@@ -0,0 +1,11 @@
+use cosmwasm_std::StdError;
+use thiserror::Error;
+
+#[derive(Error, Debug)]
+pub enum ContractError {
+    #[error("{0}")]
+    Std(#[from] StdError),
+
+    #[error("Unauthorized")]
+    Unauthorized {},
+}
diff --git a/examples/ctf-01/src/integration_tests.rs b/examples/ctf-01/src/integration_tests.rs
new file mode 100644
index 0000000..7a2fe4b
--- /dev/null
+++ b/examples/ctf-01/src/integration_tests.rs
@@ -0,0 +1,108 @@
+#[cfg(test)]
+pub mod tests {
+    use crate::{
+        contract::{DENOM, LOCK_PERIOD, MINIMUM_DEPOSIT_AMOUNT},
+        msg::{ExecuteMsg, InstantiateMsg, QueryMsg},
+        state::Lockup,
+    };
+    use cosmwasm_std::{coin, Addr, Empty, Uint128};
+    use cw_multi_test::{App, Contract, ContractWrapper, Executor};
+
+    pub fn challenge_contract() -> Box<dyn Contract<Empty>> {
+        let contract = ContractWrapper::new(
+            crate::contract::execute,
+            crate::contract::instantiate,
+            crate::contract::query,
+        );
+        Box::new(contract)
+    }
+
+    pub const USER: &str = "user";
+    pub const ADMIN: &str = "admin";
+
+    pub fn proper_instantiate() -> (App, Addr) {
+        let mut app = App::default();
+        let cw_template_id = app.store_code(challenge_contract());
+
+        // init contract
+        let msg = InstantiateMsg { count: 1i32 };
+        let contract_addr = app
+            .instantiate_contract(
+                cw_template_id,
+                Addr::unchecked(ADMIN),
+                &msg,
+                &[],
+                "test",
+                None,
+            )
+            .unwrap();
+
+        // mint funds to contract
+        app = mint_tokens(
+            app,
+            contract_addr.to_string(),
+            MINIMUM_DEPOSIT_AMOUNT * Uint128::new(10),
+        );
+
+        // mint funds to user
+        app = mint_tokens(app, USER.to_string(), MINIMUM_DEPOSIT_AMOUNT);
+
+        // deposit
+        let msg = ExecuteMsg::Deposit {};
+        let sender = Addr::unchecked(USER);
+        app.execute_contract(
+            sender.clone(),
+            contract_addr.clone(),
+            &msg,
+            &[coin(MINIMUM_DEPOSIT_AMOUNT.u128(), DENOM)],
+        )
+        .unwrap();
+
+        // verify no funds
+        let balance = app.wrap().query_balance(USER, DENOM).unwrap().amount;
+        assert_eq!(balance, Uint128::zero());
+
+        (app, contract_addr)
+    }
+
+    pub fn mint_tokens(mut app: App, recipient: String, amount: Uint128) -> App {
+        app.sudo(cw_multi_test::SudoMsg::Bank(
+            cw_multi_test::BankSudo::Mint {
+                to_address: recipient.to_owned(),
+                amount: vec![coin(amount.u128(), DENOM)],
+            },
+        ))
+        .unwrap();
+        app
+    }
+
+    #[test]
+    fn basic_flow() {
+        let (mut app, contract_addr) = proper_instantiate();
+
+        let sender = Addr::unchecked(USER);
+
+        // test query
+        let msg = QueryMsg::GetLockup { id: 1 };
+        let lockup: Lockup = app
+            .wrap()
+            .query_wasm_smart(contract_addr.clone(), &msg)
+            .unwrap();
+        assert_eq!(lockup.amount, MINIMUM_DEPOSIT_AMOUNT);
+        assert_eq!(lockup.owner, sender);
+
+        // fast forward 24 hrs
+        app.update_block(|block| {
+            block.time = block.time.plus_seconds(LOCK_PERIOD);
+        });
+
+        // test withdraw
+        let msg = ExecuteMsg::Withdraw { ids: vec![1] };
+        app.execute_contract(sender, contract_addr, &msg, &[])
+            .unwrap();
+
+        // verify funds received
+        let balance = app.wrap().query_balance(USER, DENOM).unwrap().amount;
+        assert_eq!(balance, MINIMUM_DEPOSIT_AMOUNT);
+    }
+}
diff --git a/examples/ctf-01/src/lib.rs b/examples/ctf-01/src/lib.rs
new file mode 100644
index 0000000..0f32e97
--- /dev/null
+++ b/examples/ctf-01/src/lib.rs
@@ -0,0 +1,7 @@
+pub mod contract;
+mod error;
+pub mod integration_tests;
+pub mod msg;
+pub mod state;
+
+pub use crate::error::ContractError;
diff --git a/examples/ctf-01/src/msg.rs b/examples/ctf-01/src/msg.rs
new file mode 100644
index 0000000..4416dcb
--- /dev/null
+++ b/examples/ctf-01/src/msg.rs
@@ -0,0 +1,21 @@
+use cosmwasm_schema::{cw_serde, QueryResponses};
+
+use crate::state::Lockup;
+
+#[cw_serde]
+pub struct InstantiateMsg {
+    pub count: i32,
+}
+
+#[cw_serde]
+pub enum ExecuteMsg {
+    Deposit {},
+    Withdraw { ids: Vec<u64> },
+}
+
+#[cw_serde]
+#[derive(QueryResponses)]
+pub enum QueryMsg {
+    #[returns(Lockup)]
+    GetLockup { id: u64 },
+}
diff --git a/examples/ctf-01/src/state.rs b/examples/ctf-01/src/state.rs
new file mode 100644
index 0000000..355c277
--- /dev/null
+++ b/examples/ctf-01/src/state.rs
@@ -0,0 +1,18 @@
+use cosmwasm_schema::cw_serde;
+use cosmwasm_std::{Addr, Timestamp, Uint128};
+use cw_storage_plus::{Item, Map};
+
+#[cw_serde]
+pub struct Lockup {
+    /// Unique lockup identifier
+    pub id: u64,
+    /// Owner address
+    pub owner: Addr,
+    /// Locked amount
+    pub amount: Uint128,
+    /// Timestamp when the lockup can be withdrawn
+    pub release_timestamp: Timestamp,
+}
+
+pub const LAST_ID: Item<u64> = Item::new("lock_id");
+pub const LOCKUPS: Map<u64, Lockup> = Map::new("lockups");
diff --git a/examples/ctf-01/tests/mbt_oaksecurity_cosmwasm_ctf_01.rs b/examples/ctf-01/tests/mbt_oaksecurity_cosmwasm_ctf_01.rs
new file mode 100644
index 0000000..a9b308a
--- /dev/null
+++ b/examples/ctf-01/tests/mbt_oaksecurity_cosmwasm_ctf_01.rs
@@ -0,0 +1,277 @@
+pub mod state_structs {
+    use itf::de::{self, As};
+    use num_bigint::BigInt;
+    use serde::Deserialize;
+    use std::collections::HashMap;
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct InstantiateMsg {
+        pub count: BigInt,
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct Lockup {
+        pub id: BigInt,
+        pub owner: String,
+        pub amount: BigInt,
+        pub release_timestamp: BigInt,
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct ContractState {
+        pub last_id: BigInt,
+        pub lockups: HashMap<BigInt, Lockup>,
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct NondetPicks {
+        #[serde(with = "As::<de::Option::<_>>")]
+        pub sender: Option<String>,
+
+        #[serde(with = "As::<de::Option::<_>>")]
+        pub denom: Option<String>,
+
+        #[serde(with = "As::<de::Option::<_>>")]
+        pub amount: Option<BigInt>,
+
+        #[serde(with = "As::<de::Option::<_>>")]
+        pub message_ids: Option<Vec<BigInt>>,
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct Message {}
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct Attribute {
+        pub key: String,
+        pub value: QuintSerializedValue,
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    #[serde(tag = "tag", content = "value")]
+    pub enum QuintSerializedValue {
+        FromInt(BigInt),
+        FromStr(String),
+        FromListInt(Vec<BigInt>),
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct Response {
+        pub messages: Vec<Message>,
+        pub attributes: Vec<Attribute>,
+    }
+
+    #[derive(Clone, Debug, Deserialize)]
+    pub struct State {
+        pub contract_state: ContractState,
+        pub bank: HashMap<String, HashMap<String, BigInt>>,
+        #[serde(with = "As::<de::Result::<_, _>>")]
+        pub result: Result<Response, String>,
+        pub action_taken: String,
+        pub nondet_picks: NondetPicks,
+        pub time: BigInt,
+    }
+}
+
+#[cfg(test)]
+pub mod tests {
+    use oaksecurity_cosmwasm_ctf_01::contract;
+    use oaksecurity_cosmwasm_ctf_01::msg::{ExecuteMsg, InstantiateMsg};
+
+    use crate::state_structs::*;
+    use cosmwasm_std::{coin, Addr, Uint128};
+    use cw_multi_test::{App, AppResponse, ContractWrapper, Executor};
+    use itf::trace_from_str;
+    use num_bigint::BigInt;
+    use num_traits::{ToPrimitive, Zero};
+
+    pub const DENOM: &str = "uawesome";
+    pub const TICK: u64 = contract::LOCK_PERIOD;
+
+    pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App {
+        app.sudo(cw_multi_test::SudoMsg::Bank(
+            cw_multi_test::BankSudo::Mint {
+                to_address: recipient.to_owned(),
+                amount: vec![coin(amount.u128(), denom)],
+            },
+        ))
+        .unwrap();
+        app
+    }
+
+    fn compare_state(test_state: &TestState, app: &App, state: &State) {
+        // compare contract balances
+        let balance = app
+            .wrap()
+            .query_balance(&test_state.contract_addr, DENOM)
+            .unwrap()
+            .amount;
+        let trace_balance = state
+            .bank
+            .get(&test_state.contract_addr.to_string())
+            .and_then(|x| x.get(DENOM))
+            .and_then(|x| x.to_u128())
+            .unwrap_or(0);
+        println!(
+            "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}",
+            test_state.contract_addr,
+            balance,
+            Uint128::new(trace_balance)
+        );
+        assert_eq!(balance, Uint128::new(trace_balance));
+
+        // TODO: Query the contract and compare the state as you wish
+    }
+
+    fn compare_result(
+        trace_result: Result<Response, String>,
+        app_result: Result<AppResponse, anyhow::Error>,
+    ) {
+        if trace_result.is_ok() {
+            assert!(
+                app_result.is_ok(),
+                "Action unexpectedly failed, error: {:?}",
+                app_result.err()
+            );
+            println!("Action successful as expected");
+        } else {
+            assert!(
+                app_result.is_err(),
+                "Expected action to fail with error: {:?}",
+                trace_result.err()
+            );
+            println!("Action failed as expected");
+        }
+    }
+
+    fn funds_from_trace(amount: Option<BigInt>, denom: Option<String>) -> Vec<cosmwasm_std::Coin> {
+        if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) {
+            return vec![];
+        }
+
+        vec![coin(
+            amount.as_ref().unwrap().to_u128().unwrap(),
+            denom.unwrap(),
+        )]
+    }
+
+    // Testing is stateful.
+    struct TestState {
+        // we will only know the contract address once we have processed an `instantiate` step
+        pub contract_addr: Addr,
+    }
+
+    #[test]
+    fn model_test() {
+        let mut app = App::default();
+        let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query);
+        let code_id = app.store_code(Box::new(code));
+
+        // create test state
+        let mut test_state = TestState {
+            contract_addr: Addr::unchecked("contract0"),
+        };
+
+        // load trace data
+        let data = include_str!("../quint/test.itf.json");
+        let trace: itf::Trace<State> = trace_from_str(data).unwrap();
+
+        for s in trace.states {
+            let last_result = s.value.result.clone();
+            if last_result.is_ok() && !last_result.unwrap().messages.is_empty() {
+                println!("Processing messages, skipping");
+                continue;
+            }
+
+            let action_taken = &s.value.action_taken;
+            let nondet_picks = &s.value.nondet_picks;
+            let amount = nondet_picks.amount.clone();
+            let denom = nondet_picks.denom.clone();
+            let sender = nondet_picks.sender.clone();
+
+            println!("Step number: {:?}", s.meta.index);
+            println!("Result from trace: {:?}", s.value.result.clone());
+
+            match action_taken.as_str() {
+                "deposit_action" => {
+                    let sender = Addr::unchecked(sender.unwrap());
+                    let funds = funds_from_trace(amount, denom);
+
+                    let msg = ExecuteMsg::Deposit {};
+                    println!("Message: {:?}", msg);
+                    println!("Sender: {:?}", sender);
+                    println!("Funds: {:?}", funds);
+
+                    let res = app.execute_contract(
+                        sender,
+                        test_state.contract_addr.clone(),
+                        &msg,
+                        &funds,
+                    );
+
+                    compare_result(s.value.result.clone(), res)
+                }
+
+                "q::init" => {
+                    println!("Initializing contract.");
+
+                    let sender = Addr::unchecked(sender.unwrap());
+                    let funds = funds_from_trace(amount, denom);
+
+                    let msg = InstantiateMsg { count: 0 };
+                    println!("Message: {:?}", msg);
+                    println!("Sender: {:?}", sender);
+                    println!("Funds: {:?}", funds);
+
+                    test_state.contract_addr = app
+                        .instantiate_contract(code_id, sender, &msg, &funds, "test", None)
+                        .unwrap();
+
+                    for (addr, coins) in s.value.bank.clone().iter() {
+                        for (denom, amount) in coins.iter() {
+                            app = mint_tokens(
+                                app,
+                                addr.clone(),
+                                denom.to_string(),
+                                Uint128::new(amount.to_u128().unwrap()),
+                            );
+                        }
+                    }
+                }
+
+                "withdraw_action" => {
+                    let sender = Addr::unchecked(sender.unwrap());
+                    let funds = funds_from_trace(amount, denom);
+
+                    let message_ids = nondet_picks
+                        .message_ids
+                        .clone()
+                        .unwrap()
+                        .iter()
+                        .map(|x| x.to_u64().unwrap().into())
+                        .collect();
+                    let msg = ExecuteMsg::Withdraw { ids: message_ids };
+                    println!("Message: {:?}", msg);
+                    println!("Sender: {:?}", sender);
+                    println!("Funds: {:?}", funds);
+
+                    let res = app.execute_contract(
+                        sender,
+                        test_state.contract_addr.clone(),
+                        &msg,
+                        &funds,
+                    );
+
+                    compare_result(s.value.result.clone(), res)
+                }
+
+                _ => panic!("Invalid action taken"),
+            }
+            compare_state(&test_state, &app, &(s.value.clone()));
+            println!("clock is advancing for {} seconds", TICK);
+            app.update_block(|block| {
+                block.time = block.time.plus_seconds(TICK);
+            });
+            println!("-----------------------------------");
+        }
+    }
+}