TLA PreCheck

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).