| name | tla-inductive-invariant-validation |
| description | Validate candidate inductive invariants for TLA+ safety proofs with Apalache or TLC. Use when designing or debugging an invariant, especially when TLAPS cannot discharge initiation, consecution, or safety-implication obligations. |
Validate a TLA+ inductive invariant
Use a model checker to falsify a candidate invariant before investing in its TLAPS proof. Treat a successful finite check as evidence only: prove the invariant in TLAPS, and finish with the benchmark's authoritative check_proof_bin command.
Run the three Apalache checks
Shape the candidate as IndInv == TypeOK /\ H, where TypeOK contains one finite-domain membership clause for every variable and H contains the additional facts needed for induction. Given a target module Target, a typed wrapper APTarget.tla, and a safety predicate Safety, run:
apalache-mc check --config=APTarget.cfg --init=Init --inv=IndInv --length=0 APTarget.tla
apalache-mc check --config=APTarget.cfg --init=IndInv --inv=IndInv --length=1 APTarget.tla
apalache-mc check --config=APTarget.cfg --init=IndInv --inv=Safety --length=0 APTarget.tla
Interpret these checks as:
Init => IndInv: legitimate initial states satisfy the candidate.IndInv /\ Next => IndInv': one step preserves the candidate.IndInv => Safety: the candidate is strong enough to prove the goal.
The checks starting from --init=IndInv require the candidate to assign every variable. A bare safety predicate can instead produce an assignment error such as x' is used before it is assigned. Write the missing TypeOK if the stripped target has none. Bound Nat-typed values to small finite sets, for example num \in [P -> 0..4], and widen a bound before trusting a counterexample that may depend on it.
When a check fails, read the counterexample. Apalache writes violation1.tla in a timestamped directory under _apalache-out/<module>.tla/ unless redirected with --out-dir or --run-dir; the Check the trace in: ... log line gives the exact path.
- A failure of the first check means the candidate excludes a legitimate initial state.
- A failure of the second check gives a state satisfying
IndInv and a successor violating it. The trailing InvariantViolation formula identifies the broken conjunct and usually exposes the fact missing from H.
- A failure of the third check means the candidate does not imply the safety goal.
Strengthen or correct the candidate from the trace, then rerun all three checks.
Build a non-invasive Apalache wrapper
Keep tool-specific annotations out of Target.tla. Re-declare its constants and variables with Apalache types in a separate wrapper, then instantiate the target:
---- MODULE APTarget ----
EXTENDS Naturals
CONSTANT
\* @type: Int;
N
VARIABLE
\* @type: Set(Int);
active
INSTANCE Target
TypeOK == active \in SUBSET (0..N)
H == TRUE
IndInv == TypeOK /\ H
====
Match every re-declared name exactly so implicit INSTANCE substitution binds it. Put each \* @type: annotation between the CONSTANT or VARIABLE keyword and the name it annotates, including every name originally declared in a multi-name block. A comment above the keyword is not accepted and leads to Expected a type annotation for VARIABLE <name>.
Define IndInv in the wrapper. Fix finite constants in APTarget.cfg, for example:
INIT Init
NEXT Next
CONSTANT N = 5
Alternatively, use --cinit. For an uninterpreted constant, define a finite value operator such as JugVal in the wrapper and substitute it with Jug <- JugVal in the configuration. If a polymorphic helper such as Sum, Range, or ToSet defeats type checking, shadow it in the wrapper with a monomorphic version.
Only if the wrapper cannot be made to typecheck, annotate a private scratch copy:
mkdir -p scratch
cp Target.tla scratch/Candidate.tla
Never make the submitted solution extend or instantiate the wrapper or scratch module. Do not alter the target or any dependency as part of model-checking exploration.
Fall back to TLC
Use TLC when Apalache cannot type the target through a wrapper. Create a separate MCTarget.tla that extends Target and defines TypeOK, H, and IndInv, with MCTarget.cfg beside it. TLC is not on PATH; run:
java -cp /opt/sany/lib/tla2tools.jar tlc2.TLC -deadlock -config MCTarget.cfg MCTarget.tla
Check the inductive step by making the candidate its own initial predicate:
INIT IndInv
NEXT Next
INVARIANT IndInv
This checks IndInv /\ Next => IndInv' because IndInv is an ordinary invariant of the specification started in IndInv. Check Init => IndInv separately on the real specification with SPECIFICATION Spec and INVARIANT IndInv. Include Safety as a conjunct of IndInv to check that the candidate implies it.
Use the same enumerable TypeOK /\ H shape as for Apalache. TLC first builds the states satisfying TypeOK and then filters them with H, so start with the smallest useful model. To reduce enumeration:
- Move a conjunct of
H immediately after the TypeOK clauses that bind the variables it mentions, allowing TLC to prune earlier.
- Sample large domains with
RandomSubset(k, S) from the Randomization module. Rewrite v \subseteq W as v \in SUBSET W and sample it with RandomSetOfSubsets(k, p, W).
Aim for a few dozen initial states. A TLC violation supplies the same useful two-state signal as Apalache. Once random sampling is involved, a run with no violation proves nothing; rerun it about a dozen times and abandon a run whose search depth grows beyond roughly a dozen steps.
See Leslie Lamport's Using TLC to Check Inductive Invariance for the TLC technique.
Never cite an Apalache or TLC verdict as justification for a TLAPS proof step.
