model-checking

Jupyter kernel for TLA⁺

Generate (message) sequence diagrams from TLA+ state traces

CoreIR Symbolic Analyzer

Model-based testing tool

The CBMC starter kit makes it easy to add CBMC verification to a software project.

A simple REPL for TLA+.

A Python-like programming language for testing and experimenting with concurrent programs.

Open-source, agent-agnostic RTL formal verification skill library for AI coding agents: JasperGold FPV, SVA, proof optimization, and TCL workflows for Claude Code, Codex, Gemini CLI, and Cursor.

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

BehaVerify: A Formal Verification Tool for Behavior Trees

A multi-formalism, multi-solution model-checker centered on the language GAL

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

Read-only mirror of the Klever Git repository

Baum-Welch for all kind of Markov models

Equilibrium Verification Environment (EVE) is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems.

Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

The interface between probabilistic model checking and data-driven policy learning.

Intrepyd Model Checker

LSVerifier - Large Systems Verifier

Unified Maude model-checking tool