Formulas¶

Formulas are immutable dataclasses; combine them freely, and wrap one in a Constraint to check it. All of them are importable from agentltl. The formula table gives a one-line summary of each.

Building from a string¶

agentltl._parser.parse ¶

parse(text: str) -> Formula

Parse an LTL formula string into an AST Formula node.

Examples:

>>> parse('before("a", "b")')
Before(a='a', b='b')

>>> parse('called("x") & F(called("y"))')
And(left=Called(tool='x'), right=Eventually(operand=Called(tool='y')))

Formula nodes¶

Abstract Syntax Tree for First-Order Linear Temporal Logic formulas.

This module defines the node types that compose an FOLTL formula AST. It extends propositional LTL with first-order quantifiers (∀, ∃) over dynamically-extracted entity domains.

Every node is an immutable (frozen) dataclass that inherits from Formula.

Supported constructs¶

Atomic propositions (leaf nodes) * Called(tool) – tool appears at least once in the trace * CalledWith(tool, args) – tool called with specific argument values * CalledNTimes(tool, n, op) – tool called exactly / at least / at most n times * Before(a, b) – first occurrence of a precedes first occurrence of b * After(a, b) – first occurrence of a follows first occurrence of b * AllBefore(tools, b) – every tool in tools precedes b (multi-input gate) * BranchCalled(tool, wrong_tool, context) – correct branch tool called (not wrong one)

Temporal operators (unary / binary) * Globally(φ) – G φ (φ holds at every position) * Eventually(φ) – F φ (φ holds at some position) * Next(φ) – X φ (φ holds at the next position) * Until(φ, ψ) – φ U ψ (φ holds until ψ holds) * WeakUntil(φ, ψ) – φ W ψ (φ holds until ψ, or forever) * Release(φ, ψ) – φ R ψ (dual of Until)

Logical connectives * Not(φ) – ¬ φ * And(φ, ψ) – φ ∧ ψ * Or(φ, ψ) – φ ∨ ψ * Implies(φ, ψ) – φ → ψ

Special / convenience * Predicate(fn, desc) – arbitrary Python callable evaluated with trace context * AtPosition(index, φ)– φ holds at a specific trace position

First-order quantifiers (FOLTL extension) * Var(name) – variable placeholder, bound by ForAll / Exists * ForAll(var, domain, body) – ∀x ∈ D. φ(x) * Exists(var, domain, body) – ∃x ∈ D. φ(x)

Substitution * substitute(formula, bindings) – replace Var references with concrete values

All nodes support __str__ for human-readable syntax export and __repr__ for debugging.

Formula `dataclass` ¶

Formula()

Abstract base for every LTL AST node.

Called `dataclass` ¶

Called(tool: str)

Bases: Formula

True iff tool appears at least once in the trace.

Now `dataclass` ¶

Now(tool: str)

Bases: Formula

True iff the call AT THE CURRENT POSITION is tool.

The step-local counterpart of Called, which is a fact about the whole trace (called("x") holds at every position once x appears anywhere). Inside temporal operators that is rarely what a rule means: G(called("deploy") -> X(...)) fires at every step of a run that deploys once. G(now("deploy") -> X(...)) fires at the deploy step only.

CalledWith `dataclass` ¶

CalledWith(tool: str, expected_args: Dict[str, Any] = dict())

Bases: Formula

True iff tool was called with arguments matching expected_args.

expected_args is a dict; the check passes when every key in expected_args is present in the actual call arguments and the values are equal. Extra keys in the actual call are allowed.

CalledNTimes `dataclass` ¶

CalledNTimes(tool: str, n: int, op: str = '==')

Bases: Formula

True iff the number of calls to tool satisfies the comparison.

op is one of "==", ">=", "<=", ">", "<".

Before `dataclass` ¶

Before(a: str, b: str)

Bases: Formula

True iff the first occurrence of a precedes the first occurrence of b.

After `dataclass` ¶

After(a: str, b: str)

Bases: Formula

True iff the first occurrence of a follows the first occurrence of b.

AllBefore `dataclass` ¶

AllBefore(tools: Sequence[str], target: str)

Bases: Formula

True iff every tool in tools appears before the first occurrence of target.

This captures a multi-input gate constraint: several parallel steps must all complete before a convergence point.

BranchCalled `dataclass` ¶

BranchCalled(correct_tool: str, wrong_tool: Optional[str] = None, context: str = '')

Bases: Formula

True iff the correct_tool was called (and optionally wrong_tool was NOT called).

Captures branch / conditional constraints where the agent must choose the correct tool path. context is a human-readable description of the branch condition (e.g. "risk_score > 0.7").

CalledWithResult `dataclass` ¶

CalledWithResult(tool: str, expected_result: Any, expected_args: Dict[str, Any] = dict())

Bases: Formula

True iff tool was called and its return value matches expected_result.

expected_args optionally restricts which call instances are considered (same subset-match semantics as CalledWith).

expected_result may be:

a plain value — checked for equality against the recorded result,
a dict — checked as a subset of the result dict (partial match),
a Var — bound by an enclosing quantifier.

