diff --git a/Code/itf/Cargo.toml b/Code/itf/Cargo.toml
new file mode 100644
index 000000000..6eb9dbf28
--- /dev/null
+++ b/Code/itf/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "malachite-itf"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+itf = "0.1.0"
+serde = { version = "1.0.189", features = ["derive"] }
diff --git a/Code/itf/fixtures/0DecideNonProposerTest.itf.json b/Code/itf/fixtures/0DecideNonProposerTest.itf.json
new file mode 100644
index 000000000..86e3eb499
--- /dev/null
+++ b/Code/itf/fixtures/0DecideNonProposerTest.itf.json
@@ -0,0 +1,1781 @@
+{
+  "#meta": {
+    "format": "ITF",
+    "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html",
+    "source": "consensus.qnt",
+    "status": "passed",
+    "description": "Created by Quint on Wed Oct 25 2023 15:38:28 GMT+0200 (Central European Summer Time)",
+    "timestamp": "1698241108633"
+  },
+  "vars": [
+    "system",
+    "_Event",
+    "_Result"
+  ],
+  "states": [
+    {
+      "#meta": {
+        "index": 0
+      },
+      "_Event": {
+        "height": -1,
+        "name": "Initial",
+        "round": -1,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "newRound",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 1
+      },
+      "_Event": {
+        "height": 1,
+        "name": "NewRound",
+        "round": 0,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPropose",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 2
+      },
+      "_Event": {
+        "height": 1,
+        "name": "NewRound",
+        "round": 0,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPropose",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 3
+      },
+      "_Event": {
+        "height": 1,
+        "name": "Proposal",
+        "round": 0,
+        "value": "block",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 1,
+          "id": "block",
+          "round": 0,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 4
+      },
+      "_Event": {
+        "height": 1,
+        "name": "Proposal",
+        "round": 0,
+        "value": "block",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 1,
+          "id": "block",
+          "round": 0,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 5
+      },
+      "_Event": {
+        "height": 1,
+        "name": "ProposalAndPolkaAndValid",
+        "round": 0,
+        "value": "block",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 1,
+          "id": "block",
+          "round": 0,
+          "src": "Josef",
+          "step": "precommit"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": 0,
+              "lockedValue": "block",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": 0,
+              "validValue": "block"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 6
+      },
+      "_Event": {
+        "height": 1,
+        "name": "ProposalAndPolkaAndValid",
+        "round": 0,
+        "value": "block",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 1,
+          "id": "block",
+          "round": 0,
+          "src": "Josef",
+          "step": "precommit"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": 0,
+              "lockedValue": "block",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": 0,
+              "validValue": "block"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 7
+      },
+      "_Event": {
+        "height": 1,
+        "name": "ProposalAndCommitAndValid",
+        "round": 0,
+        "value": "block",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "block",
+        "name": "decided",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": 0,
+              "lockedValue": "block",
+              "p": "Josef",
+              "round": 0,
+              "step": "decided",
+              "validRound": 0,
+              "validValue": "block"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 8
+      },
+      "_Event": {
+        "height": 1,
+        "name": "ProposalAndCommitAndValid",
+        "round": 0,
+        "value": "block",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "block",
+        "name": "decided",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 1,
+              "lockedRound": 0,
+              "lockedValue": "block",
+              "p": "Josef",
+              "round": 0,
+              "step": "decided",
+              "validRound": 0,
+              "validValue": "block"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 9
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewHeight",
+        "round": 0,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "newRound",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 10
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewHeight",
+        "round": 0,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "newRound",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 11
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewRoundProposer",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "proposal",
+        "proposal": {
+          "height": 2,
+          "proposal": "nextBlock",
+          "round": 0,
+          "src": "Josef",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 12
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewRoundProposer",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "proposal",
+        "proposal": {
+          "height": 2,
+          "proposal": "nextBlock",
+          "round": 0,
+          "src": "Josef",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 13
+      },
+      "_Event": {
+        "height": 2,
+        "name": "Proposal",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nextBlock",
+          "round": 0,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 14
+      },
+      "_Event": {
+        "height": 2,
+        "name": "Proposal",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nextBlock",
+          "round": 0,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 15
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PolkaAny",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPrevote",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 16
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PolkaAny",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPrevote",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 17
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPrevote",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 0,
+          "src": "Josef",
+          "step": "precommit"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 18
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPrevote",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 0,
+          "src": "Josef",
+          "step": "precommit"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 19
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PrecommitAny",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPrecommit",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 20
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PrecommitAny",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPrecommit",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 21
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPrecommit",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "skipRound",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": 1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 22
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPrecommit",
+        "round": 0,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "skipRound",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": 1,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 0,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 23
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewRound",
+        "round": 1,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPropose",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 24
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewRound",
+        "round": 1,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPropose",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 25
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPropose",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 1,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 26
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPropose",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 1,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 27
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PolkaNil",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 1,
+          "src": "Josef",
+          "step": "precommit"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 28
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PolkaNil",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 1,
+          "src": "Josef",
+          "step": "precommit"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 29
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PrecommitAny",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPrecommit",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 30
+      },
+      "_Event": {
+        "height": 2,
+        "name": "PrecommitAny",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPrecommit",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 31
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPrecommit",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "skipRound",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": 2,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 32
+      },
+      "_Event": {
+        "height": 2,
+        "name": "TimeoutPrecommit",
+        "round": 1,
+        "value": "nextBlock",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "skipRound",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": 2,
+        "timeout": "",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 1,
+              "step": "precommit",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 33
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewRound",
+        "round": 2,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPropose",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 2,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 34
+      },
+      "_Event": {
+        "height": 2,
+        "name": "NewRound",
+        "round": 2,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "timeout",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "timeoutPropose",
+        "voteMessage": {
+          "height": -1,
+          "id": "",
+          "round": -1,
+          "src": "",
+          "step": ""
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 2,
+              "step": "propose",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    },
+    {
+      "#meta": {
+        "index": 35
+      },
+      "_Event": {
+        "height": 2,
+        "name": "ProposalInvalid",
+        "round": 2,
+        "value": "",
+        "vr": -1
+      },
+      "_Result": {
+        "decided": "",
+        "name": "votemessage",
+        "proposal": {
+          "height": -1,
+          "proposal": "",
+          "round": -1,
+          "src": "",
+          "validRound": -1
+        },
+        "skipRound": -1,
+        "timeout": "",
+        "voteMessage": {
+          "height": 2,
+          "id": "nil",
+          "round": 2,
+          "src": "Josef",
+          "step": "prevote"
+        }
+      },
+      "system": {
+        "#map": [
+          [
+            "Josef",
+            {
+              "height": 2,
+              "lockedRound": -1,
+              "lockedValue": "nil",
+              "p": "Josef",
+              "round": 2,
+              "step": "prevote",
+              "validRound": -1,
+              "validValue": "nil"
+            }
+          ]
+        ]
+      }
+    }
+  ]
+}
diff --git a/Code/itf/src/deserializers.rs b/Code/itf/src/deserializers.rs
new file mode 100644
index 000000000..97d975e6b
--- /dev/null
+++ b/Code/itf/src/deserializers.rs
@@ -0,0 +1,52 @@
+use serde::de::IntoDeserializer;
+use serde::Deserialize;
+
+use crate::{Proposal, VoteMessage};
+
+pub(crate) fn empty_string_as_none<'de, D, T>(de: D) -> Result<Option<T>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+    T: serde::Deserialize<'de>,
+{
+    let opt = Option::<String>::deserialize(de)?;
+    match opt.as_deref() {
+        None | Some("") => Ok(None),
+        Some(s) => T::deserialize(s.into_deserializer()).map(Some),
+    }
+}
+
+pub(crate) fn minus_one_as_none<'de, D, T>(de: D) -> Result<Option<T>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+    T: serde::Deserialize<'de>,
+{
+    let opt = Option::<i64>::deserialize(de)?;
+    match opt {
+        None | Some(-1) => Ok(None),
+        Some(i) => T::deserialize(i.into_deserializer()).map(Some),
+    }
+}
+
+pub(crate) fn proposal_or_none<'de, D>(de: D) -> Result<Option<Proposal>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+{
+    let proposal = Proposal::deserialize(de)?;
+    if proposal.is_empty() {
+        Ok(None)
+    } else {
+        Ok(Some(proposal))
+    }
+}
+
+pub(crate) fn vote_message_or_none<'de, D>(de: D) -> Result<Option<VoteMessage>, D::Error>
+where
+    D: serde::Deserializer<'de>,
+{
+    let vote_message = VoteMessage::deserialize(de)?;
+    if vote_message.is_empty() {
+        Ok(None)
+    } else {
+        Ok(Some(vote_message))
+    }
+}
diff --git a/Code/itf/src/lib.rs b/Code/itf/src/lib.rs
new file mode 100644
index 000000000..0d87fa496
--- /dev/null
+++ b/Code/itf/src/lib.rs
@@ -0,0 +1,178 @@
+use itf::ItfMap;
+use serde::Deserialize;
+
+mod deserializers;
+use deserializers as de;
+
+pub type Address = String;
+pub type Value = String;
+pub type Step = String;
+pub type Round = i64;
+pub type Height = i64;
+
+#[derive(Clone, Debug, Deserialize)]
+pub enum Timeout {
+    #[serde(rename = "timeoutPrevote")]
+    Prevote,
+
+    #[serde(rename = "timeoutPrecommit")]
+    Precommit,
+
+    #[serde(rename = "timeoutPropose")]
+    Propose,
+}
+
+#[derive(Clone, Debug, Deserialize)]
+pub struct ItfState {
+    pub system: System,
+
+    #[serde(rename = "_Event")]
+    pub event: Event,
+
+    #[serde(rename = "_Result")]
+    pub result: Result,
+}
+
+#[derive(Clone, Debug, Deserialize)]
+pub struct System(ItfMap<Address, ConsensusState>);
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(tag = "name")]
+pub enum Event {
+    Initial,
+    NewRound {
+        height: Height,
+        round: Round,
+    },
+    Proposal {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    ProposalAndPolkaAndValid {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    ProposalAndCommitAndValid {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    NewHeight {
+        height: Height,
+        round: Round,
+    },
+    NewRoundProposer {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    PolkaNil {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    PolkaAny {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    PrecommitAny {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    TimeoutPrevote {
+        height: Height,
+        round: Round,
+    },
+    TimeoutPrecommit {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    TimeoutPropose {
+        height: Height,
+        round: Round,
+        value: Value,
+    },
+    ProposalInvalid {
+        height: Height,
+        round: Round,
+    },
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct Result {
+    pub name: String,
+    #[serde(deserialize_with = "de::proposal_or_none")]
+    pub proposal: Option<Proposal>,
+    #[serde(deserialize_with = "de::vote_message_or_none")]
+    pub vote_message: Option<VoteMessage>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub timeout: Option<Timeout>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub decided: Option<Value>,
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub skip_round: Option<Round>,
+}
+
+#[derive(Clone, Debug, Deserialize, PartialEq, Eq)]
+#[serde(rename_all = "camelCase")]
+pub struct Proposal {
+    pub src: Address,
+    pub height: Height,
+    pub round: Round,
+    pub proposal: Value,
+    pub valid_round: Round,
+}
+
+impl Proposal {
+    pub fn is_empty(&self) -> bool {
+        self.src.is_empty()
+            && self.proposal.is_empty()
+            && self.height == -1
+            && self.round == -1
+            && self.valid_round == -1
+    }
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct VoteMessage {
+    pub src: Address,
+    pub height: Height,
+    pub round: Round,
+    pub step: Step,
+    pub id: Value,
+}
+
+impl VoteMessage {
+    pub fn is_empty(&self) -> bool {
+        self.src.is_empty()
+            && self.id.is_empty()
+            && self.height == -1
+            && self.round == -1
+            && self.step.is_empty()
+    }
+}
+
+#[derive(Clone, Debug, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct ConsensusState {
+    pub p: Address,
+    pub height: Height,
+    pub round: Round,
+    pub step: Step,
+
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub locked_round: Option<Round>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub locked_value: Option<Value>,
+    #[serde(deserialize_with = "de::minus_one_as_none")]
+    pub valid_round: Option<Round>,
+    #[serde(deserialize_with = "de::empty_string_as_none")]
+    pub valid_value: Option<Value>,
+}
diff --git a/Code/itf/tests/decide_non_proposer.rs b/Code/itf/tests/decide_non_proposer.rs
new file mode 100644
index 000000000..d0baa0cf6
--- /dev/null
+++ b/Code/itf/tests/decide_non_proposer.rs
@@ -0,0 +1,9 @@
+use malachite_itf::ItfState;
+
+const FIXTURE_JSON: &str = include_str!("../fixtures/0DecideNonProposerTest.itf.json");
+
+#[test]
+fn parse_fixture() {
+    let state = itf::trace_from_str::<ItfState>(FIXTURE_JSON).unwrap();
+    dbg!(state);
+}