Why Your AI Agent Should Think in Temporal Logic (LTL)

These days, many of the problems we ask LLMs to solve aren't really language problems. They're behavior problems. As we give agents more access to our lives, reliability becomes crucial. We don't just care what an agent does. We care when it does it, what must happen before something else, and what should never happen at all.

We usually mention better prompts, stronger models, or more sophisticated planning algorithms when we talk about making our agents more reliable. These help, but they can only take you so far.

In researching solutions, I came across another tool that software engineers have been using for decades to reason about complex systems: Linear Temporal Logic (LTL). It lets you express behavior in verifiable terms and has been game-changing in my production agents. Let's get into what LTL is and how you can use it with your agents.

Prompt Engineering Isn't a Specification

Imagine that we're building an autonomous code review agent. As part of the agent, we might write a prompt like this:

Review the pull request, run tests if necessary, leave comments, and only approve if everything passes.

On first review, it sounds reasonable. But how do you know what order the agent will complete these tasks in? What happens if the model decides to approve before finishing the review? Or leaves comments after approving?

We can keep adding more instructions, but eventually the prompt will become a wall of text that's difficult for both humans and models to reason about. It also increases token costs and introduces more opportunities to add conflicting instructions over time.

If you look closely at our prompt, though, you'll notice something interesting: we're using natural language to describe a state machine. We're describing an ordering problem (which tasks must happen before others) and natural language is imprecise for that.

That's what formal specification languages were invented for.

Thinking in Behaviors Instead of Instructions

Instead of describing behavior procedurally, temporal logic lets us describe properties that must always hold. For example:

• A pull request must always be reviewed before approval.
• If tests fail, approval must never occur.
• Every requested tool call must eventually be completed.
• An agent that starts a task must eventually either succeed or fail at that task.

These are the rules that define whether the system behaved correctly and they must be followed regardless of which LLM generates the response.

What Does LTL Look Like in a Program?

LTL extends propositional logic with operators about time.

Here are the symbols we'll use in this post:

If that syntax looks intimidating and takes you back to your college math and logic courses, don't worry! The ideas are much simpler than they appear. In fact, you're probably already thinking about these concepts informally.

Here are a few simple LTL formulas and what they mean in plain language.

G(approved → reviewed)

means:

Approval should never happen unless the review has already completed.

Or:

G(toolRequested → F toolCompleted)

means:

Every tool request should eventually finish.

In a program, names like toolRequested and toolCompleted represent facts we can observe about the current state. We might derive them from state machine states, context values, or emitted events:

As the program runs, those observations form a trace:

planning → searching → toolCompleted → answering
Copy to clipboard

A verifier evaluates the trace and checks that every occurrence of toolRequested is eventually followed by toolCompleted. That's something many agent frameworks attempt to enforce today with retries and bookkeeping. LTL gives us a declarative way to describe the guarantee itself.

Agents Already Have States

Modern agents aren't simply generating text. They're moving through workflows to complete tasks, review files, etc.:

Receive task → Plan → Call tool → Receive result → Reason → Call another tool → Generate response
Copy to clipboard

Each step in a workflow represents a state transition. A state machine manages those transitions, while temporal logic specifies the properties that must hold across them.

You can express transitions like:

• Planning must happen before execution
• Two tools can/cannot run simultaneously
• The agent can/cannot answer without verification
• Memory updates must occur after success
• A task cannot remain unfinished forever

These are architectural decisions, not suggestions that can be left to chance through prompt engineering. Combining a state machine with temporal logic lets us apply deterministic workflows to our non-deterministic agents.

How do we put this into action? Let's walk through an example setup with TypeScript and XState.

Encoding Agent Guarantees with XState

Consider an agent that must research a question before producing an answer. Its behavioral requirements are simple:

1. The agent must plan before calling a tool.
2. It must not answer while a tool call is outstanding.
3. Every started run must eventually reach a final state.
4. A failed tool call must transition to recovery or failure rather than leaving the agent stuck.

In temporal logic, we can describe these properties as:

G(answering → toolCompleted)
# Whenever the agent is answering, its tool call must already be complete

G(toolRequested → F(toolCompleted ∨ failed))
# Whenever a tool is requested, it must eventually complete or fail.