The result is read from the "tool_result" (or "result") key in the raw metrics["tool_calls"] entry.

InstanceBefore `dataclass` ¶

InstanceBefore(tool_a: str, n: int, tool_b: str, m: int)

Bases: Formula

True iff the n-th occurrence of tool_a precedes the m-th occurrence of tool_b.

Both n and m are 1-based. If either tool has fewer occurrences than required the constraint fails with a clear message.

Example:

InstanceBefore("read_file", 2, "write_file", 1)
# "the second read_file happened before the first write_file"

CalledInOrder `dataclass` ¶

CalledInOrder(tools: Sequence[str])

Bases: Formula

True iff tools appear as a subsequence of the trace in the given order.

The tools need not be consecutive — only their relative order matters. Duplicate tool names are allowed; each match consumes one occurrence.

Example:

CalledInOrder(["validate", "process", "commit"])
# validate appears somewhere before process, which appears before commit

WithinSteps `dataclass` ¶

WithinSteps(tool_a: str, tool_b: str, n: int)

Bases: Formula

True iff tool_b first occurs within n steps after the first occurrence of tool_a.

Both tools must be present in the trace, and tool_b must appear at or after tool_a. The distance is position(b) − position(a); the constraint passes when distance <= n.

Example:

WithinSteps("alert", "acknowledge", 3)
# acknowledge must be called within 3 steps of alert

Globally `dataclass` ¶

Globally(operand: Formula)

Bases: Formula

G φ – φ must hold at every position of the trace.

Eventually `dataclass` ¶

Eventually(operand: Formula)

Bases: Formula

F φ – φ must hold at some position of the trace.

Next `dataclass` ¶

Next(operand: Formula)

Bases: Formula

X φ – φ must hold at the next position.

Until `dataclass` ¶

Until(left: Formula, right: Formula)

Bases: Formula

Φ U ψ – φ holds at every position until ψ becomes true (strong until).

WeakUntil `dataclass` ¶

WeakUntil(left: Formula, right: Formula)

Bases: Formula

Φ W ψ – like Until but φ may hold forever without ψ ever occurring.

Release `dataclass` ¶

Release(left: Formula, right: Formula)

Bases: Formula

Φ R ψ – ψ must hold until (and including) the first position where φ holds.

Not `dataclass` ¶

Not(operand: Formula)

Bases: Formula

¬ φ

And `dataclass` ¶

And(left: Formula, right: Formula)

Bases: Formula

Φ ∧ ψ

Or `dataclass` ¶

Or(left: Formula, right: Formula)

Bases: Formula

Φ ∨ ψ

Implies `dataclass` ¶

Implies(left: Formula, right: Formula)

Bases: Formula

Φ → ψ

Predicate `dataclass` ¶

Predicate(fn: Callable, description: str = 'predicate', runtime_safe: Optional[bool] = None)

Bases: Formula

Arbitrary predicate evaluated against the full trace context.

fn receives (trace: Trace, position: int) and must return bool. description is a human-readable label used in reports and __str__.

runtime_safe is consulted by the static runtime-safety classifier in agentltl.runtime_safety. Set it to True to declare that a violation of fn is detectable at any finite prefix (a safety property) or False to declare that the property is unbounded liveness. None (the default) means the framework defers to the user; the classifier reports AMBIGUOUS and the registration-time hook stays silent.

Because callables are not hashable in general, equality falls back to identity comparison.

AtPosition `dataclass` ¶

AtPosition(index: int, operand: Formula)

Bases: Formula

Φ holds at a specific index (0-based) in the trace.

Previous `dataclass` ¶

Previous(operand: Formula)

Bases: Formula

Y φ – φ held at the previous position (false at the first one).

Once `dataclass` ¶

Once(operand: Formula)

Bases: Formula

O φ – φ held at some position up to and including this one.

Historically `dataclass` ¶

Historically(operand: Formula)

Bases: Formula

H φ – φ held at every position up to and including this one.

Since `dataclass` ¶

Since(left: Formula, right: Formula)

Bases: Formula

Φ S ψ – ψ held at some position j up to this one, and φ at every position after j.

CountBefore `dataclass` ¶

CountBefore(operand: Formula, n: int, op: str = '<')

Bases: Formula

The number of positions before this one where operand held satisfies op n.

CallPattern ¶

What Matches asks about a call. Harnesses supply their own (globs, paths, files that exist); ToolPattern is the plain one.

match(name, args) returns True, False, or None for "maybe": the call's arguments are only known when it runs (xargs rm). A pattern whose match takes a third argument also gets the recorded call (a ToolCall: its result, and raw with the exit status a harness recorded as status). bind(bindings) returns the pattern with quantifier variables (Var values) replaced. tools names the tools it can match, for linting.

ToolPattern ¶

ToolPattern(tools: Union[str, Sequence[str]], args: Optional[Dict[str, Any]] = None)

Bases: CallPattern

A call to one of tools whose arguments include args (equal values; a Var value is bound by an enclosing quantifier).

Matches `dataclass` ¶

Matches(pattern: Any, maybe: bool = False)

Bases: Formula

