apalache-mc/apalache

Apalache is a symbolic model checker for TLA+ specifications that performs bounded model checking, type checking, and simulation. It processes TLA+ and Quint inputs through a modular, pass-based analysis pipeline to generate verification conditions for SMT solvers like Z3 and CVC5. The system provides interactive exploration capabilities via JSON-RPC and gRPC, allowing users to step through symbolic transitions and manage model checking sessions programmatically.

28 changes.

The project underwent a major architectural overhaul by introducing a new Low-level Intermediate Representation (LIR) and a redesigned bounded model checker core. This period focused on restructuring the analysis engine for better type safety and modularity, while simultaneously expanding the CLI, test coverage, and development tooling to support the new infrastructure.

54 changes.

This period focused on rebuilding the project's core infrastructure, introducing a comprehensive type-checking system and a modular, pass-based analysis pipeline. Significant efforts were made to enhance the model checker with new SMT solver backends, profiling capabilities, and source-location tracking to improve reliability and debugging.

16 changes.

The project introduced a new stratified rewriting engine and typed symbolic memory cells to refactor the model checker's core infrastructure. This work included implementing specific rules for constants, sets, and boolean logic, alongside a modular SANY importer and comprehensive test coverage for the new components. Additionally, the JSON-RPC interface was extended with snapshot-based rollback capabilities and new session management methods.

Users can now select CVC5 as an SMT solver backend in addition to the existing Z3 support. This change introduces the Cvc5SolverContext implementation, which maps TLA+ encodings (OOPSLA19, Arrays, FunArrays) to specific CVC5 logics (QF\_UFLIA, QF\_AUFLIA) and supports solver tuning parameters and random seeds via the new SolverConfig. The SolverContextFactory has been updated to instantiate the CVC5 context when configured, allowing users to switch solvers for potentially different performance characteristics or constraint support.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt · high confidence

Users can now transpile TLA+ specifications to the VMT format for verification using the VMT solver. This change introduces a new translation pipeline in the \tla-bmcmt\ module that converts TLA+ expressions into SMT terms (supporting boolean logic, quantifiers over restricted sets, and EUF operations like function definitions and updates) and writes the resulting declarations, initial states, transitions, and invariants to an \output.vmt\ file.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/vmt · high confidence

The model checker now provides a \cross\ method on \Iterable\ instances via an implicit class, allowing users to easily generate the Cartesian product of two collections. This utility simplifies operations that require pairing elements from two different sets within the TLA+ model checking context.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/implicitConversions · high confidence

The mod-distribution module now includes a new \apalache-version.properties\ file that exposes the project's version, group ID, and artifact ID as build-time properties. This allows the distribution to self-report its specific Apalache integration details.

mod-distribution · high confidence

The model checker now collects basic profiling metrics for rewriting rules, allowing users to understand performance characteristics. This includes tracking the number of times each rule is called, as well as the count and average size of SMT constants, arena cells, and SMT assertions introduced by each rule. These statistics are written to a dedicated profiling output file when profiling is enabled.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/profiler · high confidence

The JSON-RPC server and the Shai gRPC service now expose an interactive exploration API that allows clients to load a TLA+ or Quint specification, step through its symbolic transitions, check invariants, and query the current state without running a full bounded model check. This enables incremental analysis and debugging of specifications by exposing session-based operations such as loading specs, assuming transitions or states, rolling back to snapshots, and querying operator values or execution traces.

repository · high confidence

Added protobuf definitions for two new Shai services: CmdExecutor, which exposes Apalache's CLI commands (parse, check, typecheck, TLA) via RPC, and TransExplorer, which manages model loading and connection state. These definitions establish the contract for remote command execution and transition exploration capabilities within the Shai API.

shai/src/main/protobuf · high confidence

Added a new hand-written parser and lexer for the Type System 1 grammar (ADR-002) in the \tlair\ module. This implementation uses Scala parser combinators to parse type expressions (such as functions, sets, records, and variants) and type aliases from strings, replacing the previous mechanism and resolving prior parsing bugs.

tlair/src/main/scala/at/forsyte/apalache/tla/types/parser · high confidence

The type-checking module now exposes a listener-based architecture for observing type-checking progress, allowing external components to receive notifications when types are found, errors occur, or warnings are generated. This is implemented via the new TypeCheckerListener trait and its concrete implementations (DefaultTypeCheckerListener, MultiTypeCheckerListener, and SourceAwareTypeCheckerListener). Additionally, the core TypeChecker trait and TypeContext class have been introduced to define the interface for computing expression types within a typing context, and a new TypingInputException has been added to handle irrecoverable errors in user input.

tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck · high confidence

The new sbt-changeling plugin allows users to maintain a merge-conflict-free changelog by storing unreleased change entries in separate files within an \.unreleased\ directory structure. This approach isolates concurrent edits to individual change files, preventing conflicts during merges. The plugin provides SBT tasks to render these entries into a formatted markdown release note file and to update the main \CHANGES.md\ file by prepending the new release notes and cleaning up processed entries. It supports configurable change kinds (such as Features, Bug fixes, and Breaking changes) and integrates into the release pipeline to automate changelog generation.