G(started → F(completed ∨ failed))
# Whenever a run starts, it must eventually complete or fail.
Copy to clipboard

With XState, we can encode a lot of this behavior in the state machine.

Asynchronous work such as model requests, database queries, and tool calls can run as invoked actors. XState starts an actor when the machine enters the state that invokes it and stops the actor when the machine leaves that state.

1import { assign, setup } from "xstate";
2
3const researchAgentMachine = setup({
4  types: {
5    context: {} as AgentContext,
6    input: {} as AgentInput,
7  },
8  actors: {
9    createPlan,
10    searchDocs,
11    generateAnswer,
12  },
13  actions: {
14    storePlan: assign({
15      plan: ({ event }) => event.output,
16    }),
17    storeSearchResult: assign({
18      searchResult: ({ event }) => event.output,
19    }),
20    storeAnswer: assign({
21      answer: ({ event }) => event.output,
22    }),
23    storeError: assign({
24      error: ({ event }) => event.error,
25    }),
26  },
27}).createMachine({
28  id: "researchAgent",
29  initial: "planning",
30  context: ({ input }) => ({
31    question: input.question,
32    plan: undefined,
33    searchResult: undefined,
34    answer: undefined,
35    error: undefined,
36  }),
37  states: {
38    planning: {
39      invoke: {
40        src: "createPlan",
41        onDone: {
42          target: "searching",
43          actions: "storePlan",
44        },
45        onError: {
46          target: "failed",
47          actions: "storeError",
48        },
49      },
50    },
51    searching: {
52      invoke: {
53        src: "searchDocs",
54        onDone: {
55          target: "answering",
56          actions: "storeSearchResult",
57        },
58        onError: {
59          target: "failed",
60          actions: "storeError",
61        },
62      },
63    },
64    answering: {
65      invoke: {
66        src: "generateAnswer",
67        onDone: {
68          target: "completed",
69          actions: "storeAnswer",
70        },
71        onError: {
72          target: "failed",
73          actions: "storeError",
74        },
75      },
76    },
77    completed: { type: "final" },
78    failed: { type: "final" },
79  },
80});
Copy to clipboard

That way, the order of operations goes from just a suggestion in the prompt to an encoded structure:

planning → searching → answering → completed
    ↘ failed    ↘ failed     ↘ failed
Copy to clipboard

There's no transition from planning directly to answering or from searching to completed. The agent can't enter answering until the search actor has completed successfully, which gives us a useful safety property:

G(answering → searchCompleted)
Copy to clipboard

In plain language, the structure of the machine makes the invalid transition unreachable.

Running the Machine

The machine now defines the agent's allowed states and transitions, but it is still only a description. To execute that workflow, we create an actor from the machine, subscribe to its state changes, and start it.

1import { createActor } from "xstate";
2
3const agent = createActor(researchAgentMachine, {
4  input: {
5    question: "How does temporal logic improve agent reliability?",
6  },
7});
8
9agent.subscribe({
10  next: (snapshot) => {
11    console.log("State:", snapshot.value);
12    console.log("Context:", snapshot.context);
13  },
14
15  error: (error) => {
16    console.error("Actor crashed:", error);
17  },
18
19  complete: () => {
20    const snapshot = agent.getSnapshot();
21
22    if (snapshot.matches("completed")) {
23      console.log("Answer:", snapshot.context.answer);
24    } else {
25      console.error("Agent failed:", snapshot.context.error);
26    }
27  },
28});
29
30agent.start();
Copy to clipboard

A successful run might produce this sequence using the actor above:

planning
searching
answering
completed
Copy to clipboard

A tool failure might instead produce this sequence:

planning
searching
failed
Copy to clipboard

The machine gives us a sequence of states. That sequence then becomes a trace, which is the execution history we'll test against our LTL specification.

Why the Trace Matters

Temporal logic evaluates behavior across an entire trace (aka, a sequence of states) not just one state at a time. Traditional validation, by contrast, usually asks whether the system is valid right now. For example:

1const valid = Boolean(
2  snapshot.context.searchResult &&
3  snapshot.context.answer,
4);
Copy to clipboard

That check can tell us whether the current snapshot contains both a search result and an answer, but it can't tell us how the system reached that snapshot and that distinction matters.

Suppose two executions end in exactly the same state:

