analint

A Python DSL for declaring and verifying how a system behaves.

Requirements live in Word, Confluence, and Miro — readable by humans, but impossible to check for contradictions, diff, or hand to an AI agent. Code is the other extreme: too low-level. analint sits in the middle: Python that reads like a specification and checks like one.

checkout = Action(
    pre=[
        Wallet.balance >= Order.total,
        Order.status == OrderStatus.PENDING,
    ],
    effect=[
        Set(Order.status, OrderStatus.PAID),
        Subtract(Wallet.balance, Order.total),
    ],
)

sc_broke = Scenario(
    name="Insufficient balance",
    action=checkout,
    given=[
        Order(id="o1", total=50.0, customer_id="c1"),
        Wallet(balance=10.0, customer_id="c1"),  # 10 < 50 → blocked
    ],
    expected=Expect.FAIL,
)

analint examples/ecommerce/

SCENARIOS
  PASS  checkout/happy           (6 rules)
  PASS  checkout/no-funds        (6 rules)
         ↳  PRE failed: Wallet.balance >= Order.total
         ↳  correctly blocked — rules rejected this data as expected

It is not limited to business analytics: the same primitives describe game rules and narrative consistency — see examples/cloak/, the classic Cloak of Darkness IF benchmark expressed as a verifiable spec.

Installation

pip install analint
# or with uv:
uv add analint

Quick start

Create spec.py and run analint . in the same directory.

from analint import Entity, Action, Scenario, Spec, Expect

class Item(Entity):
    price: float
    stock: int

class Budget(Entity):
    amount: float

buy = Action(
    pre=[
        Item.price > 0,
        Budget.amount >= Item.price,
    ],
)

sc_ok = Scenario(
    name="Happy path",
    action=buy,
    given=[Item(price=10.0, stock=5), Budget(amount=20.0)],
)

spec = Spec(id="shop", name="Shop", actions=[buy], scenarios=[sc_ok])

The model is what Spec lists; Item and Budget join it because buy uses them.

ids are derived from variable names (buy, sc_ok) — set id= explicitly only when you want a different one.

DSL reference

The DSL has three layers: state (Entity, Event), constraints (Invariant, predicates), and transitions (Action, Lifecycle). Scenarios and Flows tie them together with concrete examples.

Entity

Typed system state. Annotate fields normally; class-level access returns a FieldDescriptor usable in predicate expressions. Use Field(...) for constraints on one value, and attach a Lifecycle(...) directly to a field whose states have declared transitions.

from enum import StrEnum
from analint import Entity, Field, Lifecycle

class OrderStatus(StrEnum):
    PENDING   = "pending"
    PAID      = "paid"
    CANCELLED = "cancelled"

class Order(Entity):
    status: OrderStatus = Lifecycle(
        initial=OrderStatus.PENDING,
        transitions={
            OrderStatus.PENDING: [OrderStatus.PAID, OrderStatus.CANCELLED],
            OrderStatus.PAID: [OrderStatus.CANCELLED],
        },
        terminal=[OrderStatus.CANCELLED],
    )
    total: float = Field(gt=0)                 # required, must be positive
    customer_id: str

Order.total                           # class level → FieldDescriptor (for predicates)
Order(total=50.0, customer_id="c1").total   # instance level → 50.0

Field(default, ge=..., gt=..., le=..., lt=...) validates constructed instances, checks post-action values, and supplies finite numeric bounds to the reachability engine. Field(default, values=[...]) declares an explicit finite scalar domain. With saturate=True, numeric values clamp at the declared ge/le thresholds instead of making the transition invalid.

Predicates

Comparison operators on fields build predicate objects; combinators are plain functions:

Order.total > 0
Order.status == OrderStatus.PENDING
Wallet.balance >= Order.total          # field-to-field comparison

from analint import And, Or, Not, Implies, In, IsNull, IsNotNull

And(Order.total > 0, Wallet.balance >= Order.total)
Implies(Hook.holds_cloak, Not(Player.has_cloak))               # if A then B
In(Order.status, [OrderStatus.PAID, OrderStatus.CANCELLED])

Arithmetic over fields builds expression nodes — including named, reusable ones (Quint-style derived values):