project/sbt-changeling · high confidence

The \tlair\ module now includes a new set of \Unsafe\*Builder\ traits (e.g., \UnsafeBaseBuilder\, \UnsafeSetBuilder\, \UnsafeFunBuilder\) in the \typecomp.unsafe\ package. These builders provide a programmatic API for constructing TLA+ Intermediate Representation (IR) expressions for base operators, sets, functions, arithmetic, and temporal logic. They operate in a 'scope-unsafe' mode, meaning they do not automatically track variable scoping or binding contexts, which allows for more direct expression construction at the cost of manual scope management by the caller.

tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe · high confidence

Added LoopEncoder and TableauEncoder components to enable the encoding of temporal properties as invariants. LoopEncoder introduces an InLoop variable and auxiliary saved variables to track loop entry and ensure loop closure by comparing current and saved state values. TableauEncoder traverses the temporal formula syntax tree, creating boolean variables for each node to track truth values across states, and rewrites assignment operators to equalities to facilitate this encoding.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/temporal · high confidence

Added a new trace evaluation capability that allows users to drive the model checker using an external trace file (ITF or Apalache JSON format). The \TraceePass\ reads the trace, constructs new Init and Next operators that force the specification to follow the provided state sequence, and replaces the original exploration logic. This enables verification of specific execution paths or replaying observed behaviors without manual invariant tweaking.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/tracee · high confidence

The \stratifiedRules/support\ package now contains the foundational components for the new stratified rewriting engine. This includes a \RewriterImpl\ that maps TLA+ expressions to specific rewriting rules via a lookup table, and a \DelayedConstraintGenerator\ trait that allows SMT constraints to be batched rather than discharged immediately. Several cache implementations (\IntValueCache\, \IntRangeCache\, \RecordDomainCache\, \UninterpretedLiteralCache\) have been added to optimize the creation of Arena cells and manage SMT constraints efficiently. Additionally, a suite of Oracle implementations (\IntOracle\, \MockOracle\, \SparseOracle\, \UninterpretedConstOracle\, \ZipOracle\) provides mechanisms for selecting values from finite candidate sets during model checking.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/support · high confidence

A new \UTFPrinter\ class has been added to the \tlair\ module to handle the pretty-printing of TLA+ expressions into strings. This printer utilizes Unicode characters for logical and set-theoretic operators (such as ∧, ∨, ∈, ⊆, ⊇) and supports the formatting of various TLA+ constructs including boolean operations, arithmetic, temporal logic (box/diamond), function definitions, and LET-IN expressions. This provides a standardized way to convert internal TLA+ Intermediate Representation (LIR) into human-readable text using standard mathematical notation.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/io · high confidence

The \tlair\ module now includes a new \storage\ package that provides infrastructure for tracing TLA+ expressions back to their original source locations. This is achieved through \ChangeListener\, which records the lineage of expressions as they are transformed (mapping new UIDs to their origins), and \SourceLocator\, which combines this lineage with a \SourceMap\ to resolve any expression ID to a \SourceLocation\. Additionally, the package introduces \BodyMapFactory\ for managing operator declarations using \SortedMap\ for stable ordering, and a \DisjointSets\ utility for managing equivalence classes of elements.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/storage · high confidence

The model checker now includes a new \stratifiedRules\ package that defines the core interfaces and data structures for a refactored rewriting engine. This change introduces the \Rewriter\ trait as the central access point for transforming TLA+ expressions into Arena cells, alongside \RewriterScope\ to manage mutable state like the arena and variable bindings during rewriting. It also provides the \StratifiedRule\ interface, which separates arena construction from SMT constraint generation, and includes an initial implementation for the assignment rule (\AssignmentStratifiedRule\).

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules, tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/apalache · high confidence

This change introduces the foundational components of the new bounded model checker implementation in the tla-bmcmt module. It adds the Arena for managing symbolic memory cells, the SymbState and Binding classes for tracking symbolic state and variable bindings, and the SeqModelChecker which orchestrates the sequential model checking process using a TransitionExecutor. The diff also includes the LazyEquality mechanism for caching equality constraints, the SymbStateRewriter for applying operational semantics, and listener interfaces (ModelCheckerListener) for collecting counterexamples and dumping traces to files.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt · high confidence

The \src/tla\ directory now provides a set of TLA+ modules (\Apalache.tla\, \Variants.tla\, \Option.tla\, and several \\_\rewire\\*.tla\ files) that are made available to SANY when parsing specifications. These modules define operators for Apalache-specific features such as data generation (\Gen\), non-deterministic choice (\Guess\), and typed variants, while also providing Apalache-compatible rewrites for standard community modules like \SequencesExt\, \BagsExt\, \Functions\, and \TLC\. This allows users to write specifications using these operators, which Apalache will interpret symbolically or rewire internally, while maintaining compatibility with TLC and TLAPS through the provided default implementations.

