This repo contains materials for the "CosmWasm Contract Security: Practical Formal Methods with Quint" workshop held at AwesomWasm 2024.

Pre-Workshop

Let's install the software useful for coding along in the workshop.

1. Install Quint

Run npm i @informalsystems/quint -g

Check that Quint is installed by running quint --version. (The version at the time of AwesomWasm is 0.20.0.)

2. Install the VSCode plugin

This plugin provides language support for Quint inside VSCode: syntax highlighting, typechecking, and similar.

In the VSCode go to Extensions (Ctrl+Shift+x or Cmd+Shift+x) and search for "Quint". You will find the Quint extension by Informal Sytems.

For other editors, see instructions here.

3. Install the ITF Trace Viewer plugin

This plugin helps visualizing Quint-produced traces.

Go to Extensions and search for "ITF Trace Viewer". There will be an extension of that name by Informal Systems.

Happy modeling with Quint :)

For the impatient

If you want to try out Quint before the workshop, have a look at Quint tutorials.

Useful Resources for During the Hackathon

• Quint Cheatsheet
• REPL Tutorial
• Example Quint Models
• cosmwasm-to-quint

Workshop Examples

For a detailed walkthrough through the CTF-01 example showed in the workshop, go through walkthrough.md