Formal Model Checking
Concurrency, retries and crashes can break invariants that ordinary tests miss. Check small finite-state models, retain counterexamples and bounds, and connect useful traces to implementation tests without claiming a whole-program proof.
Install
Choose a supported route below. Package contents, agent registration and runtime dependencies can differ between installers.
-
Claude Code via this marketplace /plugin install formal-model-checking@netresearch-claude-code-marketplaceFirst add the marketplace once in Claude Code:
/plugin marketplace add netresearch/claude-code-marketplace. Then install the selected plugin. For setup and installation scopes, seeClaude Code plugin setupA plugin can include several skills and additional components. -
npx interactive skill selection npx skills add https://github.com/netresearch/formal-model-checking-skillRequires Node.js 22.20+. Run from the target project, then choose the source skills and agents in the installer. Uses the skills CLI from
skills.shInstalls skill instructions. Extra plugin hooks, commands and external runtime tools are not installed by this route. -
composer skills:add PHP project, direct source composer skills:add netresearch/formal-model-checking-skillInstall and activate netresearch/composer-agent-skill-plugin first; approve the selected source's skill registration. Provided by
netresearch/composer-agent-skill-pluginPins source repositories without a Packagist package and records them incomposer.skills.lock. Runtime dependencies remain separate.
What you can do with it
- An invariant depends on competing requests, retries or recovery.
- Process loss can interrupt a sequence of durable operations.
- A finite-state checker or TLA+/TLC result needs validation.
- A design needs systematic state exploration or a counterexample.
What you get back
- A precise property, model, configuration and explicit bounds and assumptions.
- A completed search or an interpretable execution violating the property.
- Valid negative controls and reachability evidence supporting positive claims.
- A model-to-code mapping when code exists; runtime evidence when implementation verification is requested.
- Excluded paths and incomplete checks.
What it expects in your project
- A concrete design claim, protocol or implementation boundary.
- Relevant source and storage semantics when implementation mapping is requested.
- A suitable available checker or interpreter to execute the chosen model.
- Python 3.11 or later for the repository's standard-library fixture tests.