src/tla · high confidence

The Shai RPC server now exposes a new \CmdExecutorService\ that allows clients to execute Apalache CLI subcommands (such as parsing, type checking, and model checking) via structured gRPC requests, avoiding JVM startup overhead. This service validates configuration against remote-serving restrictions, executes the corresponding pass chains, and returns results or detailed error data. The server also increases the maximum inbound gRPC message size to 1GB to support large inputs and improves startup error logging for port binding failures.

shai/src/main/scala · high confidence

The repository now includes a \bin/run-in-docker-container\ script that serves as the entrypoint for the Docker image. This script creates a non-root user matching the host user's UID/GID to prevent permission issues with bind-mounted files, verifies the presence of \.tla\ files in the working directory, and executes the Apalache model checker (\apalache-mc\) as that user while preserving environment variables. Additionally, a \bin/apalache-mc\ symlink is introduced to point to the built distribution package.

bin · high confidence

Added SmtTools.scala, which introduces a new internal representation for boolean formulas (BoolFormula) including operators like And, Or, Neg, Implies, and comparison functions (LtFns, NeFns). This component provides a toSmt2 method to convert these formulas into SMT-LIB 2 string format and a simplify method to reduce redundant logical connectives, enabling downstream SMT solvers to process these specific boolean structures.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/smt · high confidence

The tla-assignments module now introduces a new mechanism for handling assignments in TLA+ specifications. AssignmentOperatorIntroduction replaces standard equality assignments (x' = e) with a special assignment operator (x' \<- e) to optimize processing. SymbTransGenerator constructs symbolic transitions from assignment strategies, using sorted maps and sets to ensure deterministic results and avoid sorting overhead. ModuleAdapter facilitates the insertion and extraction of transitions as operators with special names in TLA+ modules. These changes support more efficient and deterministic handling of assignments and transitions in the Apalache model checker.

tla-assignments/src/main · high confidence

The tla-io module introduces a new structured configuration framework (ApalacheConfig) that replaces legacy configuration handling, supporting JSON-based configuration files with strict parsing and precedence rules. This change also adds a new OutputManager to standardize how Apalache writes output files to stable, timestamped run directories, and introduces a ReportGenerator to automatically create bug report templates. Additionally, the module adds a new annotation parser and pretty-printing infrastructure to support reading and writing TLA+ code annotations.

tla-io · high confidence

The rewriter module now includes a MetricProfilerListener that collects SMT translation metrics and writes them to a profile.csv file for performance analysis, a RewriterConfig class to expose the shortCircuit option for controlling boolean operator translation, and new internal types (Recoverable, SymbStateRewriterListener, SymbStateRewriterSnapshot) to support state snapshotting and cache management. Additionally, a ConstSimplifierForSmt class provides SMT-specific constant simplification, including precise boolean constant detection and safe handling of set membership operations.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter · high confidence

The repository now includes a suite of new scripts to streamline development workflows. The release pipeline is automated via \release-prepare.sh\ (generates changelogs, creates a release branch, and opens a PR), \release-publish.sh\ (packages artifacts, tags the release, and publishes to GitHub), and \publish-maven.sh\ (publishes Scala libraries to Maven Central). Version management is handled by \get-version.sh\ and \version-bump.sh\. For analysis, \explorer.py\ provides an interactive TLA+ specification explorer, \heatmap.py\ visualizes SMT profiling data, and \prof.py\ parses SMT solver logs.

script · high confidence

The \tlair\ module now provides a comprehensive set of scope-safe builder traits for constructing TLA+ expressions, including \ActionBuilder\, \ArithmeticBuilder\, \BoolBuilder\, \SetBuilder\, \FunBuilder\, \SeqBuilder\, \TemporalBuilder\, and others. These new scope-safe interfaces delegate to the existing \unsafe\ builder implementations, allowing users to build TLA+ specifications with automatic type checking and scope management while maintaining the underlying expression generation logic.

tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder · high confidence

The \tlair\ module now includes a new set of classes for tracking source code locations, including \SourcePosition\, \SourceRegion\, \SourceLocation\, \RegionTree\, and \SourceStore\. \SourceStore\ acts as a central registry that maps expression identifiers to their corresponding source regions, maintaining a tree structure to handle nested source regions. It also implements \TransformationListener\ to automatically propagate source location information when expressions are transformed, ensuring that source mapping remains consistent during analysis. This infrastructure supports more precise error reporting and debugging by preserving the link between TLA+ expressions and their original source positions.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/src · high confidence

