I3DP

Automatic Inductive Invariant Inference for TLA+ Protocols

---

This repository accompanies the I3DP paper and contains the implementation, benchmark suite, proof artifacts, and evaluation scripts used to study automatic inductive invariant inference for TLA+ protocols.

I3DP targets safety verification of TLA+ specifications. It generates candidate inductive strengthenings, records run artifacts for debugging and reproduction, and can be paired with the TLA+ proof system (TLAPS) for mechanized proof checking.

Paper: I3DP: Automatic Inductive Invariant Inference for TLA+ Protocols (SOSP 2026).

Environment

The artifact was developed and evaluated on the following setup:

• OS: macOS 26.5.2 (arm64)
• Python: 3.11.14
• pip: 26.0.1
• setuptools: 82.0.0
• Python packages: openai==2.21.0, filelock==3.23.0
• Java: OpenJDK 25.0.2
• Apalache: 0.52.1
• TLAPS: 1.6.0-pre (fd3988f)
• Hardware: MacBook Pro with Apple M4 Pro (12 cores: 8 performance + 4 efficiency), 48 GB memory

No deliberate malicious or destructive operations are performed by any component of this artifact.

What Is In This Repository

Path	Description
src/i3dp/	Core implementation
i3dp_cli.py	Main CLI wrapper used for benchmark runs
benchmarks/	Benchmark specifications, configs, and proof files
outputs/	Saved benchmark outputs
replays/	Recovered LLM replay logs for all 29 benchmarks
run_benchmarks.py	Batch runner for the benchmark suite
replay_all.py	Offline replay runner for the complete benchmark suite
evaluate_benchmarks.py	Result summarization script
evaluate_replays.py	Replay result summarization script
checkproofs.py	TLAPS proof-checking report generator
scripts/setup_artifact.py	Native installer for pinned evaluation dependencies
lib/tla2tools-checkall.jar	Bundled TLC jar
LICENSE	MIT license for this release

Prerequisites

• Java 11 or newer, available on PATH, or pointed to by JAVA_EXE; paper results used OpenJDK 25.0.2
• Python 3.10 or newer
• Apalache 0.52.1 — download this exact version from apalache-mc releases, ensure apalache-mc is on PATH, or set APALACHE_EXE=/path/to/apalache-mc
• LLM API key — required only for live runs; obtain an OpenRouter API key and set OPENROUTER_API_KEY to generate candidate invariants via LLM
• TLAPS 1.6.0-pre (fd3988f) (optional, for proof checking) — install from TLAPS releases; required only if running checkproofs.py

Runtime dependencies and development tools are pinned in setup.py; build dependencies are pinned in pyproject.toml. requirements.txt mirrors the runtime pins for tools that consume requirements files directly.

The repository ships with a modified TLC jar at lib/tla2tools-checkall.jar, sourced from the Endive repository. This jar extends the standard tla2tools.jar with a checkall mode that batch-checks all candidate invariants against reachable states in a single TLC run, significantly reducing per-iteration overhead. To override it, set TLA2TOOLS_JAR=/path/to/tla2tools.jar.

Automated native setup

On macOS arm64 and Linux x86-64, the setup script installs checksum-verified JDK 25.0.2 and Apalache 0.52.1 under .artifact-tools/, creates .venv/, and installs the pinned Python dependencies. It does not modify system directories:

python scripts/setup_artifact.py
source .artifact-tools/env.sh

To include TLAPS for proof checking, add --with-proofs. The TLAPS archive is large (approximately 0.9–1.1 GB):

python scripts/setup_artifact.py --with-proofs
source .artifact-tools/env.sh

Run the script with Python 3.10 or newer; the virtual environment uses that same interpreter. Repeated setup runs reuse installed tools that have already passed checksum validation. Users on other platforms should follow the manual prerequisites above.

Tip

If your system Python is externally managed and rejects pip install -e ., use a virtual environment or a Conda environment.

Note

IC3 queries (consecution, frontier, predecessor, and clause checks) default to Apalache. Pass --tlc to run_benchmarks.py to use TLC for all IC3 queries instead, which is faster for some protocols. Three protocols (learning_switch, learning_switch_i4, paxos_epr) cannot run IC3 queries under TLC and always use Apalache. Invariant screening is always performed by TLC regardless of this setting.

Reproducing a Single Run

Install and run:

python -m venv .venv
source .venv/bin/activate
python -m pip install pip==26.0.1
pip install -e .
export OPENROUTER_API_KEY="sk-or-v1-..."

For a minimal end-to-end run, start with a small benchmark such as TwoPhase:

python run_benchmarks.py TwoPhase \
  --output-dir outputs/reproduced/minimal

run_benchmarks.py accepts either a benchmark alias such as TwoPhase, a benchmark directory such as benchmarks/TwoPhase, or a full spec stem such as benchmarks/TwoPhase/TwoPhase.

Typical outputs for one run

• Terminal output mirrored to outputs/reproduced/minimal/benchmarks/TwoPhase.out
• Generated intermediate files under benchmarks/TwoPhase/gen_tla/
• Reachable-state and auxiliary data under benchmarks/TwoPhase/states/ and benchmarks/TwoPhase/tmp/
• Per-run logs and debug bundles under benchmarks/TwoPhase/results/

