I3DP
I3DP Artifact for SOSP 2026: Automatic Inductive Invariant Inference for TLA+ Protocols
File Explorer
- client_server_ae.config.json
- client_server_ae.tla
- client_server_ae_IndProofs.tla
- client_server_db_ae.config.json
- client_server_db_ae.tla
- client_server_db_ae_IndProofs.tla
- Randomization.tla
- Consensus.config.json
- Consensus.tla
- Consensus_IndProofs.tla
- consensus_epr.config.json
- consensus_epr.tla
- consensus_epr_IndProofs.tla
- Randomization.tla
- consensus_forall.config.json
- consensus_forall.tla
- consensus_forall_IndProofs.tla
- Randomization.tla
- consensus_wo_decide.config.json
- consensus_wo_decide.tla
- consensus_wo_decide_IndProofs.tla
- Randomization.tla
- firewall.config.json
- firewall.tla
- firewall_IndProofs.tla
- learning_switch.config.json
- learning_switch.tla
- learning_switch_IndProofs.tla
- Randomization.tla
- learning_switch_i4.config.json
- learning_switch_i4.tla
- learning_switch_i4_apalache_queries.tla
- learning_switch_i4_IndProofs.tla
- lockserv.config.json
- lockserv.tla
- lockserv_IndProofs.tla
- lockserv_automaton.config.json
- lockserv_automaton.tla
- lockserv_automaton_IndProofs.tla
- lockserver.config.json
- lockserver.tla
- lockserver_IndProofs.tla
- majorityset_leader_election.config.json
- majorityset_leader_election.tla
- majorityset_leader_election_IndProofs.tla
- Randomization.tla
- MongoLoglessDynamicRaft.config.json
- MongoLoglessDynamicRaft.tla
- MongoLoglessDynamicRaft_IndProofs.tla
- Randomization.tla
- naive_consensus.config.json
- naive_consensus.tla
- naive_consensus_IndProofs.tla
- Randomization.tla
- paxos_epr.config.json
- paxos_epr.tla
- paxos_epr_IndProofs.tla
- paxos_epr_simcheck.tla
- Randomization.tla
- quorum_leader_election.config.json
- quorum_leader_election.tla
- quorum_leader_election_IndProofs.tla
- Randomization.tla
- sharded_kv.config.json
- sharded_kv.tla
- sharded_kv_IndProofs.tla
- Randomization.tla
- sharded_kv_no_lost_keys.config.json
- sharded_kv_no_lost_keys.tla
- sharded_kv_no_lost_keys_IndProofs.tla
- Simple.config.json
- Simple.tla
- Simple_IndProofs.tla
- simple_decentralized_lock.config.json
- simple_decentralized_lock.tla
- simple_decentralized_lock_IndProofs.tla
- simple_election.config.json
- simple_election.tla
- simple_election_IndProofs.tla
- SimpleRegular.config.json
- SimpleRegular.tla
- SimpleRegular_IndProofs.tla
- TCommit.config.json
- TCommit.tla
- TCommit_IndProofs.tla
- toy_consensus.config.json
- toy_consensus.tla
- toy_consensus_IndProofs.tla
- toy_consensus_epr.config.json
- toy_consensus_epr.tla
- toy_consensus_epr_IndProofs.tla
- toy_consensus_forall.config.json
- toy_consensus_forall.tla
- toy_consensus_forall_IndProofs.tla
- two_phase_commit.config.json
- two_phase_commit.tla
- two_phase_commit_IndProofs.tla
- TwoPhase.config.json
- TwoPhase.tla
- TwoPhase_IndProofs.tla
- Randomization.tla
- tla2tools-checkall.jar
- client_server_ae.out
- client_server_db_ae.out
- Consensus.out
- consensus_epr.out
- consensus_forall.out
- consensus_wo_decide.out
- firewall.out
- learning_switch.out
- learning_switch_i4.out
- lockserv.out
- lockserv_automaton.out
- lockserver.out
- majorityset_leader_election.out
- MongoLoglessDynamicRaft.out
- naive_consensus.out
- paxos_epr.out
- quorum_leader_election.out
- sharded_kv.out
- sharded_kv_no_lost_keys.out
- Simple.out
- simple_decentralized_lock.out
- simple_election.out
- SimpleRegular.out
- TCommit.out
- toy_consensus.out
- toy_consensus_epr.out
- toy_consensus_forall.out
- two_phase_commit.out
- TwoPhase.out
- client_server_ae.out
- client_server_db_ae.out
- Consensus.out
- consensus_epr.out
- consensus_forall.out
- consensus_wo_decide.out
- firewall.out
- learning_switch.out
- learning_switch_i4.out
- lockserv.out
- lockserv_automaton.out
- lockserver.out
- majorityset_leader_election.out
- MongoLoglessDynamicRaft.out
- naive_consensus.out
- paxos_epr.out
- quorum_leader_election.out
- sharded_kv.out
- sharded_kv_no_lost_keys.out
- Simple.out
- simple_decentralized_lock.out
- simple_election.out
- SimpleRegular.out
- TCommit.out
- toy_consensus.out
- toy_consensus_epr.out
- toy_consensus_forall.out
- two_phase_commit.out
- TwoPhase.out
- client_server_ae.recovered.jsonl
- client_server_db_ae.recovered.jsonl
- Consensus.recovered.jsonl
- consensus_epr.recovered.jsonl
- consensus_forall.recovered.jsonl
- consensus_wo_decide.recovered.jsonl
- firewall.recovered.jsonl
- learning_switch.recovered.jsonl
- learning_switch_i4.recovered.jsonl
- lockserv.recovered.jsonl
- lockserv_automaton.recovered.jsonl
- lockserver.recovered.jsonl
- majorityset_leader_election.recovered.jsonl
- MongoLoglessDynamicRaft.recovered.jsonl
- naive_consensus.recovered.jsonl
- paxos_epr.recovered.jsonl
- quorum_leader_election.recovered.jsonl
- sharded_kv.recovered.jsonl
- sharded_kv_no_lost_keys.recovered.jsonl
- Simple.recovered.jsonl
- simple_decentralized_lock.recovered.jsonl
- simple_election.recovered.jsonl
- SimpleRegular.recovered.jsonl
- TCommit.recovered.jsonl
- toy_consensus.recovered.jsonl
- toy_consensus_epr.recovered.jsonl
- toy_consensus_forall.recovered.jsonl
- two_phase_commit.recovered.jsonl
- TwoPhase.recovered.jsonl
- reconstruct_mldr_h24_prompt.py
- recover_replays.py
- setup_artifact.py
- __init__.py
- apalache_wrapper.py
- cleanup.py
- cleanup_cli.py
- cli.py
- config.py
- core.py
- llm_interface.py
- tla_gen.py
- tlc_pool.py
- tlc_wrapper.py
- utils.py
- test_benchmark_runner.py
- test_config.py
- test_cti_coverage.py
- test_llm_replay.py
- test_replay_artifacts.py
- test_success_path_compatibility.py
- test_validator_outcomes.py
- .gitignore
- checkproofs.py
- evaluate_benchmarks.py
- evaluate_replays.py
- i3dp_cli.py
- LICENSE
- pyproject.toml
- README.md
- replay_all.py
- requirements.txt
- run_benchmarks.py
- setup.py
# Use via CDN
jsDelivrjsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.
Link
Example
// repository documentation
Was this content helpful?
(0 ratings)