1{
2  state: "completed",
3  hasSearchResult: true,
4  hasAnswer: true,
5}
Copy to clipboard

At first glance, both appear valid but their histories may look very different.

A correct execution might be: planning → searching → answering → completed, while an invalid execution might be: planning → answering → searching → completed.

The final snapshot alone hides the violation. Both executions eventually contain a search result and an answer, but only one respected the requirement that evidence must be gathered before the answer was generated. Temporal logic preserves that distinction because it evaluates behavior across the entire trace. LTL cannot determine whether the evidence itself is true, but it can verify that the agent gathered evidence before making a claim based on it.

These are properties of history and progression, not properties of a single state.

This distinction shows up throughout agentic systems: authenticate before accessing sensitive data, retrieve evidence before making a grounded claim, receive approval before performing a destructive action, and finish required tool calls before returning a response. Temporal logic gives us a way to classify and verify requirements like these.

Safety and Liveness

Temporal properties are often divided into two broad categories: safety and liveness.

A safety property says:

Something bad must never happen.

For example:

G(answering → searchCompleted)
# The agent must never enter `answering` before search has completed.
Copy to clipboard

A safety violation can be identified as soon as the forbidden behavior occurs. Consider this finite trace: planning → answering. The moment the agent enters answering before search completes, the property has been violated. No later transition can undo that violation, so we do not need to observe the rest of the execution.

A liveness property says:

Something good must eventually happen.

For example:

G(toolStarted → F(toolCompleted ∨ toolFailed))
# Whenever a tool begins, it must eventually complete or fail.
Copy to clipboard

This property is about progress. A trace such as: planning → searching → toolStarted → waiting → waiting → waiting may not contain an explicitly invalid state, but it shows a different kind of failure: the system has stopped making progress.

This is particularly important for agents because it's easy for an agent to remain in individually valid states while still being behaviorally broken. It may retry forever, wait indefinitely for a tool, repeatedly revise its plan, or bounce between two subagents without ever resolving the user's task. With just snapshot validation, we may see nothing wrong. To see loops, we need trace validation.

Once we turn that trace into data, we can test these properties directly.

Evaluating a Trace in TypeScript

We can represent a temporal requirement as a function over the full sequence. For example, the property:

The agent must not answer before search completes.
Copy to clipboard

can be checked like this:

1type TraceEntry =
2  | { type: "state"; value: string }
3  | {
4      type: "event";
5      value: string;
6      callId?: string;
7    };
8
9function assertSearchBeforeAnswer(
10  trace: readonly TraceEntry[],
11): void {
12  let searchCompleted = false;
13
14  for (const entry of trace) {
15    if (
16      entry.type === "event" &&
17      entry.value === "searchCompleted"
18    ) {
19      searchCompleted = true;
20    }
21
22    if (
23      entry.type === "state" &&
24      entry.value === "answering" &&
25      !searchCompleted
26    ) {
27      throw new Error(
28        "Temporal violation: answering began before search completed.",
29      );
30    }
31  }
32}
Copy to clipboard

Notice that this verifier maintains knowledge of the past. Instead of looking at just the answering state, it asks whether the required event occurred earlier in the trace.

We can write a similar monitor for unresolved tool calls:

1function assertEveryToolCallResolved(
2  trace: readonly TraceEntry[],
3): void {
4  const outstandingCallIds = new Set<string>();
5
6  for (const entry of trace) {
7    if (
8      entry.type === "event" &&
9      entry.value === "toolStarted"
10    ) {
11      if (!entry.callId) {
12        throw new Error(
13          "Temporal violation: tool started without a call ID.",
14        );
15      }
16
17      if (outstandingCallIds.has(entry.callId)) {
18        throw new Error(
19          `Temporal violation: duplicate tool call ID ${entry.callId}.`,
20        );
21      }
22
23      outstandingCallIds.add(entry.callId);
24    }
25
26    if (
27      entry.type === "event" &&
28      (
29        entry.value === "toolCompleted" ||
30        entry.value === "toolFailed"
31      )
32    ) {
33      if (
34        !entry.callId ||
35        !outstandingCallIds.delete(entry.callId)
36      ) {
37        throw new Error(
38          "Temporal violation: tool resolved without a matching call ID.",
39        );
40      }
41    }
42  }
43
44  if (outstandingCallIds.size > 0) {
45    throw new Error(
46      `Temporal violation: ${outstandingCallIds.size} tool call(s) never resolved.`,
47    );
48  }
49}
Copy to clipboard

