A proof is semantically correct if each proof obligation is correct – meaning that the assertion follows from the usable facts. Thus, the following could be a semantically correct proof:

However, we would not expect any computer program to check its
correctness. For most mechanical theorem provers, a proof is
checkable if the current version of the prover will verify the proof.
A TLA+ proof is checkable if each of its obligations is checkable.
Since the language is independent of any prover, there can be
no precise definition of what constitutes a checkable obligation. In
practice, a proof step is checkable if there is *some* backend
verifier that accepts it. You should resist tailoring your proof to
particular backends because your proofs will then become
unmaintainable as TLAPS evolves. Instead, if a backend verifier does
not accept a leaf proof, you should try to simplify the reasoning
further using a new level of proof. Eventually, your proof will
produce obligations of sufficiently low complexity that they will
likely continue to be accepted by future versions of TLAPS.

That being said, there are some cases in which you may want to
bypass the default behavior of TLAPS. You may want to
give a longer timeout to the default backend provers. Or you may
want to call particular specialized backend verifiers that perform
better than general purpose theorem provers for certain fragments
of logic. We call these specialized
procedures *tactics*. These tactics are declared in
the `TLAPS.tla`

standard module.

For proving an obligation, the default behaviour of TLAPS
is to try three back-ends in
succession:

SMT is the baseline SMT solver (by default Z3); it is tried with a timeout of 5 seconds.Zenon is a tableaux-based prover for first-order logic; it is tried with a timeout of 10 seconds.Isa is the automatic tactic`auto`

of the Isabelle prover; is tried with a timeout of 30 seconds.

BY ZenonT(30) | Modifying Zenon timeout. |

BY Isa | Calling directly Isabelle with default tactic and timeout. |

BY IsaT(60) | Modifying Isabelle timeout. |

BY IsaM("blast") | Modifying Isabelle tactic. |

BY IsaMT("blast",60) | Modifying Isabelle timeout and tactic. |

Note: the Z3 solver is
distributed with TLAPS. If you want to use CVC4
you have to download and install it from
CVC4. Please check that
you are allowed to install a version according to the licensing
conditions of these solvers, and make sure
that the executables are in your `$PATH`

.

The

BY SMT | Call baseline SMT solver with default timeout of 5 seconds. |

BY SMTT(60) | Call baseline SMT solver with a different timeout. |

In order to
invoke Z3 explicitly, use
the

BY Z3 | Call Z3 backend with default timeout of 5 seconds. |

BY Z3T(60) | Call Z3 with a different timeout. |

In order to
invoke CVC4, use
the `CVC4`

or `CVC4T`

identifiers in
a `USE`

or
`BY`

clause (but remember
that CVC4 is not distributed with TLAPS).

BY CVC4 | Call CVC4 backend with default timeout of 5 seconds. |

BY CVC4T(60) | Call CVC4 with a different timeout. |

If you want to change the baseline SMT solver, you have three options.

`--solver`

command-line option to tlapm with the solver's command line
(described below) as argument, surrounded by single quotes. If you use the
ToolBox, you have to click on "Launch Prover" to give
that argument (see Advanced
options). The option and argument would be entered in the text
box as follows:
solver | text box contents |
---|---|

CVC4 | `--solver 'cvc4 -L smt "$file"'` |

Z3 (Windows) | `--solver 'z3 /smt2 "$file"'` |

Z3 (Linux, MacOS) | `--solver 'z3 -smt2 "$file"'` |

`"$file"`

in place of the
file name. Here are a few examples:
solver | command line |
---|---|

CVC4 | `cvc4 -L smt "$file"` |

Z3 (Windows) | `z3 /smt2 "$file"` |

Z3 (Linux, MacOS) | `z3 -smt2 "$file"` |

`TLAPM_SMT_SOLVER`

environment variable to be the
command line described above. For example, under Linux you should
add the line
export TLAPM_SMT_SOLVER='cvc4 -lang smt2 "$file"' |

`.bashrc`

).