Wallet.balance - Order.total >= 0
total_supply = Alice.coins + Bob.coins + Eve.coins   # named expression
supply_fits  = AlwaysHolds(total_supply <= MAX_SUPPLY)

Predicates are values — name them and reuse them:

board_is_active = Board.status == BoardStatus.ACTIVE

create_card  = Action(pre=[board_is_active, ...])
archive_card = Action(pre=[board_is_active, ...])

Invariant

A relation that must hold in every state — checked before an action and re-checked after its effects. Put constraints involving one field on Field(...); use Invariant for relationships between fields or entities.

from analint import Implies, Invariant

delivered_means_paid = Invariant(
    Implies(
        Order.status == OrderStatus.DELIVERED,
        Payment.status == PaymentStatus.CAPTURED,
    ),
    label="A delivered order must have a captured payment",
)

An invariant is skipped in scenarios whose given does not include the entities it references.

Action

A state transition: what must hold before (pre), what changes (effect), and what must hold after (post).

from analint import Action, Set, Subtract

checkout = Action(
    name="Customer Checkout",
    pre=[
        Wallet.balance >= Order.total,
        Product.stock > 0,
        Order.status == OrderStatus.PENDING,
    ],
    effect=[                                       # facts about the next state
        Set(Order.status, OrderStatus.PAID),
        Subtract(Wallet.balance, Order.total),
        Subtract(Product.stock, 1),
    ],
    post=[Order.status == OrderStatus.PAID],       # optional double-entry check
    emits=[OrderPlaced(order_id=Order.id, total=Order.total, customer_id=Order.customer_id)],
)

Effects are simultaneous facts, not a program. Every right-hand side is evaluated against the pre-state; the order of the list carries no meaning; two effects on the same field are a structural error.

Current semantic boundary: event-driven causality is modelled through state, not a dispatch primitive.

Parameterized actions

A family of similar transitions is one declaration over finite domains — never a host-language loop:

from analint import Param

src    = Param("src", AliceCoins, BobCoins, EveCoins)
dst    = Param("dst", AliceCoins, BobCoins, EveCoins)
amount = Param("amount", ge=1, le=3)   # integer range — same vocabulary as Field

send = Action(
    params=[src, dst, amount],
    where=[src != dst],
    pre=[src.coins >= amount, dst.coins <= MAX_BALANCE - amount],
    effect=[Subtract(src.coins, amount), Add(dst.coins, amount)],
)

The engine expands every binding that satisfies where into a concrete action (send(src=AliceCoins, dst=BobCoins, amount=2)); traces and reports use the parametric names. A scenario picks one binding: action=send.bind(src=BobCoins, dst=EveCoins, amount=2).

Bounded multiplicity

Scope declares a fixed finite set of identified instances of one entity type. Instance refs work in predicates and effects, and can be a Param domain:

from analint import Absent, Present, Scope

class Account(Entity):
    balance: int = Field(0, ge=0, le=5)

accounts = Scope(Account, keys=["alice", "bob", "eve"])
alice = accounts["alice"]

src = Param("src", accounts)
dst = Param("dst", accounts)

transfer = Action(
    params=[src, dst],
    where=[src != dst],
    pre=[src.balance >= 1],
    effect=[Subtract(src.balance, 1), Add(dst.balance, 1)],
)

alice_pays_bob = Scenario(
    action=transfer.bind(src=alice, dst=accounts["bob"]),
    given=[
        alice(balance=3),
        accounts["bob"](balance=0),
        Absent(accounts["eve"]),
    ],
)

alice_exists = Present(alice)

The universe is fixed, but membership is explicit. A normal scoped snapshot is present; Absent(ref) marks an allocated slot as absent; Present(ref) is a predicate usable in guards and queries. In scenarios, omitted scoped slots are also absent. Reachability defaults every scoped slot to present unless given=[Absent(ref)] says otherwise. Field reads and ordinary effects on an absent slot are rejected.

Create(ref, **fields) and Delete(ref) change that membership as next-state facts, symmetric to Set over a value:

from analint import Create, Delete

open_account = Action(effect=[Create(accounts["eve"], balance=0)])  # eve must be absent
close_account = Action(effect=[Delete(alice)])                       # alice must be present