The standard transformations package now includes a suite of new language predicates and module transformations to validate and manipulate TLA+ specifications. ContextualLanguagePred serves as an abstract base for checking operator definitions, while specific implementations like FlatLanguagePred, KeraLanguagePred, KeramelizerInputLanguagePred, MonotypeLanguagePred, NonrecursiveLanguagePred, and ReTLALanguagePred enforce constraints such as flattening, monomorphic typing, and non-recursiveness for various backend requirements. Additionally, new transformations include DeclarationSorter for stable topological sorting of operator definitions, DeepCopy for creating structurally identical copies with fresh IDs, Flatten for normalizing boolean operators, IncrementalRenaming for concise variable renaming, ModuleByExTransformer for applying expression transformations to module declarations, PrimePropagation for expanding prime operators, ReplaceFixed for syntax-based substitution, and SimpleUnchangedUnroller for flattening UNCHANGED expressions.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard · high confidence

The stratified rewriting engine now includes dedicated rules for handling built-in constants, integer values, and variable substitutions. BuiltinConstStratifiedRule maps boolean literals, sets, and integers to predefined arena cells, while IntConstStratifiedRule manages integer constants using a value cache to optimize repeated values. SubstStratifiedRule handles the substitution of bound names (such as variables declared with VARIABLE or CONSTANT) by resolving them to their corresponding cells in the current scope, ensuring proper variable binding during model checking.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base · high confidence

