test(mbt): Add Model Based Test for Emerald

This patch connects the newly added Quint specs to Emerald's code via
the Quint Connect library.

Author: erickpintor

.github/workflows/test.yml

@@ -8,6 +8,7 @@ on:
 
 permissions:
   contents: read
+  packages: read
 
 # If new code is pushed to a PR branch, then cancel in progress workflows for that PR.
 # Ensures that we don't waste CI time, and returns results quicker.
@@ -23,6 +24,7 @@ env:
   RUST_BACKTRACE: short
   CARGO_NET_RETRY: 10
   RUSTUP_MAX_RETRIES: 10
+  QUINT_VERBOSE: 1
 
 jobs:
   unit:
@@ -57,11 +59,62 @@ jobs:
       - name: Run Forge build
         run: forge build
         if: steps.filter.outputs.code == 'true'
-      - name: Run tests
+      - name: Run unit tests
         run: |
           cargo nextest run \
             --workspace \
             --all-features \
             --no-fail-fast \
-            --failure-output final
+            --failure-output final \
+            --filterset 'not package(emerald-mbt)'
+        if: steps.filter.outputs.code == 'true'
+
+  mbt:
+    name: MBT Tests
+    runs-on: ubuntu-latest
+    # XXX: Do not block on MBT initially until we gain confidence CI is not
+    # flaky for any reason.
+    continue-on-error: true
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v5
+        with:
+          submodules: recursive
+      - id: filter
+        uses: dorny/paths-filter@v3
+        with:
+          filters: |
+            code:
+              - '**/*.rs'
+              - '**/*.qnt'
+              - 'Makefile'
+              - '**/Cargo.toml'
+              - '**/Cargo.lock'
+              - '**/*.sh'
+              - '*/workflows/test.yml'
+      - name: Setup Node.js
+        uses: actions/setup-node@v4
+        with:
+          node-version: '22'
+      - name: Install Quint
+        run: npm install -g @informalsystems/quint
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+      - name: Install Protoc
+        uses: arduino/setup-protoc@v3
+        with:
+          repo-token: ${{ secrets.GITHUB_TOKEN }}
+      - name: Setup Rust toolchain
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+      - name: Run Forge build
+        run: forge build
+        if: steps.filter.outputs.code == 'true'
+      - name: Run MBT tests
+        run: make mbt-test
         if: steps.filter.outputs.code == 'true'

Cargo.lock

@@ -7,6 +7,7 @@ members = [
   "engine",
   "utils",
   "types",
+  "tests/mbt",
 ]
 
 [workspace.package]

Cargo.toml

@@ -1,4 +1,4 @@
-.PHONY: all build release test docs docs-serve testnet-config testnet-reth-recreate testnet-reth-restart testnet-start sync testnet-node-stop testnet-node-restart testnet-stop testnet-clean clean-volumes clean-prometheus spam spam-contract
+.PHONY: all build release test docs docs-serve testnet-config testnet-reth-recreate testnet-reth-restart testnet-start sync testnet-node-stop testnet-node-restart testnet-stop testnet-clean clean-volumes clean-prometheus spam spam-contract mbt-test mbt-clean
 
 all: build
 
@@ -12,7 +12,7 @@ release:
 	cargo build --release
 
 test:
-	cargo test
+	cargo test --workspace --exclude emerald-mbt
 	forge test -vvv
 
 # Docs
@@ -107,3 +107,15 @@ spam-contract:
 		--time=60 \
 		--rate=1000 \
 		--rpc-url=127.0.0.1:8645
+
+# Model-Based Testing (MBT)
+
+TEST ?=
+
+mbt-test: RETH_NODES=reth0 reth1 reth2
+mbt-test: testnet-config
+	@echo "Running MBT tests..."
+	@echo "Note: RETH will be automatically started and stopped for each test"
+	cargo test --package emerald-mbt -- --nocapture --test-threads=1 $(TEST)
+
+mbt-clean: testnet-clean

Makefile

@@ -0,0 +1,25 @@
+[package]
+name    = "emerald-mbt"
+version = { workspace = true }
+edition = { workspace = true }
+publish = false
+
+[lints]
+workspace = true
+
+[dependencies]
+emerald                     = { workspace = true }
+malachitebft-eth-types      = { workspace = true }
+malachitebft-eth-engine     = { workspace = true }
+malachitebft-eth-cli        = { workspace = true }
+malachitebft-app-channel    = { workspace = true }
+malachitebft-core-consensus = { workspace = true }
+
+serde = { workspace = true }
+itf   = { workspace = true }
+tokio = { workspace = true }
+
+quint-connect = "0.1"
+anyhow        = "1.0"
+bimap         = "0.6.3"
+tempfile      = "3.23.0"