Again, no single snapshot necessarily exposes the problem. The violation emerges from the relationship between events over time.

Finite Traces and Real Agent Runs

These monitors work neatly for completed traces, but live and interrupted agent runs introduce another question: what should a verifier conclude when the trace simply ends?

Classical LTL is often defined over infinite sequences. Agent runs, however, produce finite traces: they complete, fail, time out, or are cancelled. This means a production verifier has to decide what the end of a trace means.

Consider this property: toolStarted → eventually toolCompleted. Now consider a trace that ends with: toolStarted → waitingForTool. Has the property been violated?

There are several possible interpretations:

• The tool is still running, so the result is not known yet.
• The workflow was cancelled, so completion is no longer expected.
• The trace ended unexpectedly, so the tool call should be treated as abandoned.
• A timeout occurred, which should count as a failure transition.

The important point is that termination semantics must be explicit. In an XState machine, this usually means modeling outcomes such as:

completed
failed
cancelled
timedOut
Copy to clipboard

rather than treating every stopped trace as equivalent. A temporal specification can then describe the acceptable outcomes:

G(toolStarted → F(toolCompleted ∨ toolFailed ∨ cancelled ∨ timedOut))
Copy to clipboard

This makes the runtime behavior much easier to reason about. Every started operation must eventually reach a recognized resolution state, even if that resolution is not success.

Recording an Execution Trace

With those termination semantics defined, we can record every XState snapshot and turn it into a trace suitable for testing or verification:

1type AgentState =
2  | "planning"
3  | "searching"
4  | "answering"
5  | "completed"
6  | "failed";
7
8type TraceEntry = {
9  state: AgentState;
10  timestamp: number;
11  hasPlan: boolean;
12  hasSearchResult: boolean;
13  hasAnswer: boolean;
14};
15
16function runAgent(question: string) {
17  const trace: TraceEntry[] = [];
18
19  const actor = createActor(researchAgentMachine, {
20    input: { question },
21  });
22
23  actor.subscribe((snapshot) => {
24    trace.push({
25      state: snapshot.value as AgentState,
26      timestamp: Date.now(),
27      hasPlan: snapshot.context.plan !== undefined,
28      hasSearchResult:
29        snapshot.context.searchResult !== undefined,
30      hasAnswer: snapshot.context.answer !== undefined,
31    });
32  });
33
34  actor.start();
35
36  return { actor, trace };
37}
38
39function assertAnsweringRequiresSearch(
40  trace: readonly TraceEntry[],
41): void {
42  for (const entry of trace) {
43    if (entry.state === "answering" && !entry.hasSearchResult) {
44      throw new Error(
45        "Temporal violation: agent entered answering without a completed search result.",
46      );
47    }
48  }
49}
Copy to clipboard

Once execution is captured this way, the same trace can support local tests, runtime monitors, and production observability.

From Logs to Behavioral Evidence

Most agent platforms already collect traces for debugging and observability. They record model calls, tool invocations, retries, latency, token usage, and errors. Temporal verification changes the role of that data.

A trace is no longer just a debugging artifact that someone inspects after an incident. It becomes evidence that the system followed its behavioral contract. For every execution, we can ask:

1const result = verifyAgentTrace(trace, specifications);
2
3if (!result.valid) {
4  reportViolation({
5    runId,
6    property: result.property,
7    counterexample: result.counterexample,
8  });
9}
Copy to clipboard

A counterexample might be as small as searching → answering or toolStarted → waiting → cancelled. That minimal sequence is often more actionable than a vague evaluation score. It tells us exactly which guarantee failed and which transition exposed the problem.

Behavioral Guarantees, Not Better Suggestions

Prompts still matter, but they are not the right place to enforce every requirement about ordering, progress, and termination. State machines give an agent an explicit workflow. Traces make its execution observable. Temporal logic lets us state what must remain true across that execution.

Together, these tools move agent reliability beyond asking whether the final answer looks plausible. They let us verify whether the entire process that produced the answer was valid.