MESH2/docs/specs/MESH-Dev-Environment-Specification.md

MESH PROTOCOL

Development Environment Specification

Toolchains, Images, and Setup for VM-Based Development

Version 1.0 | March 2026

1. Overview

This document specifies the complete development environment for the MESH protocol reference implementation. It is designed for a single developer working in a virtual machine environment, using official Docker images and standard package managers wherever possible.

The environment is structured as a primary development VM running Docker, with containerised toolchains for build, test, and formal verification. This ensures reproducibility: any developer on any host OS can recreate the identical environment from this document.

1.1 Host VM Requirements

---

Requirement Specification

Operating System Ubuntu 24.04 LTS (Noble Numbat), server or desktop edition. This is the reference OS. All commands in this document assume Ubuntu 24.04. Other Linux distributions will work but package names may differ.

Architecture x86_64 (amd64). ARM64 (aarch64) is supported but some Docker images may require emulation. All specified images have amd64 variants.

CPU Minimum: 4 cores. Recommended: 8+ cores. Rust compilation and TLA+ model checking are both CPU-intensive.

RAM Minimum: 8 GB. Recommended: 16 GB. The TLC model checker is a JVM application and benefits from large heap sizes. Rust's linker (mold/lld) also benefits from available RAM.

Disk Minimum: 50 GB free. Recommended: 100 GB. Rust's target/ directory grows quickly. Docker images consume 5--10 GB. The cargo registry cache uses 1--5 GB.

Network Internet access required for initial setup (pulling images, crates). Subsequent development can be done offline if all dependencies are vendored.

---

1.2 Environment Architecture

The development environment consists of three layers:

• Layer 1 --- Host VM: Ubuntu 24.04 with Docker Engine, Git, and an editor (VS Code or Neovim). This is where you write code and run docker compose commands.

• Layer 2 --- Build Container: Official Rust Docker image with additional system dependencies. This is where Rust code compiles. Mounted as a volume so source files live on the host.

• Layer 3 --- Auxiliary Containers: TLA+ tools, Tamarin Prover, and the multi-validator testnet. These run as separate Docker containers orchestrated by docker compose.

2. Host VM Setup

2.1 Base Packages

Install the following packages on the host VM. These are all available from Ubuntu's default APT repositories.

sudo apt update && sudo apt upgrade -y

sudo apt install -y \

build-essential pkg-config libssl-dev \

git curl wget ca-certificates \

docker.io docker-compose-v2 \

jq tmux htop \

clang lld mold

---

Package Version Purpose

docker.io ≥24.0 Container runtime. Ubuntu's official Docker package. Alternatively install Docker CE from docker.com --- both work.

docker-compose-v2 ≥2.24 Multi-container orchestration for the testnet and auxiliary tools. Uses the docker compose (v2, no hyphen) syntax.

git ≥2.43 Version control. Standard.

build-essential current GCC, make, libc headers. Needed for some Rust crate build scripts that compile C code.

pkg-config current Helps Rust crates find system libraries (e.g., OpenSSL headers).

libssl-dev current OpenSSL development headers. Required by the quinn QUIC library for TLS 1.3.

clang ≥17 Alternative C/C++ compiler. Some crates prefer clang for cross-compilation.

lld ≥17 LLVM linker. Faster than GNU ld for large Rust binaries.

mold ≥2.4 Even faster linker than lld. Recommended for development builds. Set via .cargo/config.toml.

jq current JSON processor. Useful for parsing benchmark output and test vectors.

tmux current Terminal multiplexer. You will want multiple panes when running 4 validators.

---

2.2 Docker Post-Install

Add your user to the docker group so you can run Docker without sudo:

sudo usermod -aG docker $USER

newgrp docker # apply group change without logout

docker run hello-world # verify it works

2.3 Rust Toolchain (Host-Native)

While compilation happens inside Docker containers for reproducibility, you will also want a native Rust installation on the host for IDE integration (rust-analyzer), quick cargo check cycles, and running individual tests without the container overhead.

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y \

--default-toolchain stable \

--profile default \

--component rust-analyzer clippy rustfmt

source "$HOME/.cargo/env"

rustup --version # verify: rustup 1.28+

cargo --version # verify: cargo 1.85+

rustc --version # verify: rustc 1.85+

Pin the Rust version in the project root to ensure all developers and CI use the same compiler:

# In the project root, create rust-toolchain.toml:

[toolchain]

channel = "1.85.0"

components = ["clippy", "rustfmt", "rust-analyzer"]

targets = ["x86_64-unknown-linux-gnu"]

2.4 Cargo Configuration

Create .cargo/config.toml in the project root to set the fast linker and compilation flags:

# .cargo/config.toml

[target.x86_64-unknown-linux-gnu]

linker = "clang"

rustflags = ["-C", "link-arg=-fuse-ld=mold"]

[build]

# Use all available cores for compilation

jobs = 0

[profile.dev]

# Speed up dev builds at the cost of optimisation

opt-level = 0

debug = true

[profile.test]

opt-level = 1 # Some crypto tests are too slow at opt-level 0

[profile.release]

opt-level = 3

lto = "thin"

codegen-units = 1

strip = true

WHY mold?: The default GNU linker (ld) can take 5--15 seconds to link a medium-sized Rust binary. mold reduces this to under 1 second. Over hundreds of compile-test cycles per day, this saves hours of cumulative wait time. It is the single highest-impact developer experience improvement.

2.5 Editor / IDE

Either of the following is fully supported:

• VS Code + rust-analyzer extension: Install via the Extensions marketplace. rust-analyzer provides inline type hints, go-to-definition, auto-completion, and integrated test running. Add the Even Better TOML extension for Cargo.toml editing.

• Neovim + rust-analyzer via nvim-lspconfig: If you prefer terminal-based editing. Requires Neovim 0.9+ and the nvim-lspconfig plugin configured for rust_analyzer.

Whichever editor you choose, ensure it is configured to run rustfmt on save. The project enforces formatting via CI --- unformatted code will be rejected.

3. Docker Images

All containerised toolchains use official images from Docker Hub or well-established community images. No custom base images. Every image is pinned to a specific tag for reproducibility.

3.1 Image Registry

---

Image Tag (pinned) Purpose

docker.io/library/rust 1.85.0-bookworm Primary build image. Debian Bookworm base with full Rust toolchain. Used for compiling all MESH crates. ~1.4 GB.

docker.io/library/rust 1.85.0-slim-bookworm Slim build variant. No GCC, no man pages. Used for CI builds where image pull time matters. ~800 MB.

docker.io/library/debian bookworm-slim Runtime base image. For the final validator and wallet binaries. Minimal: ~80 MB.

docker.io/library/eclipse-temurin 21-jre-jammy Java 21 runtime for TLA+ tools (TLC model checker, SANY parser). Eclipse Temurin is the official successor to AdoptOpenJDK. ~220 MB.

ghcr.io/tamarin-prover/tamarin-prover 1.8.0 Tamarin Prover for cryptographic protocol verification. Official GitHub Container Registry image.

docker.io/library/python 3.12-slim-bookworm Python runtime for test vector generation scripts, benchmarking scripts, and the Jupyter-based TLA+ environment. ~150 MB.

docker.io/jupyter/minimal-notebook latest Jupyter notebook environment for interactive TLA+ specification development using tlaplus-jupyter kernel. ~1.2 GB.

---

3.2 Pull All Images

Run the following to pre-fetch all images. This will consume approximately 5 GB of disk space and takes 5--15 minutes depending on bandwidth.

docker pull rust:1.85.0-bookworm

docker pull rust:1.85.0-slim-bookworm

docker pull debian:bookworm-slim

docker pull eclipse-temurin:21-jre-jammy

docker pull ghcr.io/tamarin-prover/tamarin-prover:1.8.0

docker pull python:3.12-slim-bookworm

docker pull jupyter/minimal-notebook:latest

3.3 Build Container (Dockerfile.build)

This Dockerfile extends the official Rust image with the additional system libraries and tools needed to compile MESH crates:

# Dockerfile.build

FROM rust:1.85.0-bookworm

# System dependencies for crypto crates and QUIC

RUN apt-get update && apt-get install -y --no-install-recommends \

pkg-config libssl-dev clang lld mold \

cmake \ # some crates need cmake

