tla-precheck

library0.1.7jsnpmunverified

TLA PreCheck is a TypeScript DSL and compiler that lets you define state machines with formal verification via TLA+ model checking. Version 0.1.7, pre-release. It translates a single specification into a TLA+ spec for mathematical correctness proofs, a TypeScript interpreter for runtime, typed function bindings for development, and Postgres DDL for database constraint enforcement. Key differentiator: it proves the generated code and spec produce identical state graphs, catching invariant violations at build time. Targets developers building reliable distributed systems, agents, or workflow engines who want to replace scattered if/else guards with verifiable state machines. Requires Node.js 18+ and the TLA+ tools (TLC model checker).

devops

npm install tla-precheck

github ↗package ↗homepage ↗

INSTALL

IMPORT

SIG · TLA-PRECHECK

tla-precheck

devopsjavascriptv0.1.7

harness data pending

Install & Compatibility

Where this runs

No compatibility data collected yet for this library.

Code

Verified usage

Verified import paths — ran on the pinned version, not inferred.

defineMachine

✓ import { defineMachine } from 'tla-precheck';

✗ const { defineMachine } = require('tla-precheck');

ESM-only package; CommonJS require is not supported.

Machine

✓ import type { Machine } from 'tla-precheck';

✗ import { Machine } from 'tla-precheck';

Machine is a type export for TypeScript; don't import as value.

mapVar

✓ import { mapVar } from 'tla-precheck';

Named export for defining state variables.

Defines a minimal state machine with one action, then shows how to generate code.

import { defineMachine, mapVar, enumType, lit, eq, index, and, param } from 'tla-precheck'; const machine = defineMachine({ version: 1, moduleName: 'AgentRuns', variables: { status: mapVar('Runs', enumType('active', 'done'), lit('active')), }, actions: { complete: { params: { r: 'Runs' }, guard: eq(index(status, param('r')), lit('active')), updates: [setMap('status', param('r'), lit('done'))], }, }, }); type AgentRunsMachine = typeof machine; // Now generate code: npx tla-precheck generate

Debug

Known issues

deprecatedThe package is pre-1.0; API may change breakingly in minor versions.

fix

Pin to exact version and test upgrades.

affects: <1.0

gotchaTLA+ tools must be installed separately and on PATH; build will fail without them.

fix

Install tlaplus-community-tools from GitHub releases or via package manager.

affects: >=0.0

gotchaOnly Node.js 18+ supported; older versions cause cryptic errors.

fix

Upgrade Node.js to 18+.

affects: >=0.0

gotchaGenerated Postgres DDL assumes use of pg or similar; not automatically applied.

fix

Manually run generated SQL files or integrate with migration tool.

affects: >=0.0

Errors

Common errors & fixes

Error: Command failed: tlc ... TLC exited with code 1

TLC model checker not installed or not on PATH.

fix

Install tlaplus-community-tools and ensure 'tlc' binary is in PATH.

SyntaxError: Cannot use import statement outside a module

Attempting to use ESM import in a CommonJS context.

fix

Ensure package.json has 'type': 'module' or run with --input-type=module.

Upgrade

Version history

0.1.7latest on npm

Audit

Dependencies

tlaplus-community-toolsrequiredRequired to run TLC model checker for formal verification

Agent activity

2 hits · last 30 days

node

Resources

githubhttps://github.com/kingbootoshi/tla-precheck ↗

packagetla-precheck ↗

homepagehttps://github.com/kingbootoshi/tla-precheck#readme ↗