Traces and verification¶

A Trace is the ordered list of tool calls; a Constraint names and weights a formula; verify_trace checks constraints on a finished run and computes the compliance score.

Constraints and scoring¶

Constraint declaration and compliance evaluation.

This module provides:

Constraint – a named, weighted LTL formula that forms one item in a checklist of procedure compliance requirements.
verify_trace – evaluate a list of constraints against an agent trace and produce per-constraint results plus an aggregate compliance score.

Compliance score¶

Given constraints K = {κ₁, …, κₙ} and the set V ⊆ K of violated constraints:

C(τ, G_P) = 1 − Σ_{κᵢ ∈ V}  w(κᵢ)
                ─────────────────────
                Σ_{κᵢ ∈ K}  w(κᵢ)

C = 1.0 → FULL compliance
C = 0.0 → complete VIOLATION
0 < C < 1 → PARTIAL compliance

Constraint `dataclass` ¶

Constraint(name: str, formula: Formula, weight: float = 1.0, description: str = '', repair: str = '', meta: Dict[str, Any] = dict(), applies_to_final_answer: bool = False)

A single compliance constraint.

Attributes:

Name	Type	Description
`name`	`str`	Short, human-readable identifier (also used as dict key).
`formula`	`Formula`	The LTL formula that must hold on a valid trace.
`weight`	`float`	Importance weight w(κᵢ). Higher → more impact on C.
`description`	`str`	Optional longer explanation shown in reports.
`repair`	`str`	Optional imperative instruction shown to the AGENT when this constraint blocks a call ("Send note as an object with a text field carrying the referral comment"). Where `description` explains why a rule exists, `repair` says what to do about it. Empty by default, and when empty the enforcement feedback is byte-identical to what it was before this field existed.

meta `class-attribute` `instance-attribute` ¶

meta: Dict[str, Any] = field(default_factory=dict, compare=False)

Anything a caller wants to carry with the constraint (where it came from, how a harness classifies it). AgentLTL never reads it.

applies_to_final_answer `class-attribute` `instance-attribute` ¶

applies_to_final_answer: bool = False

When True, this constraint is also evaluated before the final_answer tool is executed (online enforcement). Default False preserves existing behaviour where final_answer is always exempt from pre-execution constraint checks.

ConstraintResult `dataclass` ¶

ConstraintResult(name: str, weight: float, passed: bool, detail: str, description: str = '', repair: str = '')

Result of evaluating a single constraint against a trace.

ComplianceResult `dataclass` ¶

ComplianceResult(compliance_score: float, compliance_label: str, details: str, tool_sequence: List[str], constraints: List[ConstraintResult])

Aggregate result of evaluating all constraints against a trace.

verify_trace ¶

verify_trace(metrics: Dict[str, Any], constraints: Sequence[Constraint], *, weight_overrides: Optional[Dict[str, float]] = None, full_compliance_detail: str = 'All constraints satisfied.', partial_trace: bool = False) -> Dict[str, Any]

Evaluate a list of FOLTL constraints against an agent trace.

Parameters:

Name	Type	Description	Default
`metrics`	`Dict[str, Any]`	The metrics dict from `Agent.run()["metrics"]`. `metrics["tool_calls"]` is used to build the trace.	required
`constraints`	`Sequence[Constraint]`	Ordered sequence of `Constraint` instances.	required
`weight_overrides`	`Optional[Dict[str, float]]`	Optional mapping of constraint names → custom weights.	`None`
`full_compliance_detail`	`str`	Human-readable message returned when all constraints pass.	`'All constraints satisfied.'`
`partial_trace`	`bool`	When `True`, use trigger semantics for ordering constraints. Use during pre-execution checking on growing traces.	`False`

Returns:

Type	Description
`Dict[str, Any]`	A dict: { "compliance_score": float, # C(τ, G_P) in [0, 1] "compliance_label": str, # FULL \| PARTIAL \| VIOLATION "details": str, "tool_sequence": list[str], # φ(τ) "constraints": list[dict], # per-constraint records }

Traces¶

Trace representation for FOLTL evaluation.

A Trace wraps the ordered sequence of tool calls produced by an agent run and exposes helper methods used during formula evaluation.

The canonical input is metrics["tool_calls"], a list of dicts with at least a "tool_name" key.

Example¶

from agentltl import Trace trace = Trace.from_metrics({"tool_calls": [ ... {"tool_name": "fetch"}, ... {"tool_name": "clean"}, ... {"tool_name": "summarize"}, ... ]}) trace.events ['fetch', 'clean', 'summarize'] trace.contains("clean") True trace.first_index("fetch") 0

ToolCall `dataclass` ¶

ToolCall(name: str, args: Dict[str, Any] = dict(), position: int = 0, raw: Dict[str, Any] = dict(), result: Any = None)

A single tool invocation recorded in the trace.

Attributes:

Name	Type	Description
`name`	`str`	The tool name string.
`args`	`Dict[str, Any]`	The arguments dict passed to the tool (may be empty).
`position`	`int`	0-based index in the trace.
`raw`	`Dict[str, Any]`	The original dict from `metrics["tool_calls"]`, preserved verbatim so that downstream predicates can inspect any key.
`result`	`Any`	The return value of the tool call, if recorded. Populated from the `"tool_result"` (or `"result"`) key in the raw dict. `None` when not provided.

Trace `dataclass` ¶

Trace(calls: List[ToolCall] = list())

Ordered sequence of tool calls produced by an agent run.

Implements the trace τ = [t₁, t₂, …, tₙ] over which LTL formulas are evaluated.

events `property` ¶

events: List[str]

Return the flat list of tool names in call order.

from_metrics `classmethod` ¶

from_metrics(metrics: Dict[str, Any]) -> 'Trace'

Build a Trace from the metrics dict returned by Agent.run().

Expects metrics["tool_calls"] to be a list of dicts, each with at least a "tool_name" key.

from_names `classmethod` ¶

from_names(names: Sequence[str]) -> 'Trace'

Build a Trace from a plain list of tool name strings (for tests).

contains ¶

contains(tool: str) -> bool

True iff tool appears at least once.

count ¶

count(tool: str) -> int

Number of times tool appears.

first_index ¶

first_index(tool: str) -> int

0-based index of the first occurrence of tool, or -1.

last_index ¶

last_index(tool: str) -> int

0-based index of the last occurrence of tool, or -1.

nth_index ¶

nth_index(tool: str, n: int) -> int

0-based index of the n-th occurrence (1-based n) of tool, or -1.

all_indices ¶

all_indices(tool: str) -> List[int]

All 0-based indices where tool appears.

calls_with ¶

calls_with(tool: str, expected_args: Dict[str, Any]) -> List[ToolCall]

Return all calls to tool whose args are a superset of expected_args.

suffix ¶

suffix(position: int) -> 'Trace'

Return the sub-trace starting at position (inclusive).

Used internally by the LTL evaluator for temporal operators. The new trace preserves original positions.

at ¶

at(position: int) -> Optional[ToolCall]

Return the call at position, or None.

The evaluator¶

FOLTL formula evaluation over tool-call traces.

The LTLEvaluator recursively interprets an FOLTL Formula AST node against a Trace. It extends propositional LTL evaluation with support for first-order quantifiers (∀, ∃) via eager substitution.

Evaluation is synchronous, operates on finite traces, and produces both a boolean verdict and a human-readable explanation string suitable for compliance reports.

Finite-trace semantics¶

Standard LTL is defined over infinite traces. For finite agent traces we adopt the weak finite-trace semantics common in runtime verification:

F φ is true iff φ holds at some position in the remaining trace.
G φ is true iff φ holds at every position in the remaining trace (vacuously true on the empty suffix).
X φ is true iff a next position exists and φ holds there. (X φ is false when the trace has ended — safety-oriented choice.)
φ U ψ (strong until) requires ψ to eventually hold.
φ W ψ (weak until) is satisfied if ψ never occurs but φ holds forever.
φ R ψ is the dual of Until.

First-order quantifier semantics¶

∀x ∈ D. φ(x) — true iff φ holds for every entity in D. Empty D → vacuously true.
∃x ∈ D. φ(x) — true iff φ holds for at least one entity in D. Empty D → false.

Atomic propositions (Called, Before, etc.) are evaluated against the full trace regardless of the current suffix position, since they express global facts about the run. Now is the exception: it looks at the call at the current position only.

Partial traces¶

These are the semantics of a complete trace, used for scoring. While a run is still going (partial_trace=True) the formula is judged in the five-valued semantics of agentltl._partial, which knows the difference between a final violation and an obligation not met yet; EvalResult.value and EvalResult.witnesses carry that verdict.

EvalResult `dataclass` ¶

EvalResult(passed: bool, detail: str, formula: Formula, value: Optional[int] = None, witnesses: List[Tuple[Tuple[Any, ...], int]] = list())

Result of evaluating a single formula on a trace.

Attributes:

Name	Type	Description
`passed`	`bool`	Whether the formula is satisfied.
`detail`	`str`	Human-readable explanation of the verdict.
`formula`	`Formula`	The formula that was evaluated (for debugging).
`value`	`Optional[int]`	On a partial trace, the five-valued verdict (see `agentltl._partial`); None on a complete trace.
`witnesses`	`List[Tuple[Tuple[Any, ...], int]]`	On a partial trace, the failing instances with their values.

LTLEvaluator ¶

Stateless interpreter that evaluates LTL formulas against finite traces.

Usage:

evaluator = LTLEvaluator()
result = evaluator.evaluate(formula, trace)
print(result.passed, result.detail)

evaluate ¶

evaluate(formula: Formula, trace: Trace, position: int = 0, *, metrics: Optional[Dict[str, Any]] = None, partial_trace: bool = False) -> EvalResult

Evaluate formula on trace starting at position.

Parameters:

Name	Type	Description	Default
`formula`	`Formula`	The FOLTL formula to evaluate.	required
`trace`	`Trace`	The tool-call trace.	required
`position`	`int`	Starting position in the trace (for temporal operators).	`0`
`metrics`	`Optional[Dict[str, Any]]`	Optional raw metrics dict, passed to domain extractors in ForAll / Exists quantifiers.	`None`
`partial_trace`	`bool`	When `True`, the run is still going: judge the formula in the five-valued semantics of `agentltl._partial`. passed is then "not refused now", and value / witnesses say how final that is. Default `False`: the strict post-hoc semantics.	`False`

Returns:

Type	Description
`EvalResult`	An `EvalResult` with passed (bool) and detail (str).

Traces and verification¶

Constraints and scoring¶

Compliance score¶

Constraint dataclass ¶

meta class-attribute instance-attribute ¶

applies_to_final_answer class-attribute instance-attribute ¶

ConstraintResult dataclass ¶

ComplianceResult dataclass ¶

verify_trace ¶

Traces¶

Example¶

ToolCall dataclass ¶

Trace dataclass ¶

events property ¶

from_metrics classmethod ¶

from_names classmethod ¶

contains ¶

count ¶

first_index ¶

last_index ¶

nth_index ¶

all_indices ¶

calls_with ¶

suffix ¶

at ¶

The evaluator¶

Finite-trace semantics¶

First-order quantifier semantics¶

Partial traces¶

EvalResult dataclass ¶

LTLEvaluator ¶

evaluate ¶

Constraint `dataclass` ¶

meta `class-attribute` `instance-attribute` ¶

applies_to_final_answer `class-attribute` `instance-attribute` ¶

ConstraintResult `dataclass` ¶

ComplianceResult `dataclass` ¶

ToolCall `dataclass` ¶

Trace `dataclass` ¶

events `property` ¶

from_metrics `classmethod` ¶

from_names `classmethod` ¶

EvalResult `dataclass` ¶