&& rm -rf /var/lib/apt/lists/*

# Install additional Rust tools

RUN rustup component add clippy rustfmt rust-analyzer

RUN cargo install cargo-audit cargo-deny cargo-nextest

# cargo-nextest: faster test runner with better output

# cargo-audit: checks dependencies for known vulnerabilities

# cargo-deny: checks licenses and advisories

WORKDIR /workspace

VOLUME /workspace

Build and tag it:

docker build -f Dockerfile.build -t mesh-build:latest .

Usage --- compile the project inside the container with host source mounted:

docker run --rm -v $(pwd):/workspace -v cargo-cache:/usr/local/cargo/registry \

mesh-build:latest cargo build

# Run tests:

docker run --rm -v $(pwd):/workspace -v cargo-cache:/usr/local/cargo/registry \

mesh-build:latest cargo nextest run

# Run clippy:

docker run --rm -v $(pwd):/workspace -v cargo-cache:/usr/local/cargo/registry \

mesh-build:latest cargo clippy -- -D warnings

CARGO CACHE VOLUME: The -v cargo-cache:/usr/local/cargo/registry flag creates a named Docker volume that persists the cargo registry cache across container runs. Without this, every docker run would re-download all crates. The volume survives container restarts and typically grows to 1--3 GB.

3.4 Runtime Container (Dockerfile.runtime)

The runtime image is minimal. It contains only the compiled binary and its runtime dependencies. This is what the testnet validators run.

# Dockerfile.runtime

FROM debian:bookworm-slim

RUN apt-get update && apt-get install -y --no-install-recommends \

ca-certificates libssl3 \

&& rm -rf /var/lib/apt/lists/*

COPY --from=builder /workspace/target/release/mesh-validator /usr/local/bin/

COPY --from=builder /workspace/target/release/mesh-wallet /usr/local/bin/

EXPOSE 4430/udp # QUIC port for validator

EXPOSE 4431/udp # QUIC port for client connections

ENTRYPOINT ["mesh-validator"]

This uses a multi-stage build. The full Dockerfile combines Dockerfile.build and Dockerfile.runtime:

# Dockerfile (multi-stage)

FROM rust:1.85.0-bookworm AS builder

RUN apt-get update && apt-get install -y --no-install-recommends \

pkg-config libssl-dev clang lld mold cmake \

&& rm -rf /var/lib/apt/lists/*

WORKDIR /workspace

COPY . .

RUN cargo build --release

FROM debian:bookworm-slim

RUN apt-get update && apt-get install -y --no-install-recommends \

ca-certificates libssl3 && rm -rf /var/lib/apt/lists/*

COPY --from=builder /workspace/target/release/mesh-validator /usr/local/bin/

COPY --from=builder /workspace/target/release/mesh-wallet /usr/local/bin/

EXPOSE 4430/udp 4431/udp

ENTRYPOINT ["mesh-validator"]

4. Formal Verification Toolchains

4.1 TLA+ (TLC Model Checker)

TLA+ is used to formally verify the consensus protocol properties (SPEC-010 §10.6). The TLC model checker is a Java application distributed as a JAR file.

4.1.1 Setup via Docker

There is no single official TLA+ Docker image on Docker Hub. The recommended approach is a lightweight custom image based on Eclipse Temurin JRE:

# Dockerfile.tlaplus

FROM eclipse-temurin:21-jre-jammy

# Download TLA+ tools JAR from official GitHub releases

ARG TLAPLUS_VERSION=1.8.0

RUN apt-get update && apt-get install -y --no-install-recommends wget && \

wget -q https://github.com/tlaplus/tlaplus/releases/download/v${TLAPLUS_VERSION}/tla2tools.jar \

-O /opt/tla2tools.jar && \

apt-get remove -y wget && apt-get autoremove -y && \

rm -rf /var/lib/apt/lists/*

WORKDIR /specs

VOLUME /specs

# Convenience aliases as entrypoints

# Usage: docker run mesh-tlaplus tlc MySpec.tla

ENTRYPOINT ["java", "-cp", "/opt/tla2tools.jar"]

CMD ["tlc2.TLC", "-help"]

Build and use:

docker build -f Dockerfile.tlaplus -t mesh-tlaplus:latest .

# Parse a spec:

docker run --rm -v $(pwd)/specs:/specs mesh-tlaplus:latest \

tla2sany.SANY /specs/Tier1.tla

# Run the model checker:

docker run --rm -v $(pwd)/specs:/specs mesh-tlaplus:latest \

tlc2.TLC /specs/Tier1.tla -workers auto

# Interactive REPL:

docker run --rm -it -v $(pwd)/specs:/specs mesh-tlaplus:latest \

tlc2.REPL

4.1.2 Jupyter + TLA+ (Interactive Development)

For iterative specification development, the tlaplus-jupyter kernel allows writing and checking TLA+ inside Jupyter notebooks:

# Dockerfile.tlaplus-jupyter

FROM jupyter/minimal-notebook:latest

USER root

RUN apt-get update && apt-get install -y --no-install-recommends \

default-jre-headless && rm -rf /var/lib/apt/lists/*

USER ${NB_UID}

RUN pip install --no-cache-dir tlaplus-jupyter

RUN python -m tlaplus_jupyter.install

WORKDIR /home/jovyan/specs

Run it:

docker build -f Dockerfile.tlaplus-jupyter -t mesh-tlaplus-jupyter:latest .

docker run --rm -p 8888:8888 -v $(pwd)/specs:/home/jovyan/specs \

mesh-tlaplus-jupyter:latest

# Open http://localhost:8888 and create a TLA+ notebook

4.2 Tamarin Prover

Tamarin Prover is used to verify cryptographic protocol properties (SPEC-010 §10.6). It has an official Docker image on GitHub Container Registry.

# Pull the official image:

docker pull ghcr.io/tamarin-prover/tamarin-prover:1.8.0

# Run a proof:

docker run --rm -v $(pwd)/proofs:/proofs \

ghcr.io/tamarin-prover/tamarin-prover:1.8.0 \

tamarin-prover --prove /proofs/PTLC_Atomicity.spthy

# Interactive mode (launches web UI on port 3001):

docker run --rm -p 3001:3001 -v $(pwd)/proofs:/proofs \

ghcr.io/tamarin-prover/tamarin-prover:1.8.0 \

tamarin-prover interactive /proofs/ --interface='*4'

# Open http://localhost:3001 for the Tamarin web interface

TAMARIN LEARNING CURVE: Tamarin's specification language (spthy) has a steep learning curve. Start with the official tutorial at https://tamarin-prover.com/manual/master/book/ before attempting to model MESH protocols. Budget 2--4 weeks of study before writing production-quality proofs.

5. Testnet Orchestration

The full 4-validator testnet is orchestrated by docker compose. This is the primary way to run the MVP end-to-end.

5.1 docker-compose.yml

# docker-compose.yml

version: "3.9"

services:

validator-1:

build: .

container_name: mesh-validator-1

command: ["mesh-validator", "--config", "/config/validator-1.toml"]

volumes:

- ./config:/config:ro

- validator-1-data:/data

ports:

- "4430:4430/udp"

- "4431:4431/udp"

networks:

- meshnet

validator-2:

build: .

container_name: mesh-validator-2

command: ["mesh-validator", "--config", "/config/validator-2.toml"]

volumes:

- ./config:/config:ro

- validator-2-data:/data

ports:

- "4432:4430/udp"

- "4433:4431/udp"

networks:

- meshnet

validator-3:

build: .

container_name: mesh-validator-3

command: ["mesh-validator", "--config", "/config/validator-3.toml"]

volumes:

- ./config:/config:ro

- validator-3-data:/data

ports:

- "4434:4430/udp"

- "4435:4431/udp"

networks:

- meshnet

validator-4:

build: .

container_name: mesh-validator-4

command: ["mesh-validator", "--config", "/config/validator-4.toml"]

volumes:

- ./config:/config:ro

- validator-4-data:/data

ports:

- "4436:4430/udp"

- "4437:4431/udp"

networks:

- meshnet

volumes:

validator-1-data:

validator-2-data:

validator-3-data:

validator-4-data:

networks:

meshnet:

driver: bridge

5.2 Usage

# Build and start the testnet:

docker compose up --build -d

# View logs from all validators:

docker compose logs -f

# View logs from one validator:

docker compose logs -f validator-1

# Run the wallet CLI against the testnet:

docker compose exec validator-1 mesh-wallet --config /config/wallet.toml \

send --to <bob-pubkey> --amount 500 --asset test-token

# Stop the testnet:

docker compose down

# Stop and wipe all data (clean slate):

docker compose down -v

# Simulate a crash: kill one validator

docker compose stop validator-3

# ... run transactions, they should still succeed (3/4 = 2f+1 with f=1)

docker compose start validator-3 # it should sync back up

6. CI/CD Pipeline

The project uses GitHub Actions for continuous integration. The pipeline runs on every push to any branch and every pull request to main.

6.1 GitHub Actions Workflow

# .github/workflows/ci.yml

name: CI

on: [push, pull_request]

env:

CARGO_TERM_COLOR: always

RUST_BACKTRACE: 1

jobs:

check:

runs-on: ubuntu-24.04

container: rust:1.85.0-bookworm

steps:

- uses: actions/checkout@v4

- uses: actions/cache@v4

with:

path: |

~/.cargo/registry

target/

key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}

- run: cargo fmt --all -- --check

- run: cargo clippy --all-targets -- -D warnings

- run: cargo build --all-targets

- run: cargo test --all-targets

audit:

runs-on: ubuntu-24.04

container: rust:1.85.0-bookworm

steps:

- uses: actions/checkout@v4

- run: cargo install cargo-audit cargo-deny

- run: cargo audit

- run: cargo deny check licenses

The pipeline enforces: formatting (rustfmt), lint warnings (clippy with -D warnings), compilation, all tests pass, no known vulnerabilities (cargo audit), and license compliance (cargo deny). Any failure blocks merge.

7. Rust Crate Dependencies (Pinned)

These are the exact crate versions to be specified in Cargo.toml. All versions are pinned and locked via Cargo.lock. Do not use version ranges (e.g., "^1.0") for cryptographic dependencies --- pin to the exact patch version.

7.1 mesh-crypto

---

Crate Version Purpose and Notes

ed25519-dalek 2.1.1 Ed25519 signatures. Enable features: ["hazmat", "rand_core"]. This is the dalek-cryptography crate maintained by the community since the original author's departure.

curve25519-dalek 4.1.3 Ristretto group operations for Pedersen commitments. Enable features: ["alloc", "precomputed-tables"].

bulletproofs 4.0.0 Bulletproofs range proofs over Ristretto. Depends on curve25519-dalek and merlin. MIT licensed.

merlin 3.0.0 Transcript-based Fiat-Shamir transform. Used by bulletproofs for non-interactive proofs.

sha3 0.10.8 SHA3-256 and SHAKE256. RustCrypto project. Pure Rust.

chacha20poly1305 0.10.1 ChaCha20-Poly1305 AEAD. For memo encryption and transport-layer encryption.

rand 0.8.5 Cryptographically secure random number generation. Uses OS entropy.

rand_core 0.6.4 Core traits for RNG. Required by dalek crates.

zeroize 1.8.1 Securely zeroes memory on drop. MUST be used for all secret key material.

---

7.2 mesh-network

---

Crate Version Purpose and Notes

quinn 0.11.6 QUIC protocol implementation. Built on tokio and rustls. This is the primary networking dependency.

rustls 0.23.22 TLS 1.3 implementation in Rust. No OpenSSL dependency at runtime. Used by quinn.

rustls-pemfile 2.2.0 PEM file parsing for TLS certificates.

rcgen 0.13.2 X.509 certificate generation. Used to create self-signed TLS certs for testnet validators.

tokio 1.43.0 Async runtime. Enable features: ["full"]. All async I/O runs on tokio.

bytes 1.9.0 Efficient byte buffer manipulation. Used for message framing.

---

7.3 mesh-validator

---

Crate Version Purpose and Notes

sled 0.34.7 Embedded key-value database. Used for account state, certificates, and equivocation records. Note: sled is in maintenance mode; if it becomes unmaintained, migrate to redb (0.22.0) as a drop-in replacement.

toml 0.8.20 TOML configuration file parsing. For validator config files.

tracing 0.1.41 Structured logging framework. All log output uses tracing macros.

tracing-subscriber 0.3.19 Log output formatting. Enable features: ["env-filter", "json"]. JSON output for machine-parseable logs.

---

7.4 mesh-wallet

---

Crate Version Purpose and Notes

clap 4.5.26 Command-line argument parser. Enable features: ["derive"]. All CLI commands defined via derive macros.

dialoguer 0.11.0 Interactive terminal prompts. Used for key generation confirmation and passphrase entry.

hex 0.4.3 Hex encoding/decoding. For displaying public keys and transaction hashes to the user.

---

7.5 Development and Testing

---

Crate Version Purpose and Notes

proptest 1.6.0 Property-based testing framework. Used for serialisation round-trip tests and fuzzing protocol invariants.

criterion 0.5.1 Benchmarking framework. Used for crypto operation benchmarks (range proof generation/verification, signing, etc.).

tokio-test 0.4.4 Utilities for testing async code. Pairs with tokio.

tempfile 3.14.0 Temporary file/directory creation for test isolation.

---

DEPENDENCY HYGIENE: Run cargo deny check licenses before adding any new dependency. MESH is Apache 2.0 licensed. All dependencies MUST be compatible (Apache 2.0, MIT, BSD-2, BSD-3, ISC, or Zlib). GPL dependencies are PROHIBITED because they would require the entire project to be GPL. LGPL dependencies are acceptable only if dynamically linked.

8. Repository Structure

The repository follows Rust workspace conventions with additional top-level directories for specifications, formal proofs, and configuration.

mesh/

├── Cargo.toml # Workspace root

├── Cargo.lock # Pinned dependency versions

├── rust-toolchain.toml # Pinned Rust version

├── .cargo/config.toml # Build settings (linker, flags)

├── .github/workflows/ci.yml # CI pipeline

├── Dockerfile # Multi-stage build

├── Dockerfile.build # Development build container

├── Dockerfile.tlaplus # TLA+ tools container

├── Dockerfile.tlaplus-jupyter # Interactive TLA+ notebooks

├── docker-compose.yml # 4-validator testnet

├── deny.toml # cargo-deny license config

├── LICENSE # Apache 2.0

├── README.md

├── FUTURE.md # Ideas deferred from MVP scope

│

├── crates/

│ ├── mesh-types/ # Data structures and serialisation

│ │ ├── src/lib.rs

│ │ └── Cargo.toml

│ ├── mesh-crypto/ # Cryptographic operations

│ │ ├── src/lib.rs

│ │ └── Cargo.toml

│ ├── mesh-network/ # QUIC transport layer

│ │ ├── src/lib.rs

│ │ └── Cargo.toml

│ ├── mesh-validator/ # Validator binary

│ │ ├── src/main.rs

│ │ └── Cargo.toml

│ └── mesh-wallet/ # CLI wallet binary

│ ├── src/main.rs

│ └── Cargo.toml

│

├── specs/ # Formal specifications (TLA+)

│ ├── Tier1.tla

│ ├── Tier1.cfg # TLC model config

│ └── ValueSemiring.tla

│

├── proofs/ # Tamarin protocol proofs

│ ├── PTLC_Atomicity.spthy

│ └── Stealth_Unlinkability.spthy

│

├── config/ # Testnet configuration files

│ ├── validator-1.toml

│ ├── validator-2.toml

│ ├── validator-3.toml

│ ├── validator-4.toml

│ └── wallet.toml

│

├── test-vectors/ # Reference test vectors (JSON)

│ ├── spec-002/

│ ├── spec-003/

│ └── spec-006/

│

├── docs/ # Specification documents (docx/pdf)

│ ├── MESH-Protocol-Specification-Suite-v0.1.0.docx

│ ├── MESH-Specification-Addendum-SPEC-004-005-009.docx

│ ├── MESH-MVP-Roadmap-Solo-Bootstrap.docx

│ └── MESH-Dev-Environment.docx

│

└── benches/ # Criterion benchmarks

├── crypto_bench.rs

└── serialisation_bench.rs

9. Quick Reference Card

Cut this page out and stick it on your monitor.

---

Task Command

Build (host) cargo build

Build (container) docker run --rm -v $(pwd):/workspace -v cargo-cache:/usr/local/cargo/registry mesh-build:latest cargo build

Test (fast) cargo nextest run

Test (container) docker run --rm -v $(pwd):/workspace -v cargo-cache:/usr/local/cargo/registry mesh-build:latest cargo nextest run

Lint cargo clippy -- -D warnings

Format cargo fmt --all

Format check cargo fmt --all -- --check

Audit deps cargo audit

License check cargo deny check licenses

Start testnet docker compose up --build -d

View testnet logs docker compose logs -f

Stop testnet docker compose down

Wipe testnet data docker compose down -v

Kill one validator docker compose stop validator-3

Run TLC model check docker run --rm -v $(pwd)/specs:/specs mesh-tlaplus:latest tlc2.TLC /specs/Tier1.tla -workers auto

Run Tamarin proof docker run --rm -v $(pwd)/proofs:/proofs ghcr.io/tamarin-prover/tamarin-prover:1.8.0 tamarin-prover --prove /proofs/PTLC_Atomicity.spthy

Benchmark crypto cargo bench --bench crypto_bench

Generate release binary cargo build --release

---