Polyweave

Repositories

1

Projects Packages

@polyweave/tla-runner (1.0.1)

Published 2026-07-10 19:10:52 +00:00 by Dvorak

Installation

Set up this registry in your project .npmrc file:

@polyweave:registry=https://hub.kl1.tenere.ai/api/packages/Polyweave/npm/

To install the package using npm, run the following command:

npm install @polyweave/tla-runner@1.0.1

or add it to the package.json file:

"@polyweave/tla-runner": "1.0.1"

For more information on the npm registry, see the documentation.

About this package

tla-runner

Deterministic wrappers around TLA+ toolchain — SANY syntax checking, TLC model checking, TLAPS theorem proving, Apalache symbolic checking. Factory pattern, frame-compatible results.

Synopsis

import { createSanyRunner, createTlcRunner, createTlapsRunner, createApalacheRunner } from '@polyweave/tla-runner';

const sany = createSanyRunner({ /* options */ });
const result = await sany.check('spec.tla');

Install

npm install @polyweave/tla-runner

API

createSanyRunner(options)

Factory for SANY syntax checker. Returns a runner that produces frame-compatible results.

createTlcRunner(options)

Factory for TLC model checker. Returns a runner that produces frame-compatible results.

createTlapsRunner(options)

Factory for TLAPS theorem prover. Returns a runner that produces frame-compatible results.

createApalacheRunner(options)

Factory for Apalache symbolic checker. Returns a runner that produces frame-compatible results.

Tests

npm test

Requirements

Node.js 18 or later. ESM only.

License

MIT

Dependencies

Development Dependencies

ID	Version
@rigor/core	*

Peer Dependencies

ID	Version
@polyweave/core	*

Keywords

polyweave tla-plus tlaplus tlc sany tlaps apalache formal-verification

Details

npm

2026-07-10 19:10:52 +00:00

8

John Dvorak

SEE LICENSE IN LICENSE

2.9 KiB

Assets (1)

tla-runner-1.0.1.tgz 2.9 KiB

Versions (5) View all

1.0.6 2026-07-11

1.0.5 2026-07-11

1.0.3 2026-07-11

1.0.2 2026-07-11

1.0.1 2026-07-10