The call at the current position matches pattern.

maybe says how a call that only may match (the pattern answered None) counts: True where counting it as a match is the cautious reading (a prohibited call), False where not counting it is (a call that would satisfy an obligation). Either way the failure it causes is marked as resting on a possible match.

Var `dataclass` ¶

Var(name: str)

Variable reference, bound by a ForAll or Exists quantifier.

Appears inside CalledWith.expected_args values. NOT a Formula — it is a placeholder resolved by substitute before evaluation.

ForAll `dataclass` ¶

ForAll(var: str, domain: Any, body: Formula, description: str = '')

Bases: Formula

∀x ∈ domain. body(x)

True iff body holds for every entity returned by domain. Empty domain → vacuously true (standard FOL semantics).

Parameters:

Name	Type	Description	Default
`var`	`str`	Name of the bound variable.	required
`domain`	`Any`	`Callable[[Trace, dict], list]` — entity extractor.	required
`body`	`Formula`	Formula template containing `Var(var)` references.	required
`description`	`str`	Human-readable label for the domain (used in `__str__`).	`''`

Exists `dataclass` ¶

Exists(var: str, domain: Any, body: Formula, description: str = '')

Bases: Formula

∃x ∈ domain. body(x)

True iff body holds for at least one entity returned by domain. Empty domain → false (standard FOL semantics).

Parameters:

Name	Type	Description	Default
`var`	`str`	Name of the bound variable.	required
`domain`	`Any`	`Callable[[Trace, dict], list]` — entity extractor.	required
`body`	`Formula`	Formula template containing `Var(var)` references.	required
`description`	`str`	Human-readable label for the domain (used in `__str__`).	`''`

called ¶

called(tool: str) -> Called

Shorthand: called("tool_name").

before ¶

before(a: str, b: str) -> Before

Shorthand: before("a", "b").

after ¶

after(a: str, b: str) -> After

Shorthand: after("a", "b").

eventually ¶

eventually(tool_or_formula: Union[str, Formula]) -> Eventually

F(called("tool")) when given a string, F(φ) otherwise.

always ¶

always(tool_or_formula: Union[str, Formula]) -> Globally

G(called("tool")) when given a string, G(φ) otherwise.

substitute ¶

substitute(formula: Formula, bindings: Dict[str, Any]) -> Formula

Replace all Var references in formula with concrete values.

Walks the AST recursively. Only CalledWith.expected_args values are checked for Var instances (variables don't appear in tool-name positions).

Quantifier scoping is respected: if an inner ForAll / Exists binds the same variable name, that inner scope shadows the outer binding.

Raises:

Type	Description
`ValueError`	If a standalone `Var` is encountered outside of a `CalledWith.expected_args` value.

Formulas¶

Building from a string¶

agentltl._parser.parse ¶

Formula nodes¶

Supported constructs¶

Formula dataclass ¶

Called dataclass ¶

Now dataclass ¶

CalledWith dataclass ¶

CalledNTimes dataclass ¶

Before dataclass ¶

After dataclass ¶

AllBefore dataclass ¶

BranchCalled dataclass ¶

CalledWithResult dataclass ¶

InstanceBefore dataclass ¶

CalledInOrder dataclass ¶

WithinSteps dataclass ¶

Globally dataclass ¶

Eventually dataclass ¶

Next dataclass ¶

Until dataclass ¶

WeakUntil dataclass ¶

Release dataclass ¶

Not dataclass ¶

And dataclass ¶

Or dataclass ¶

Implies dataclass ¶

Predicate dataclass ¶

AtPosition dataclass ¶

Previous dataclass ¶

Once dataclass ¶

Historically dataclass ¶

Since dataclass ¶

CountBefore dataclass ¶

CallPattern ¶

ToolPattern ¶

Matches dataclass ¶

Var dataclass ¶

ForAll dataclass ¶

Exists dataclass ¶

called ¶

before ¶

after ¶

eventually ¶

always ¶

substitute ¶

Formula `dataclass` ¶

Called `dataclass` ¶

Now `dataclass` ¶

CalledWith `dataclass` ¶

CalledNTimes `dataclass` ¶

Before `dataclass` ¶

After `dataclass` ¶

AllBefore `dataclass` ¶

BranchCalled `dataclass` ¶

CalledWithResult `dataclass` ¶

InstanceBefore `dataclass` ¶

CalledInOrder `dataclass` ¶

WithinSteps `dataclass` ¶

Globally `dataclass` ¶

Eventually `dataclass` ¶

Next `dataclass` ¶

Until `dataclass` ¶

WeakUntil `dataclass` ¶

Release `dataclass` ¶

Not `dataclass` ¶

And `dataclass` ¶

Or `dataclass` ¶

Implies `dataclass` ¶

Predicate `dataclass` ¶

AtPosition `dataclass` ¶

Previous `dataclass` ¶

Once `dataclass` ¶

Historically `dataclass` ¶

Since `dataclass` ¶

CountBefore `dataclass` ¶

Matches `dataclass` ¶

Var `dataclass` ¶

ForAll `dataclass` ¶

Exists `dataclass` ¶