ModelChecker
A programmatic framework for implementing and comparing modular semantic theories, powered by the Z3 SMT solver.
ModelChecker turns a semantic theory into executable constraints. Given a set of premises and conclusions, it searches for a countermodel — a model satisfying the premises while falsifying the conclusions — and prints that model in readable form. Where no countermodel exists, the inference is valid in the theory under test, up to the finite state space searched.
The framework is theory-agnostic. Four semantic theories ship with the package, and new theories can be written, tested, and shared using the same interfaces.
Features
- Automated countermodel search — discovers countermodels to invalid inferences, or reports their absence
- Modular operator architecture — load only the operators an analysis needs, with dependency resolution across subtheories
- Hyperintensional semantics — distinguishes necessarily equivalent propositions by their verifier and falsifier sets
- Model iteration — enumerate multiple non-isomorphic models for a single example
- Theory comparison — run the same inference against several theories side by side
- Dual solver backends — Z3 by default, with optional cvc5
- Theory library — four ready-to-use theories that double as templates for new ones
Installation
pip install model-checker
For notebook integration:
pip install model-checker[jupyter]
The optional cvc5 backend is a separate package:
pip install cvc5
For development:
git clone https://github.com/benbrastmckie/ModelChecker.git
cd ModelChecker/code
pip install -e .
Requires Python 3.10 or later. NixOS users should use nix-shell rather than pip; see
Developer Setup.
Full instructions are in the
Installation Documentation.
Quick Start
Generate a project preloaded with a theory and its examples:
model-checker -l logos # hyperintensional truthmaker semantics
model-checker -l exclusion # unilateral semantics
model-checker -l imposition # Fine's counterfactual semantics
model-checker -l bimodal # temporal-modal logic
Then run an examples module:
model-checker examples.py
Each example is a triple of premises, conclusions, and settings. This one tests counterfactual
antecedent strengthening: given that A is false and that C would hold if A did, must C
also hold if A and B both did?
CF_CM_1_premises = ['\\neg A', '(A \\boxright C)']
CF_CM_1_conclusions = ['((A \\wedge B) \\boxright C)']
CF_CM_1_settings = {
'N': 4, # bit-width: the state space has 2^N states
'contingent': True, # atomic propositions must be contingent
'iterate': 2, # find two non-isomorphic models
'max_time': 10, # solver timeout in seconds
}
It is not valid, and the framework says so by exhibiting a countermodel (abridged below; the particular model found varies between runs):
EXAMPLE CF_CM_1: there is a countermodel.
Premises:
1. \neg A
2. (A \boxright C)
Conclusion:
3. ((A \wedge B) \boxright C)
State Space:
#b0000 = □
#b0001 = a
#b0010 = b
#b0011 = a.b (world)
#b0100 = c
#b0101 = a.c (world)
#b0110 = b.c (impossible)
#b0111 = a.b.c (impossible)
#b1000 = d
#b1001 = a.d (impossible)
#b1010 = b.d (world)
#b1011 = a.b.d (impossible)
#b1100 = c.d (world)
#b1101 = a.c.d (impossible)
#b1110 = b.c.d (impossible)
#b1111 = a.b.c.d (impossible)
The evaluation world is: b.d
INTERPRETED PREMISES:
...
2. |(A \boxright C)| = < {b.d, c.d}, {a.b, a.c} > (True in b.d)
|A|-alternatives to b.d = {c.d}
|C| = < {b, b.d, d}, {a.c} > (True in c.d)
INTERPRETED CONCLUSION:
3. |((A \wedge B) \boxright C)| = < {}, {a.b, a.c, b.d, c.d} > (False in b.d)
|(A \wedge B)|-alternatives to b.d = {a.c}
|C| = < {b, b.d, d}, {a.c} > (False in a.c)
Strengthening the antecedent changes which worlds are relevant to the evaluation. A match would light if it were struck; it does not follow that it would light if it were struck while wet.
Propositions print as < verifiers, falsifiers >, and states as fusions of atomic states, so
a.c is the fusion of a and c. Formulas use LaTeX commands (\boxright, \wedge), which are
also how they are written in source; see the
Formula Reference.
Semantic Theories
| Theory | Semantics | Operators |
|---|---|---|
| Logos | Hyperintensional truthmaker semantics with bilateral verifier/falsifier sets | 18 |
| Exclusion | Bernard and Champollion's unilateral semantics, where negation arises from a primitive exclusion relation | 4 |
| Imposition | Kit Fine's counterfactual semantics, using a primitive imposition relation on states | 13 |
| Bimodal | Temporal-modal logic where worlds are histories mapping times to world states | 17 |
The Theory Library documents how theories are registered and how to contribute a new one.
The Logos Theory
The Logos provides a bilateral hyperintensional semantics for a formal language of thought. States are drawn from a finite mereology, propositions are pairs of verifier and falsifier sets, and necessarily equivalent propositions may differ in subject matter. Its operators are organized into four subtheories that can be loaded independently:
| Subtheory | Operators |
|---|---|
| Extensional | \neg (¬), \wedge (∧), \vee (∨), \rightarrow (→), \leftrightarrow (↔), \top (⊤), \bot (⊥) |
| Modal | \Box (□), \Diamond (◇), \CFBox, \CFDiamond |
| Constitutive | \leq (≤, ground), \sqsubseteq (⊑, essence), \equiv (≡, identity), \preceq (≼, relevance), \Rightarrow (reduction) |
| Counterfactual | \boxright (□→, would), \diamondright (◇→, might) |
Several operators are defined rather than primitive: A ◇→ B abbreviates ¬(A □→ ¬B),
\CFBox A abbreviates ⊤ □→ A, \CFDiamond A abbreviates ⊤ ◇→ A, and A \Rightarrow B is the
conjunction of ground and essence. Additional operators are under active development.
How Theories Are Defined
A theory supplies four things: a semantics class, operator classes, a proposition class, and a model structure. The semantics defines the primitives and frame constraints; each operator defines its own truth, falsity, verification, and falsification conditions as Z3 constraints.
Semantic primitives.
LogosSemantics
extends
SemanticDefaults
and declares three Z3 functions — verify and falsify, relating states to sentence letters, and
possible, marking which states are possible. States are bit vectors of width N, so fusion is
bitwise OR and parthood is fusion-identity, both inherited from SemanticDefaults. Frame
constraints require that possibility is downward closed under parthood and that the evaluation
world is a world — a possible state that is maximal with respect to compatibility.
Derived relations. On that basis LogosSemantics builds compatible, maximal, is_world,
max_compatible_part, and is_alternative. The last two carry the counterfactual semantics: an
alternative world to w under y contains y together with a maximal part of w compatible
with it.
Recursive evaluation. true_at, false_at, extended_verify, and extended_falsify bottom
out on sentence letters and otherwise delegate to the operator at the root of the sentence.
Operators. The
counterfactual operators
illustrate the pattern. A □→ B is true at w when, for every verifier x of A and every
x-alternative u to w, B is true at u; it is false at w when some verifier x of A
has an x-alternative u at which B is false. Because the alternatives quantified over depend
on which verifier of the antecedent is considered, the operator is hyperintensional: substituting
a necessarily equivalent antecedent can change the result.
Full contracts are in the Theory Architecture guide.
Configuration
Settings are set per example in the settings dictionary, and may be overridden by command-line
flags.
| Setting | Flag | Effect |
|---|---|---|
N |
— | Bit-width for states; the space contains 2^N states |
max_time |
— | Solver timeout in seconds |
iterate |
— | Number of non-isomorphic models to find |
contingent |
-c |
Require atomic propositions to be contingent |
non_empty |
-e |
Require non-empty verifier and falsifier sets |
non_null |
-n |
Exclude the null state from verifying or falsifying |
disjoint |
-d |
Require atomic propositions to be disjoint; the exact constraint is theory-specific |
maximize |
-m |
Compare theories on the same examples |
solver |
--z3 / --cvc5 |
Select the SMT backend |
print_impossible |
-i |
Include impossible states in the display |
print_constraints |
-p |
Show the constraints given to the solver |
print_z3 |
-z |
Show raw solver output |
save_output |
-s |
Save results; -s markdown or -s json selects a format |
sequential |
-q |
Prompt to save each model individually |
align_vertically |
-a |
Display temporal models top to bottom |
Run model-checker --help for the full command-line interface. For theory comparison and
multi-theory setups, see the
Tools Guide.
Development
Clone the repository and work from the code/ directory. These scripts do not require the package
to be installed:
| Script | Purpose |
|---|---|
./dev_cli.py examples.py |
Run the CLI against local source rather than the installed package |
./run_tests.py |
Unified runner for example, unit, and package tests |
./run_jupyter.sh |
Start Jupyter with ModelChecker available, inside nix-shell |
./jupyter_link.py |
Symlink local source into user site-packages for notebook use |
dev_cli.py puts the local src/ directory at the front of sys.path, so edits take effect
immediately; it also accepts --iso-debug for isomorphism debugging. run_tests.py auto-detects
whether a target is a theory or a component:
./run_tests.py # everything
./run_tests.py --examples # example tests only
./run_tests.py --unit logos # unit tests for the logos theory
./run_tests.py logos modal # a single subtheory
./run_tests.py iterate builder # multiple components
Tests can also be run directly with pytest:
PYTHONPATH=src pytest tests/ -v
Contributions are welcome. See the Development Guide for workflow, coding standards, and testing requirements.
Documentation
- User Documentation — installation, usage, and guides
- Technical Documentation — architecture, standards, and contracts
- Theory Library — theory specifications and the contract for new theories
- Academic Background — related research
Citation
If you use ModelChecker in your research, please cite:
Brast-McKie, B. (2025). Model-Checker: A Programmatic Semantics Framework. https://github.com/benbrastmckie/ModelChecker
The theories implemented in the framework are developed in:
- Brast-McKie, B. (draft). "The Construction of Possible Worlds".
- Brast-McKie, B. (2025). "Counterfactual Worlds". Journal of Philosophical Logic.
- Brast-McKie, B. (2021). "Identity and Aboutness". Journal of Philosophical Logic, 50, 1471–1503.
Support
- Issues — bug reports and feature requests
- Discussions — questions and ideas
License
GPL-3.0. See LICENSE.
1 maintainer
Metadata
1 maintainer
Release files for model-checker 1.3.4
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | |
|---|---|---|---|
| model_checker-1.3.4.tar.gz | 950.5 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| model_checker-1.3.4-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 2.1 MB
Release files / model_checker-1.3.4.tar.gz
| Download URL | model_checker-1.3.4.tar.gz |
|---|---|
| Size | 950.5 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
d66f54c3e2d65c455f703a4fa88241a7f808a0a441a0d161a2bd011a6dd6241d
|
|
BLAKE2b-256 checksum How to use checksums |
923edb9b5e762a221db7f088373e578c69f91f24245e58a3e936615397cd1f71
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/7.0.0 CPython/3.13.14
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Aug 25, 2026.
Transparency logRelease files / model_checker-1.3.4-py3-none-any.whl
| Download URL | model_checker-1.3.4-py3-none-any.whl |
|---|---|
| Size | 1.2 MB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
d1766fdd877b860b6ce02cd3c56a08dee7963b84f6d66e1ac6052022b43e998a
|
|
BLAKE2b-256 checksum How to use checksums |
cfc872844a1dc97bbcceb2cb581fc5097db351413e9f089e7db984b89a7005c6
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/7.0.0 CPython/3.13.14
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Aug 25, 2026.
Transparency log