Create requires the slot absent and makes it present (unspecified fields take their defaults); Delete requires it present and makes it absent. The mismatched pre-state is rejected before any effect runs, so Expect.FAIL covers it. A slot's presence may change at most once per action, and the same slot may not be both (de)allocated and written by Set/Add/Subtract. The key universe stays fixed, so reachability, quantifiers and aggregates simply range over whichever slots are present in each state.

Finite quantifiers

Bound introduces a named variable over a Scope; ForAll and Exists remain explicit predicate AST nodes and work in invariants, action guards, scenario assertions, and reachability queries:

from analint import Bound, Count, Exists, ForAll, Max, Min, Sum

account = Bound("account", accounts)

all_balances_valid = AlwaysHolds(
    ForAll(account, account.balance >= 0)
)

someone_is_full = Reachable(
    Exists(account, account.balance == 5)
)

total_balance = Sum(account, account.balance)
nonempty_accounts = Count(account, account.balance > 0)
balance_range = Max(account, account.balance) - Min(account, account.balance)

Quantifiers and aggregates are finite and exhaustive over the present instances in the registered scope. Aggregate nodes are ordinary arithmetic expressions: they can be compared, composed with field math, used in effect right-hand sides, and checked by the reachability engine. Over an empty present set, ForAll is true, Exists is false, Count and Sum are zero, while Min/Max report an evaluation error.

Event

