Skip to content

Conversation

@beu5a
Copy link
Collaborator

@beu5a beu5a commented Dec 24, 2025

This PR adds TLC (the TLA+ model checker) as an alternative backend for quint verify, alongside the existing Apalache backend.

Usage

quint verify --backend=tlc spec.qnt

quint verify --backend=tlc --tlc-config=tlc.json spec.qnt

Example tlc.json:

  {
    "maxHeap": "-Xmx16G",
    "stackSize": "-Xss1G",
    "workers": 4
  }

Features

  • New --backend=tlc option for the verify command
  • TLC runs using the JAR bundled with Apalache (requires Apalache to be downloaded first)

Code organization

  • tlc.ts - TLC model checker interface
  • quintMCWrapper.ts - Unified wrapper for model checkers (Apalache, TLC)
  • Moved result processing to cliReporting.ts

Limitations

  • No ITF trace output for TLC (counterexamples printed to stdout by TLC)
  • Requires Apalache JAR to be present
  • I have read and I understand the Note on AI-assisted contributions
  • Changes manually tested locally and confirmed to work as described
    (including screenshots is helpful)
  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality

This comment was marked as resolved.

@beu5a beu5a force-pushed the yassine/add-tlc-support branch from 8eef1ad to 89873f8 Compare December 24, 2025 17:14
@beu5a beu5a closed this Jan 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants