Generate SMT from TLA+

[Abhinandan-Pal]

I’m currently working on a project where I intend to use Apalache to translate TLA+ models to SMT. In our workflow, we only need to translate the model—our LTL specification is handled separately.

Following the instructions on [link] and using the tool’s documentation, I attempted to run:

apalache-mc check --debug MC10_8.tla

• Apalache version: 0.47.2
• OS: Ubuntu 24.04 Running as a Docker Env in an Amazon EC2

However, this does not appear to produce a log.smt file as expected. Could you please advise on what I might be doing incorrectly?

Thank you very much for your time, and apologies if the issue is straightforward.

[konnov]

Right. I think the layout of the Apalache output has changed in the meantime. There is a bit of documentation in ADR22, but it would not help you much on the user side. Practically, you should check the directory _apalache-out. It should contain log.smt under the specification name and timestamp, e.g., _apalache-out/y2k_instance.tla/2025-07-01T17-07-38_2078732140518820195/log0.smt.

You should be able to override the directory names with --run-dir and --out-dir.

If you need further hints, let me know. Just keep in mind that the Apalache encoding is specific to bounded model checking. For example, it does not have quantifiers in the SMT output.

[philzook58]

Would it be possible to output the transition relation in a readable-ish smt-lib akin to what yosys can do https://yosyshq.readthedocs.io/projects/yosys/en/0.40/cmd/write_smt2.html ? I was also intrigued at maybe ingesting TLA+ via apalache->smt through the z3 parser akin to what I'm playing around with here for yosys https://github.com/philzook58/knuckledragger/blob/main/kdrag/contrib/yosys/__init__.py

[konnov]

Would it be possible to output the transition relation in a readable-ish smt-lib akin to what yosys can do https://yosyshq.readthedocs.io/projects/yosys/en/0.40/cmd/write_smt2.html ? I was also intrigued at maybe ingesting TLA+ via apalache->smt through the z3 parser akin to what I'm playing around with here for yosys https://github.com/philzook58/knuckledragger/blob/main/kdrag/contrib/yosys/__init__.py

The SMT encoding that Apalache produces is quite specific to its arena representation. I don't think we would be able to produce a generic transition relation. Currently, Apalache is unrolling Next from the arena that it produced in a previous step. Perhaps, @rodrigo7491 has some ideas there.

If you are ok with the current encoding, for sure, we could just emit smt-lib for the current exploration scope. For example, we could just add another method into JSON-RPC that we are slowly developing #3129. This would let you execute the query against various SMT solvers. The only issue is what to do when the solver finds a model. In this case, we would have to somehow ingest the model back and decode it into TLA+.

What would be your optimal workflow, if there was a way to translate TLA+ to SMT-LIB, independently of the current encoding?

[rodrigo7491]

No immediate thoughts from my side, for the time being I think what @konnov suggested is what can be done. Producing generic transition relations, not tied to the current arena representation, or BMC for that matter, might be something interesting to do at some point.

[philzook58]

I apologize, I need to look more deeply into Apalache's encoding. My system is a python interactive proof assistant as a library heavily based around the z3py ast. It is more or less an HOL akin to hol-light or isabelle/hol. I am always looking for use cases, and I thought maybe if Apalache output comprehensible smtlib a system akin to TLAPS or isabelle/tla+ could be built using apalache as the front stages. I have been investigating doing a shallow embedded temporal logic, but ingesting actual textual TLA that had the appropriate types inferred seemed interesting if somehow it were easy.

[philzook58]

My workflow is generally developing proofs in jupyter notebooks. I'd guess I'd have a python function that takes in a tla filename and subprocess calls apalache which would emit smtlib. There is presumably an Init and Trans in the file which would be emitted as a define-fun command defining an unary and binary smtlib predicate over state. I can trick z3 into parsing that back into z3py, from which a user can start an interactive Lemma object with a stated property they'd like to prove about those relations.

Alternatively, Trans might be emitted as a constraint over traces of executions represented as Array(Int, VarType). This is the semantics I recall seeing in a Lamport paper