If the run succeeds, the log includes an IndAuto == block together with clause counts and timing statistics.

To extend this example with a new protocol, copy a small benchmark directory such as benchmarks/TwoPhase, rename its .tla and .config.json files, and update the configuration fields (preds, safety, constants, quant_inv, model_consts, and typeok). The new benchmark can then be passed to run_benchmarks.py by directory or specification stem.

Replaying Without LLM API Calls

We extracted the LLM responses from the saved run logs and stored them in replays/. These files cover all 29 benchmarks and allow the runs to be replayed without LLM API calls.

Run a quick API-free check:

python replay_all.py Consensus

Replay the complete benchmark suite:

python replay_all.py

The runner processes the benchmarks sequentially and writes each console log to outputs/replays/<benchmark>.out.

The Mongo replay is expected to take approximately 1–2 hours.

A successful single replay reports that every recorded completion was consumed and an inductive invariant was found:

LLM replay consumed all ... recorded completions
Inductive invariant found!
[PASS] MongoLoglessDynamicRaft

A successful complete replay ends with:

Replay summary: 29/29 passed

Evaluate the saved replay outputs:

python evaluate_replays.py

Reproducing the Batch Evaluation

Run the default baseline suite:

python run_benchmarks.py \
  --run_all \
  --output-dir outputs/reproduced/baseline

Run selected benchmarks only:

python run_benchmarks.py TwoPhase Simple \
  --output-dir outputs/reproduced/selected

Runs are sequential by design.

To switch the LLM model (e.g., for the weaker-model ablation in the paper):

python run_benchmarks.py \
  --run_all \
  --llm_model google/gemini-3-flash-preview \
  --output-dir outputs/reproduced/gemini-flash

The default is anthropic/claude-opus-4.6.

Summarize saved outputs:

python evaluate_benchmarks.py --output-dir outputs/reproduced/baseline

This reads the selected output directory and converts run logs into compact summaries suitable for inspection or paper-oriented reporting.

Evaluate the weaker-model ablation separately:

python evaluate_benchmarks.py \
  --output-dir outputs/reproduced/gemini-flash \
  --primary-label Gemini-Flash

The dedicated output directories keep new baseline and ablation runs separate from each other and from the saved release outputs. The --run_all flag is required here because the release includes successful reference outputs that the runner otherwise skips to support interrupted-run recovery.

Benchmark Provenance

• 28 of the 29 benchmarks originate from the Endive benchmark collection.
• paxos_epr is the remaining benchmark distributed with this artifact.

The Endive-derived benchmark specifications were not modified beyond what is required for correct TLC model checking (e.g., model-value declarations, symmetry-set annotations).

Experiment-to-Paper Mapping

Paper Table / Figure	Artifact Command	Output
Table 1 (I3DP column)	python run_benchmarks.py --run_all --output-dir outputs/reproduced/baseline	Per-benchmark .out files under outputs/reproduced/baseline/benchmarks/
Table 1 (LLM-var ablation)	python run_benchmarks.py --run_all --llm_model google/gemini-3-flash-preview --output-dir outputs/reproduced/gemini-flash	Per-benchmark .out files under outputs/reproduced/gemini-flash/benchmarks/
Table 1 (paper-style summary)	python evaluate_benchmarks.py --output-dir outputs/reproduced/baseline	Printed table with Time and Inv columns
Table 1 (offline replay)	python replay_all.py	Per-benchmark replay logs under outputs/replays/
Table 1 (replay summary)	python evaluate_replays.py	Replay table and pass/fail summary
TLAPS unbounded proofs (Section 5.3)	python checkproofs.py	Proof-checking report for all *_IndProofs.tla files

Expected Resource Usage

Approximate resource usage per benchmark:

Benchmark	Est. Time	Benchmark	Est. Time
Consensus	~1 s	TCommit	~1 s
lockserver	~60 s	Simple	~50 s
toy_consensus	~34 s	SimpleRegular	~45 s
firewall	~35 s	simple_decentralized_lock	~35 s
majorityset_leader_election	~40 s	quorum_leader_election	~41 s
toy_consensus_forall	~42 s	simple_election	~46 s
naive_consensus	~55 s	lockserv	~90 s
toy_consensus_epr	~91 s	lockserv_automaton	~92 s
consensus_wo_decide	~92 s	sharded_kv	~117 s
consensus_epr	~122 s	client_server_ae	~153 s
TwoPhase	~165 s	two_phase_commit	~171 s
sharded_kv_no_lost_keys	~188 s	client_server_db_ae	~198 s
learning_switch	~315 s	consensus_forall	~383 s
learning_switch_i4	~434 s	paxos_epr	~1,806 s
MongoLoglessDynamicRaft	~4,525 s

Total suite: expect 2.5–3.5 hours wall-clock for a full sequential run. Disk usage per benchmark is typically under 200 MB for intermediate artifacts.

Apalache uses a 4–12 GB Java heap by default, depending on available memory; use --apalache-heap-gb to set a lower explicit limit. Offline replay makes no LLM API calls and incurs no API charges. Live runs use the configured OpenRouter model and may incur provider charges, which vary with the model and current provider pricing.

Timeout is 600 s per benchmark by default; paxos_epr and MongoLoglessDynamicRaft are given 2 hours each.