Apalachex

Safe, deterministic Apalache execution and artifact management for Elixir.

Apalachex validates TLA+ inputs, constructs shell-free Apalache plans, runs exactly Apalache 0.58.3, and returns ordered paths to retained ITF files. It does not open, decode, or interpret ITF contents. Version 0.1.0 supports execution on POSIX systems only.

Installation

Add apalachex to the dependencies in mix.exs:

def deps do
  [
    {:apalachex, "~> 0.1.0"}
  ]
end

Apalache 0.58.3 must be available as apalache-mc on PATH, or supplied with the :executable option.

Usage

{:ok, spec} =
  Apalachex.Spec.new(
    source: "Counter.tla",
    config: "Counter.cfg"
  )

run_directory =
  Apalachex.RunDirectory.build(
    spec,
    generated_at: DateTime.utc_now(),
    suffix: "a1b2c3"
  )

plan =
  Apalachex.Plan.new(
    spec,
    mode: :simulate,
    length: 10,
    max_run: 5,
    run_directory: run_directory
  )

{:ok, result} = Apalachex.run(plan)
result.itf_paths

Every reserved run directory is retained. Its apalachex-run.json manifest records the running and completed lifecycle. A successful result always has at least one absolute top-level regular .itf.json path, sorted lexically.

Supported boundary

• Elixir ~> 1.18
• Apalache exactly 0.58.3 or v0.58.3
• POSIX execution only; Windows is rejected after strict option validation and before executable discovery, version probing, run-directory allocation, manifest creation, or process execution
• synchronous execution without a shell
• no timeout, cancellation, supervision, cleanup, or ITF interpretation

Development

asdf plugin add just https://github.com/olofvndrhr/asdf-just.git
asdf install just 1.54.0
just setup
just test
just check
just docs
just package-audit
just consumer-smoke
just test-apalache

just setup requires asdf 0.16.5 and installs the pinned tools from .tool-versions. The consumer and real-Apalache checks require Apalache 0.58.3; the latter is installed by the owned asdf plugin and selected by the repository toolchain.

Maintainer release

Update the version in mix.exs and add its dated changelog section. Commit and push the prepared main, ensure CI is green, then run just release.

The command publishes the prepared version to Hex and creates its GitHub tag and release. It does not prepare, edit, commit, or push main.

License

MIT. See LICENSE.