The transformations package now includes core infrastructure for monitoring and validating TLA+ transformations. Users benefit from the new LanguageWatchdog, which enforces language predicates to ensure expressions remain within expected TLA+ fragments (addressing issue \#68), and the TransformationTracker, which allows clients to record changes made to expressions and declarations via the TransformationListener interface. These components provide a structured way to validate transformation outputs and observe transformation side effects.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations · high confidence

The transformation engine now includes a stable topological sort algorithm that preserves the original order of declarations within dependency layers, ensuring deterministic processing. Additionally, a new tracking system has been introduced, featuring an IdleTracker for scenarios where no tracking is needed, and a TrackerWithListeners that allows external observers to monitor transformation results via callback listeners.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl · high confidence

The model checker now uses a new \TransitionExecutor\ (TREX) abstraction in \tla-bmcmt/trex\ to manage symbolic execution. This introduces support for path constraints via \ConstrainedTransitionExecutor\, allowing users to enforce conditions at specific execution depths, and enables selective execution through \FilteredTransitionExecutor\, which filters transitions and invariants using regular expressions. The change also provides distinct execution contexts for incremental and offline SMT solvers (\IncrementalExecutionContext\ and \OfflineExecutionContext\), improving how the checker manages solver state and snapshots during verification.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex · high confidence

The \tlair/src/main/scala/at/forsyte/apalache/tla/types\ package now includes core infrastructure for the type system, introducing \EqClass\ for tracking equivalent type variables, \Substitution\ for applying type variable mappings, \TypeUnifier\ for solving type constraints, and \TypeVarPool\ for generating fresh variables. It also adds \ModelValueHandler\ to parse and construct special model value strings (e.g., \name\_OF\_Type\) and exposes \tla\ (a strict \ScopedBuilder\) and \tlaU\ (a scope-unsafe builder) for constructing TLA+ expressions with type and scope checking.

tlair/src/main/scala/at/forsyte/apalache/tla/types · high confidence

The \tlair\ module introduces new Scala objects (\Booleans\, \Integers\, \EUF\) that provide type-safe constructors for TLA+ formula terms. These additions define specific expression types—such as logical operators (And, Or, Implication), arithmetic operations (Plus, Minus, Lt), and uninterpreted function handling (Apply, DeclareFun)—with built-in runtime sort validation to ensure arguments match expected types. This change establishes a structured, type-checked API for building and manipulating TLA+ intermediate representations within the library.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/formulas · high confidence

The project has been rebranded from 'dach' to 'Apalache', a symbolic model checker for TLA+, with updated documentation, licensing, and contributor records to reflect this identity. To streamline local development, a Nix flake (\flake.nix\) and \direnv\ configuration (\.envrc\) have been introduced, providing a reproducible shell environment with Java 25 and SBT, while the Makefile has been restructured to offer user-friendly targets for building, testing, and formatting the codebase.

(repo-wide) · high confidence

The JSON-RPC interface now supports saving and recovering execution snapshots, allowing users to roll back a model checking session to a previous state via the new \rollback\ method. This is enabled by \CheckerSnapshotsPerSession\, which manages snapshot history per session and deletes forward branches upon recovery. Additionally, new methods \compact\ (to compact the symbolic trace), \checkInvariant\, \nextStep\, \assumeState\, and \assumeTransition\ are now available, with corresponding parameter parsing and standard JSON-RPC error codes (including a specific code for session not found) implemented in \JsonRpcCodes\ and \JsonParameterParser\.

json-rpc/src/main · high confidence

The intermediate representation for TLA+ operators has been reorganized into a structured hierarchy of specific operator types (such as arithmetic, boolean, set, function, sequence, temporal, and action operators) along with dedicated modules for Apalache-specific hints and internal utilities. This change introduces explicit operator classes with defined arities, precedences, and interpretations, replacing the previous monolithic or less-structured approach. For users, this provides a more robust and type-safe foundation for operator handling, enabling better static analysis, clearer separation between standard TLA+ constructs and Apalache-specific features (like \Gen\, \Guess\, and \Skolem\), and improved support for complex operations like recursive functions and variant types.

tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper · high confidence

A change to existing behaviour in tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules — 417 commits (86 fixs), 53 files.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules · medium confidence · unverified

The legacy \at.forsyte.apalache.tla.lir.convenience\ package object, which provided a \tla\ shortcut for the untyped \Builder\, is now deprecated. Users are instructed to migrate to the new typed builder located in \at.forsyte.apalache.tla.types.tla\, which offers type-safe construction of TLA+ expressions (e.g., \tla.plus(tla.int(2), tla.int(3))\).

tlair/src/main/scala/at/forsyte/apalache/tla/lir/convenience · high confidence

This release addresses several stability and correctness issues in the model checker's output generation and set handling. The PrettyWriter now correctly parenthesizes set-map bodies (e.g., { (e) : x \\in S }) and ensures that hoisting lambda arguments into LET-IN expressions does not alter expression scope, preventing syntactic errors in generated models. Additionally, fixes prevent crashes when folding operators on singleton set literals and correct the rewriting of function sets that have empty domains or co-domains.

.unreleased · high confidence

The distribution launch scripts (apalache-mc and apalache-mc.bat) now automatically probe the Java runtime to apply the --sun-misc-unsafe-memory-access=allow flag when supported, ensuring compatibility with recent Java versions while maintaining support for older runtimes. The scripts also introduce periodic garbage collection via G1GC to prevent memory contention between the JVM and Z3, resolve SANY filesystem race conditions by using a dedicated temporary directory, and avoid setting -Xmx if -XX:MaxRAMPercentage is already provided.

src/universal · high confidence

The Apalache tool now uses a structured command-line interface with distinct subcommands (parse, check, simulate, typecheck, test, config, server, transpile, tracee) instead of a flat argument list. Users will see explicit EXITCODE messages (OK or ERROR) on standard output, and the tool now consistently reports its version and build number via BuildInfo. Configuration errors and unhandled exceptions are handled gracefully, with bug reports generated for the latter, and heap memory exhaustion is caught early with a helpful error message.

mod-tool/src/main/scala/at/forsyte/apalache/tla · high confidence

The type-checking subsystem in the TLA+ module has been refactored to use a new 'Etc' (Embarrassingly simple Type Checker) implementation. This change replaces the previous generic type-checking logic with a dedicated constraint solver that collects and resolves type equations via unification, supporting both monomorphic and polymorphic type inference. The new architecture includes a builder trait for constructing internal expression trees, a translator for converting TLA+ declarations into the Etc intermediate representation, and a substitution mechanism for resolving type aliases. For users, this provides a more robust and structured approach to type checking, improving how type errors are reported and how complex operator signatures are handled.

tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc · high confidence

The model checker now exposes a comprehensive set of configuration options via \ModelCheckerParams\, allowing users to control the bounded model-checking depth (\stepsBound\), enable random simulation with a configurable number of runs (\search.simulation\, \search.simulation.maxRun\), set SMT query timeouts (\timeoutSmtSec\), and choose between \BeforeJoin\ and \AfterJoin\ invariant checking modes. Additionally, the search logic has been refactored to support enumerating multiple counterexamples (\nMaxErrors\) and optionally saving execution traces (\search.outputTraces\), with the \SearchState\ machine now tracking cumulative errors, timeouts, and simulation runs to determine when to continue or stop the search.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search · high confidence

The arena module introduces a new PureArenaAdapter class and a PtrUtil utility object to support an ongoing refactoring of the model-checking arena. PureArenaAdapter acts as a transitional wrapper that delegates operations to a PureArena while maintaining compatibility with the existing SolverContext, facilitating a migration away from the legacy Arena interface. The new PtrUtil object provides helper methods for managing ElemPtrs, including merging pointers, mapping cells to their pointing sets, and handling tuple pointers for Cartesian products, which simplifies the internal representation of set elements and their relationships within the arena.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena · high confidence

The TLA+ analysis engine now uses a new Low-level Intermediate Representation (LIR) to model specifications. This change introduces a sealed expression hierarchy (TlaEx) with typed nodes for values, names, operators, and let-in definitions, replacing the previous structure. It adds automatic, thread-safe unique identifiers (UIDs) to all expressions for precise tracking, and implements a type-tagging system (TypeTag) to enforce type safety during analysis. The update also includes a new ModuleProperty enumeration to track transformation stages (e.g., TypeChecked, Inlined) and a TlaLevelFinder to determine variable levels (const, state, action, temporal) for temporal encoding.

tlair/src/main/scala/at/forsyte/apalache/tla/lir · high confidence

The model checker's internal symbolic memory representation has been refactored to use a new typed cell system. This change introduces the ArenaCell class, which now carries explicit type information (CellT) and provides a direct conversion to the typed builder instructions, replacing the previous scope-unsafe builder usage. Additionally, a new type hierarchy (CellT) is defined to manage symbolic types such as sets, sequences, functions, and infinite sets, ensuring that the model checker's internal state aligns with the typed builder infrastructure.

tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt · high confidence

The preprocessing module has been significantly restructured to improve modularity and correctness. A new AbstractTransformer base class now provides a unified recursive transformation framework for expression passes. The Desugarer has been expanded to handle complex syntactic sugar removal, including multi-dimensional EXCEPT updates, tuple flattening in UNCHANGED actions, and rewriting leadsTo temporal operators. The Inliner has been rewritten to support polymorphic operator inlining with proper type unification and pass-by-name embedding, while the ExprOptimizer introduces new simplifications for set membership, powerset cardinality, and integer ranges. Additionally, the Keramelizer now transforms records and tuples into set comprehensions, and the Normalizer extends negation normal form support to non-Boolean operators.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp · high confidence

The model checker's configuration framework has been restructured with new Guice modules (CheckerModule, ReTLAToVMTModule, TraceeModule) that define distinct pass pipelines for standard checking, ReTLA-to-VMT transpilation, and trace evaluation. A new CheckerExceptionAdapter centralizes error handling, mapping internal exceptions (such as TypingException, SmtEncodingException, and IrrecoverablePreprocessingError) to user-friendly messages with source location context. The ReTLA module introduces a combined language predicate and a dedicated transpilation pass, while the Tracee module adds trace evaluation and bridging passes to the pipeline.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config · high confidence

The model checker now includes a new set of analysis components in the \analyses\ package to optimize performance and correctness. \ExpansionMarker\ identifies expensive set operations (like power sets and function sets) and marks them for expansion, issuing warnings to users when necessary. \ExprGradeAnalysis\ and its supporting store classify expressions by their dependency on state and actions (e.g., constant, state-free, action-bound), enabling the rewriter to cache results more effectively. Additionally, \SkolemizationMarker\ improves the handling of existential quantifiers and \let\-definitions by wrapping skolemizable expressions, which helps avoid incorrect skolemization of definitions used as values and optimizes cardinality checks.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/analyses · high confidence

The model checker now supports new stratified rules for handling finite set operations, including set construction ({e1, ..., ek}), set union (X \\cup Y), and set filtering ({x \\in S: P}). These rules rewrite TLA+ set expressions into arena cells with explicit membership constraints, improving how the backend manages set semantics during bounded model checking. The set filter rule specifically excludes infinite sets (IntSet, NatSet) to prevent unsupported operations.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set · high confidence

The type checker now includes explicit type signatures for a comprehensive set of TLA+ operators, including action, arithmetic, boolean, control, finite set, function, sequence, set, temporal, and variant operators, as well as internal Apalache operators. This change introduces a \FlexibleEquality\ mechanism that allows the type system to compare record types with compatible fields rather than requiring exact structural equality, enabling more flexible type checking for polymorphic operators like \map\, \filter\, and \union\.

tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures · high confidence

The model checker's utility layer now includes new components to support advanced operators and improve internal efficiency. LabelsCache caches expression labels to avoid redundant lookups during repeated transition evaluations. TlaExUtil provides functions to find used names and labels in TLA+ expressions, with specific handling for new operators like FoldSet, FoldSeq, and Repeat to correctly ignore auxiliary let-in definitions. IntTupleIterator and Prod2SeqIterator provide efficient iteration over Cartesian products, which is required for multi-argument operators, with IntTupleIterator using BigInt to prevent overflow errors when enumerating large sets.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util · high confidence

The command-line interface has been restructured around a new \ApalacheCommand\ base class and a unified \ApalacheConfig\ configuration model. This change introduces several new subcommands: \config\ for managing statistics submission, \simulate\ for symbolic simulation, \test\ for quick specification testing, \tracee\ for evaluating expressions over traces, and \transpile\ for generating VMT constraints. The existing \check\ command now supports additional options for SMT solver selection (\--smt-solver\), SMT encoding (\--smt-encoding\), and SMT timeout (\--timeout-smt\). Boolean flags are now parsed more flexibly (e.g., \--debug\ instead of \--debug=true\), and environment variables can override CLI options for settings like \--out-dir\ and \--profiling\. The \server\ subcommand allows running Apalache as a server with configurable port and type (checker or explorer).

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling · high confidence

The TLA+ parser's SANY importer has been restructured from a monolithic implementation into a set of specialized, decoupled components. This change introduces dedicated translators for distinct TLA+ constructs—including \ModuleTranslator\, \OpDefTranslator\, \ExprOrOpArgNodeTranslator\, \AssumeTranslator\, and \SubstTranslator\—which handle the conversion of SANY semantic nodes into the Apalache Intermediate Representation (IR). The refactoring also extracts annotation parsing into a standalone \AnnotationExtractor\ and manages source location tracking via a \SourceStore\. Additionally, the import process now includes a thread-safety wrapper (\SANYSyncWrapper\) to serialize access to the non-thread-safe SANY parser, and a \StandardLibrary\ object to explicitly map standard TLA+ modules and operators to IR equivalents.

tla-parser/src/main · high confidence

The TLA+ analysis pipeline has been restructured from a monolithic implementation into a series of distinct, composable passes (e.g., SanyParser, Configuration, Inline, Prepro, TypeChecker, Priming, Transition). This change introduces a standardized \PassWithOutputs\ interface that automatically writes intermediate module states to the output folder after each step, improving debuggability and allowing for better isolation of transformation logic. Key behavioral updates include the introduction of a dedicated \PrimingPass\ to handle variable priming before inlining, a refactored \ConfigurationPass\ that now performs explicit type-consistency checks for constant overrides from .cfg files, and a new \TemporalPass\ that encodes temporal properties into invariants using a tableau encoding. The parser pass (\SanyParserPassImpl\) has also been extended to support direct loading of .qnt (Quint) and .json (ITF) formats alongside standard .tla files.

passes/src/main · high confidence

The TLA+ type builder in the \typecomp\ package has been restructured to separate scope-unsafe and scope-safe expression construction. A new \ScopeUnsafeBuilder\ allows building typed TLA+ IR expressions without enforcing variable scope correctness, while the \ScopedBuilder\ maintains strict scope and type guarantees. This change introduces new utility objects like \Applicative\ for handling application types, \BuilderUtil\ for common builder operations, and \ParamUtil\ for parameter validation, alongside a \TypeComputationFactory\ to manage operator signatures.

tlair/src/main/scala/at/forsyte/apalache/tla/typecomp · high confidence

The passes in the \tla-bmcmt\ module have been restructured to use a trait-based interface (e.g., \AnalysisPass\, \BoundedCheckerPass\, \VCGenPass\) with corresponding implementations (e.g., \AnalysisPassImpl\, \BoundedCheckerPassImpl\, \VCGenPassImpl\). This change introduces a new \AnalysisPass\ that performs skolemization and expression grading, and a \VCGenPass\ that generates verification conditions from invariants and views. The \BoundedCheckerPass\ now explicitly supports multiple SMT encodings (OOPSLA19, Arrays, FunArrays) and solver backends, with configuration for tuning parameters and remote execution contexts. A new \ReTLAToVMTTranspilePass\ has been added to support transpilation to the VMT format. These changes improve modularity and allow for more flexible configuration of the model checking process.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes · high confidence

The caching layer in the model checker has been restructured to introduce context-aware snapshots and recovery capabilities. New base classes, AbstractCache and SimpleCache, now manage cache entries with a context level, allowing entries to be automatically filtered out when the context is popped. Corresponding snapshot classes (AbstractCacheSnapshot, SimpleCacheSnapshot, EqCacheSnapshot) enable the cache state to be saved and restored, squashing intermediate contexts. Specific caches like DefaultValueCache, IntValueCache, ModelValueCache, IntRangeCache, RecordDomainCache, and ExprCache have been updated to leverage this new infrastructure, ensuring that cached values are correctly managed across different context levels during symbolic execution.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches · high confidence

The pass execution engine has been restructured to use a new \PassChainExecutor\ that manages a sequence of passes defined in \ToolModule\, communicating state between them via a \DerivedPredicates\ trait rather than modifying the module directly. Passes now return a \PassResult\ (either a transformed module or a \PassFailure\ with error data and exit codes), and the system uses an \ExceptionAdapter\ to convert exceptions into user-friendly messages. Additionally, logging is now configured programmatically via \LogbackConfigurator\ to ensure consistent behavior across environments, with detailed logs written to \detailed.log\ and warnings/errors printed to the console.

mod-infra/src/main · high confidence

The model checker now includes dedicated stratified rewriting rules for Boolean conjunction (AND) and disjunction (OR). These new rules in the \stratifiedRules.bool\ package handle the translation of logical operators into the underlying SMT solver representation. By default, the rules translate AND/OR expressions directly into SMT conjunctions and disjunctions, but they also support an optional short-circuiting mode that translates these operators into chains of IF-THEN-ELSE expressions, mimicking the lazy evaluation behavior found in tools like TLC. This change provides a more structured and potentially more efficient way to handle Boolean logic during the rewriting phase.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool · high confidence

The TLA+ typechecker now includes new integration components that enforce type safety during transformations and apply inferred types to the TLA+ IR. TypeWatchdogTransformationListener acts as a safeguard by throwing a TypingException if any expression or declaration loses its type tag during a transformation, ensuring that typed nodes remain typed throughout the pipeline. RecordingTypeCheckerListener collects the mapping of unique identifiers to their inferred monotypes, while TypeRewriter uses this map to annotate TLA+ expressions and declarations with their corresponding types, including special handling for record field names in string values and tuple indices in EXCEPT expressions.

tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/integration · high confidence

Added Quint test for labeled state transitions; Added SMT solver context tests for CVC5 and cross-solver parity; Added TLA+ model checker test suite; Added TLA+ specification test resources for the assignment solver; Added TLA+ specifications for distributed algorithms; Added TLA+ test cases for sanitizer validation; Added TLA+ tests for the FoldExcept anti-pattern; Added TLA+ tutorial and verification tests for binary search; Added comprehensive test coverage for preprocessing passes; Added integration test infrastructure and TLA+ test suite runner; Added property-based testing generators for TLA+ type components; Added property-based tests and generators for the TLA+ intermediate representation; Added property-based tests for the TLA+ operator builder; Added test coverage for TLA+ IR transformations; Added test resources for TLA+ assignment solver and SMT integration; Added test suite for SANY importer and pretty writer precedence; Added tests for ChangeListener and DisjointSets; Added tests for CmdExecutor and TransExplorer services; Added tests for JSON-RPC service and parameter parsing; Added tests for RegionTree and SourceStore; Added tests for SMT-free symbolic transition extraction and symbolic transition generation; Added tests for TLA+ model checker analyses; Added tests for TLA+ type checking and TLC config import; Added tests for VMT rules and support utilities; Added tests for concurrent tool isolation and command configuration validation; Added tests for stratified rules support caches and oracles; Added tests for the pass chain executor; Added type-annotated TLA+ tests for the Bakery algorithm; Added unit tests for stratified rewriting rules; Added unit tests for the Type1 parser, constraint solver, and EtcExpr translation; Added unit tests for the transition executor (TREX); Expanded test coverage for SMT encodings and model checking components; Expanded test suite for TLA+ specifications in test/tla.

The project has migrated its build system from Maven to SBT, establishing a new build configuration with SBT version 1.12.11. This change introduces a centralized dependency management file (Dependencies.scala) and a new plugins.sbt, incorporating numerous library updates such as Jetty 12.1.10, ZIO 1.0.18, Guice 7.0.0, and Logback 1.5.32. The migration also adds several SBT plugins including sbt-assembly, sbt-docker, sbt-native-packager, and sbt-unidoc to support packaging, testing, and documentation generation.

project · high confidence

The project build has been migrated from Maven to SBT, introducing a new \build.sbt\ configuration that sets the Scala version to 2.13.18 and targets Java 21 for artifact compatibility. This change includes the addition of the \sbt-changeling\ plugin for release pipelines and updates the \highlight.js\ dependency for TLA+ syntax highlighting in documentation.

(dependencies) · high confidence

Written by watchdog.canine.dev from the codebase's own history, inside the signed delivery this page is composed from.

• CAI 71 → 70 (-1.4)
• Rubric changed (rubric-2026.09.8 → rubric-2026.09.16) — scores are not directly comparable.

• Code Health 84 → 84 (-0.0)
• Architecture 98 → 88 (-9.6)
• Maturity 78 → 78 (+0.1)
• Readiness 68 → 63 (-5.4)
• Security 66 → 70 (+4.2)

• Documentation: no installation or build instructions (README.md)
• Hotspot: json-rpc/src/main/scala/com/github/apalachemc/apalache/jsonrpc/JsonRpcServer.scala (json-rpc/src/main/scala/com/github/apalachemc/apalache/jsonrpc/JsonRpcServer.scala)
• Hotspot: passes/src/main/scala/at/forsyte/apalache/tla/typecheck/TypeCheckerTool.scala (passes/src/main/scala/at/forsyte/apalache/tla/typecheck/TypeCheckerTool.scala)
• Hotspot: tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala (tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala)
• Hotspot: tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala (tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala)
• Hotspot: tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala (tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala)
• Hotspot: tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala (tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala)
• Off-boarding risk: anonymized user #1

• Dependency hygiene PARTLY measured — npm pinning read, dependency currency not (no committed lockfile, so no resolved version to grade)
• Documentation: no installation or build instructions (docs/src/adr/004adr-annotations.md)
• Documentation: no installation or build instructions (docs/src/index.md)
• Documentation: no project overview (docs/src/adr/004adr-annotations.md)
• Documentation: no usage examples (docs/src/adr/004adr-annotations.md)
• Duplicated block (6 lines × 2) (script/explorer.py)
• Off-boarding risk: anonymized user #1
• Projects may be oversized for their cohesion
• Scanner failed to run — not a clean result

• 3 commits — 1 feature/other, 2 fixes

• tla-io/src — 2 commits
• (repo) — 1 commit

• fix: Merge pull request #3485 from apalache-mc/igor/fix-printer-010
• fix: fix parenthesizing of the expressions again
• change: fix the comment

• Unchanged — 0 containers · 1 contexts · 0 edges

Written by watchdog.canine.dev from the codebase's own history, inside the signed delivery this page is composed from.

apalache-mc/apalache was measured the same way every project in this corpus was: the same rubric, at a pinned commit, with the result published in full. Point a surveyor at a repository you know and see whether you agree with it.