An observable domain fact, with a typed payload. Emitting binds payload fields to expressions over the state (the kernel materialises them). An action's pre may constrain an event payload by referencing the event's fields (the event instance lives in the scenario's given):

from analint import Event

class OrderPlaced(Event):
    order_id: str
    total: float

checkout = Action(..., emits=[OrderPlaced(order_id=Order.id, total=Order.total)])

notify_vip = Action(
    pre=[OrderPlaced.total > 100],     # payload condition
    effect=[Add(Manager.alerts, 1)],
)

The linter validates payload bindings (fields exist, types match). Emitting an event does not trigger another action — event-driven causality is modelled through state (see examples/fulfillment, a saga chained via status fields).

Lifecycle

Valid states of an entity field and the allowed transitions between them. The lifecycle is declared as the field's default, so the state definition, initial value, transitions, and terminal states stay together.

class Order(Entity):
    status: OrderStatus = Lifecycle(
        initial=OrderStatus.PENDING,
        transitions={
            OrderStatus.PENDING: [OrderStatus.PAID, OrderStatus.CANCELLED],
            OrderStatus.PAID: [OrderStatus.CANCELLED],
        },
        terminal=[OrderStatus.CANCELLED],
    )

terminal states have teeth: an entity whose lifecycle field is in a terminal state cannot be modified by any action, and a transition out of a terminal state is a structural error.

Scenario

A concrete example: initial state, one action, expected outcome.

from analint import Scenario, Expect, Assert, Emitted

sc_happy = Scenario(
    name="Successful purchase",
    action=checkout,
    given=[
        Order(id="o1", total=50.0, status=OrderStatus.PENDING, customer_id="c1"),
        Wallet(balance=100.0, customer_id="c1"),
        Product(stock=5, price=50.0, name="Widget"),
    ],
    then=[
        Order.status == OrderStatus.PAID,
        Wallet.balance == 50.0,
        Emitted(OrderPlaced),
    ],
    expected=Expect.PASS,
)

expected=Expect.FAIL documents a blocked path: the scenario is correct when at least one rule rejects the data.

For an event-payload scenario, put the event instance in given — its payload is then visible to pre. This checks one local transition:

Scenario(action=notify_vip, given=[OrderPlaced(order_id="o1", total=500.0), Manager(alerts=0)])

Flow

An ordered, executed journey: each action runs through the same transition kernel — its post-state feeds the next — and checkpoints (Assert / Emitted) interleaved in steps are checked against the state reached so far. The first rejected action or failed checkpoint fails the flow (and the run) with a trace; a reached state that breaks an invariant fails it too.

from analint import Flow, Assert, Emitted

purchase_flow = Flow(
    given=[Cart(items=0), Wallet(balance=100)],
    steps=[
        add_item,
        Assert(Cart.items == 1),
        checkout,
        Assert(Order.status == OrderStatus.PAID),
        Emitted(OrderPaid),
    ],
    description="Full customer purchase journey",
)

given= is the initial state — a partial snapshot (the same one a scenario uses): only the listed entities are present, unspecified Scope slots are absent, and a step that needs an unlisted entity is rejected. It is required; given=[] means an empty world and is useful only when the flow creates everything it needs.

Reachability queries

Scenarios check states you thought of. Queries explore every reachable state (BFS over the model) and answer questions you can't answer by hand — each verdict comes with a trace:

from analint import Reachable, Unreachable, AlwaysHolds, NoDeadEnd, DeadActions

bridge_is_reachable = Reachable(Quest.bridge_crossed)
no_softlock         = NoDeadEnd(goal=Quest.bridge_crossed)
hp_never_negative   = AlwaysHolds(Hero.hp >= 0)
no_gold_from_air    = Unreachable(Hero.gold > 6)     # regression guard
every_action_used   = DeadActions()

QUERIES
  PASS  bridge_is_reachable        (Reachable, 9 states)
         ↳ reachable: buy_sword → fight_troll → cross_bridge
  FAIL  no_softlock                (NoDeadEnd, 9 states)
         ↳ dead end: after buy_potion the goal can no longer be reached
  FAIL  hp_never_negative          (AlwaysHolds, 9 states)
         ↳ breaks: buy_sword → fight_troll → cross_bridge ⇒ Hero.hp=-1

The softlock above is invisible to every scenario in the spec — nobody writes a test for a situation they didn't think of. The explorer finds it in milliseconds with the shortest trace.

• The initial state is built from entity field defaults; given=[...] supplies or overrides instances. given_any=[[...], [...]] declares an explicit finite set of roots.
• initial=Initial(vary=[...], where=[...]) declares an initial relation. vary fields range over bool, Enum, bounded integer Field, or Field(values=[...]) domains; ordinary predicates filter the Cartesian product. BoundField varies a field across an entire Scope.
• Queries quantify over every admissible root, and traces name the originating configuration (init #2 ⊢ …).
• Numeric Field(ge=..., le=...) constraints keep the state space finite. Driving a field out of range is an error with a trace; saturate=True clamps instead, for counters where only thresholds matter.
• If the state space exceeds max_states (default 10 000), the query reports INCONCLUSIVE instead of pretending.
• Each check explores only its slice. An invariant or query is checked on its cone of influence: the actions that can change what it reads, what those actions read, and so on. Independent processes in one spec therefore do not multiply each other's states. The result is exact, not an approximation, and JSON reports each check's slice. check --no-slice explores the whole model for every check.
• What the budget leaves open, TLC can finish. check --tlc exports every INCONCLUSIVE invariant and Reachable/Unreachable/AlwaysHolds query, on the slice analint used, to TLA+ and runs TLC on it. TLC keeps its states on disk and runs on all cores. The export mirrors the transition kernel exactly (presence, terminal lock, simultaneous effects, Field bounds, lifecycle edges, pruning by invariants); state counts match analint on every example. Constructs it cannot mirror (floats, Min/Max, unguarded reads of a slot that may be absent) are refused and the check stays INCONCLUSIVE. Results decided this way carry "backend": "tlc". Needs Java and a TLC jar (ANALINT_TLC_JAR, or the one bundled with Quint's Apalache).
• Query and invariant results include elapsed_ms in JSON and elapsed time in terminal output. This measures work performed by that check: exploration is charged on a cache miss, and an invariant's constrained recheck is included. Shared exploration is charged to its first consumer, so timings depend on check order. Invariants with no canonical initial state have no timing. Model preparation and shared action coverage outside a check are excluded; the sum is not total command time.
• During exploration the engine also reports violated invariants and undeclared lifecycle transitions (an effect performing A → C when the lifecycle only allows A → B).
• An ad-hoc query without editing the spec: put it in a file and run analint check . --what-if query.py.

from analint import Bound, Count, Initial

player = Bound("player", players)
role_assignments = Initial(
    vary=[player.role],
    where=[Count(player, player.role == Role.MAFIA) == 1],
)

mafia_can_win = Reachable(Game.winner == Role.MAFIA, initial=role_assignments)

Spec

The root aggregate lists the model's behaviour:

from analint import Spec

spec = Spec(
    id="ecommerce",
    name="E-commerce Platform",
    actions=[checkout],
    scenarios=[sc_happy, sc_no_funds],
    queries=[paid_is_reachable],
)

Entities, events, scopes and lifecycles follow from the behaviour that references them; listing them is allowed. Nothing is collected from module globals: a behaviour object defined but not listed is reported as an orphan.

Composition

Reusable model fragments expose an explicit Contract; one root Spec imports those contracts:

# payments.py
from analint import Contract

payments_api = Contract(
    id="payments",
    version="1.0.0",
    entities=[Payment],
    events=[PaymentCaptured],
    invariants=[payment_amount_is_positive],
    actions=[capture_payment],
)

# spec.py
from analint import Spec
from .payments import payments_api

spec = Spec(
    id="checkout",
    name="Checkout",
    imports=[payments_api],
    scenarios=[capture_payment_happy],
)

Composition is explicit: only contract contents and objects listed directly on Spec are included (plus the entities, events, scopes and lifecycles they reference), so private implementation actions do not leak through Python's import graph. Duplicate ids and incomplete contract surfaces are reported by structural validation. Multiple Spec objects in one import graph are a load error rather than being merged implicitly.

analint show contract payments -p . reports the exact exported surface. --what-if still adds hypothesis objects on top of the composed model.

Project layout

The spec is loaded through a single entry point — spec.py — and its import graph defines what is in the spec:

spec.py             ← single file is enough for small projects

# or, multi-file (use relative imports):
myproject/
  __init__.py
  entities.py       ← Entity subclasses + enums
  events.py         ← Event subclasses
  invariants.py     ← Invariant instances + reusable predicates
  actions.py        ← Action instances
  flows.py          ← Flow instances
  scenarios.py      ← Scenario instances
  spec.py           ← lists the behaviour: Contract(s) + Spec(imports=[...])

# myproject/spec.py
from analint import Contract, Spec

from .actions import archive_card, create_card
from .scenarios import sc_archive_ok, sc_create_ok

cards = Contract(id="cards", actions=[create_card, archive_card],
                 scenarios=[sc_create_ok, sc_archive_ok])
spec = Spec(id="myproject", name="My Project", imports=[cards])

Entities, events, scopes and lifecycles need not be listed: they follow from the behaviour that references them (research/35). Nothing is collected from module globals; a Spec that lists no behaviour is an "empty model" error.

A .py file in the directory that is not reachable from the entry point produces a warning — a forgotten import never silently shrinks the model. Likewise, a behaviour object (action, invariant, scenario, flow, query) defined in a spec module but not part of the model produces a warning — a forgotten registration never silently drops behaviour.

CLI

analint check [PATH]              # validate: structural checks + scenario runs
  -f, --format terminal|json
  -s, --scenario ID   -t, --tag TAG
  --strict                        # warnings become errors
  --what-if FILE.py               # add the file's objects to the model for this
                                  # run only — test a hypothesis without editing the spec
  --max-states N                  # override every exploration budget for this run
                                  # (canonical invariant check and each query)
  --no-slice                      # explore the whole model for every check
                                  # instead of each check's slice
  --tlc                           # decide what stayed INCONCLUSIVE with TLC
  --tlc-timeout SECONDS           # per exported check

analint show [KIND] [NAME] -p PATH   # inspect the model (JSON output)
  analint show -p .                  # overview: all ids by kind
  analint show contract payments -p . # exact imported contract surface
  analint show action checkout -p .  # pre/effect/post/emits/scenarios of one action
  analint show lifecycle Order.status -p .      # transitions, terminal, unreachable states

analint affects TARGET -p PATH    # impact analysis before changing something (JSON)
  analint affects Wallet.balance -p .   # who reads/writes the field, invariants, lifecycles
  analint affects checkout -p .         # what the action touches + event-linked actions

analint trace PROPERTY_ID -p PATH # query witness or invariant counterexample, with state changes
  -f, --format terminal|json
  --what-if FILE.py               # trace a property added by a hypothesis
  --no-slice                      # whole model instead of check's slice
                                  # the property is decided as check decides it

analint PATH                      # shorthand for `analint check PATH`

Exit codes: 0 ok · 1 findings (errors, failed scenarios, warnings with --strict) · 2 usage error · 3 spec could not be loaded · 4 inconclusive (a query exhausted its exploration budget without a verdict). JSON output carries a three-valued verdict (PASS/FAIL/INCONCLUSIVE); passed is true only on an effective PASS and reflects --strict.

What-if: check a hypothesis without touching the spec

A patch is a standalone file whose objects are added on top of the model for one run. It must reference the spec's objects to build predicates over them; the loaded spec's entry module is always importable under the stable alias analint_spec, regardless of whether the spec is a package or a single file:

# /tmp/hypothesis.py
from analint import Invariant
from analint_spec import Board          # the loaded spec, by stable alias

max_two = Invariant(Board.card_count <= 2, label="At most 2 cards per board")

analint check . --what-if /tmp/hypothesis.py
  FAIL  archive-card/happy
         ↳  INVARIANT failed: At most 2 cards per board

(A packaged spec can also be imported by its real package name, e.g. from myproject.entities import Board, but analint_spec works for every layout, including single-file specs.)

MCP server (for AI agents)

pip install analint[mcp]
analint-mcp        # stdio MCP server: check, show, affects, explore, trace

The same five operations as the CLI, callable as agent tools — an agent can inspect the model, run impact analysis before a change, test a hypothesis with what_if, explore reachable states, inspect traces, and validate after editing.

trace accepts query and invariant ids. Its analint.trace/v1 result identifies the target with query or invariant, then reports the root, action steps with field changes, and final state. A property without a witness returns witness: null and its status; an initial-state violation has a root and zero steps. Query and invariant ids must be distinct for tracing.

Agent Skill

The portable analint Agent Skill teaches coding agents the show → affects → what-if → apply → check workflow without requiring MCP. Install that directory with your agent client's normal skill installer; the CLI remains the execution layer.

gh skill preview angru/analint analint@main
gh skill install angru/analint analint@main

What the linter checks

Structural

• Missing/duplicate ids; duplicate class names from double imports
• Predicates reference registered entities/events and existing fields
• Event payload bindings: fields exist, annotation types match
• Two effects on the same field (simultaneity violation)
• Field constraints on construction and after effects
• Transitions out of terminal states
• Scenario given covers the entities the action references (warning)
• Scenario given states reachable from the lifecycle initial state (warning)
• Actions without scenarios (warning); files not imported by the entry point (warning)

Scenario execution

1. Invariants and pre — checked against given
2. Terminal guard — an entity in a terminal lifecycle state must not be modified
3. Effects applied simultaneously → post-state
4. post, invariants, and field constraints — checked against the post-state
5. then (Assert, Emitted) — checked against the post-state

If expected=Expect.FAIL: the scenario passes when steps 1–2 block the action.

Reachability (queries)

BFS over all reachable states; every query answers with a trace of action ids:

• Reachable(p) — a witness path exists / FAIL with "explored all N states"
• Unreachable(p) — regression guard; FAIL shows the counterexample path
• AlwaysHolds(p) — invariant over the whole space, not just scenarios
• NoDeadEnd(goal) — softlock detector: a reachable state from which the goal is gone
• DeadActions() — actions never enabled in any reachable state
• en route: invariant violations and undeclared lifecycle transitions, with traces

Examples

Status

This is an early public release (0.0.2). The engine and CLI are mature and covered by 500+ tests, but the API is not yet frozen and may change before 1.0 — pin a version if you depend on it.

analint performs bounded reachability over a finite state graph. It checks safety and reachability — invariants, Reachable, NoDeadEnd, dead actions — and returns an honest completeness verdict, preferring INCONCLUSIVE / NOT_CHECKED over a silent pass. It deliberately does not model liveness or temporal "eventually" properties; that is a scope boundary, not a defect.

Contributing

See CONTRIBUTING.md for development setup, running the tests, and the review-gated workflow.

License

MIT © angru