Symbolic Constraint Agents: Mining Formal Tool-Call Constraints to Prevent Agent Errors

Jinu Lee; Shraddha Barke

cs.AIOct 18, 2026

Symbolic Constraint Agents: Mining Formal Tool-Call Constraints to Prevent Agent Errors

Authors: Jinu Lee, Shraddha Barke

Organizations: University of Illinois Urbana-Champaign · Microsoft Research

Abstract

Symbolic constraints (programmatic, deterministic checks for tool calls) enable deterministic verification of LLM agents' tool calls, but existing approaches primarily enforce predefined safety policies rather than tool dependencies in complex tool environments. We explore whether symbolic constraints can be mined from environments and observations beyond predefined policies, and whether they can improve end-to-end task performance. We present Symbolic Constraint Agents (SCA), a framework that mines symbolic constraints from API documentation, refines them against execution traces, and checks the agent's tool calls with an SMT solver at runtime. A violation triggers a natural-language warning or, when the valid replacement is uniquely determined, an automatic repair. On AppWorld, refinement raises error-detection F1 from 37.0 to 58.3 on GPT-5.5 traces and from 39.3 to 61.9 on Qwen3.5-27B traces. At runtime, repair raises GPT-5.4-mini's task success by 5.4 points under a 40-call budget and 9.8 points when environment errors are hidden, while removing 59--87% of failed calls across models, and transfers to $τ^2$ -bench with gains of up to 5.6 points. These findings show that automatically acquired symbolic constraints can improve tool-calling reliability and task completion, particularly when failures are costly or difficult to diagnose.

Figures & tables

Figure 1: Overview of SCA. Constraint generation (top) runs once per environment: an initializer agent mines candidate rules from API documentation and a refiner agent corrects them against sample agent traces. At the constraint application stage (bottom), each proposed call is checked against the constraint memory using an SMT solver. The rule shown requires ListDir ’s api_key to originate from an earlier Login ; the call passing DEF is unsatisfiable and can be repaired to ABC .

Figure 2: Constraint generation. Left: Given the target tool’s specification, the initializer agent generates constraints by reasoning about the given tool and searching other potentially relevant tools’ definitions. Right: After the initializer agent, the refiner agent updates the catalog based on how the current constraints apply to agent traces.

Figure 3: Constraint application. (a) In warning mode, the call is left unmodified, and the violated constraint is appended to the agent’s context in natural language. Here, a Login that uses a different id from the preceding Register . (b) In repair mode, SCA treats each argument as a soft constraint and finds the assignment with minimal change (Stage 1), then asserts

v\neq v^{\star}

and re-checks to confirm the replacement is unique (Stage 2). The repaired call is then passed to the environment.

GPT-5.5 traces
	Precision (%)	Recall (%)	F1 (%)
Initialize	61.5	26.4	37.0
+ Refine	90.4	43.0	58.3
Qwen3.5-27B traces
Initialize	58.8	29.6	39.3
+ Refine	83.9	49.1	61.9

Table 1: Detection of environment-rejected calls. Refinement improves precision and recall on trajectories from both model families.

		Task success (%)			Failed calls per task
Benchmark (Setting)	Agent model	No constraints	+ Warning	+ Repair	+ Warning	+ Repair
AppWorld (Standard)	Qwen3.5-9B	18.1 $\pm$ 2.2	17.6 $\pm$ 1.2	20.4 $\pm$ 2.0	4.6 $\to$ 1.1 ( $\mathbf{-76}$ )	4.6 $\to$ 0.6 ( $\mathbf{-87}$ )
AppWorld (Standard)	GPT-5.4-mini	73.5 $\pm$ 1.5	71.2 $\pm$ 2.0	75.1 $\pm$ 3.7	6.6 $\to$ 5.1 ( $-$ 24)	6.6 $\to$ 2.7 ( $\mathbf{-59}$ )
AppWorld (Standard)	Sonnet-5	77.3 $\pm$ 2.9	75.8 $\pm$ 1.7	78.1 $\pm$ 0.5	1.0 $\to$ 0.9 ( $-$ 5)	1.0 $\to$ 0.8 ( $-$ 14)
AppWorld (Standard)	GPT-5.5	90.8 $\pm$ 0.8	91.1 $\pm$ 1.0	91.4 $\pm$ 1.0	0.95 $\to$ 0.97 (+3)	0.95 $\to$ 0.74 ( $-$ 22)
AppWorld (40-call budget)	Qwen3.5-9B	12.5 $\pm$ 0.0	11.1 $\pm$ 0.6	12.8 $\pm$ 0.1	1.1 $\to$ 0.61 ( $-$ 43)	1.1 $\to$ 0.56 ( $-$ 48)

Table 2: Task success and failed tool calls. AppWorld: 417 test tasks;

\tau^{2}

-bench: 60 test tasks (airline and retail); mean

\pm

standard deviation over three runs. Success: bold marks an improvement over no constraints, and * marks a statistically significant difference (paired task bootstrap,

p<0.05

). Failed calls: calls per task rejected by the environment, without constraints

\to

with the given mode (change in %); bold marks reductions of 50% or more.

Qwen3.5-9B
Per task	Standard	40-call	Silent
Tool calls	32 $\to$ 29 ( $-$ 9)	22 $\to$ 22 ( $-$ 2)	46 $\to$ 38 ( $-$ 17)
LLM calls	45 $\to$ 43 ( $-$ 3)	30 $\to$ 30 (0)	68 $\to$ 62 ( $-$ 10)
Prompt (k)	954 $\to$ 869 ( $-$ 9)	514 $\to$ 519 (+1)	1428 $\to$ 1291 ( $-$ 10)
Compl. (k)	23.8 $\to$ 21.4 ( $-$ 10)	11.9 $\to$ 13.7 (+15)	16.1 $\to$ 13.8 ( $-$ 14)
GPT-5.4-mini

Table 3: Cost per AppWorld task without constraints

\to

repair (change in %). Prompt / Compl. : prompt and completion tokens. Shading: savings more than 10%.

Panel of Figure 4 — Figure 4: Example of warning .

Panel of Figure 5 — Figure 5: Example of repair .

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

Benchmark	Catalog	Rules	Arg.	Hist.	Outc.	Tools
AppWorld	refined	295	239	47	9	457
$\tau^{2}$ airline	policy, initial	51	36	15	0	13
	policy, refined	51	37	14	0	13
	no policy, initial	44	41	3	0	13
	no policy, refined	44	41	3	0	13
$\tau^{2}$ retail	policy, initial	69	36	33	0	16

Appendix

Table 4: Constraint catalogs: number of rules by type (argument, history, outcome) and number of tools they apply to. AppWorld rules cover 9 apps. On

\tau^{2}

-bench, refinement on the training split replaced 10 of 51 airline and 18 of 69 retail policy rules (adding 10 and 12), and 4 of 44 airline and 6 of 47 retail no-policy rules (adding 4 and 6).

AppWorld, argument rule applies to amazon__add_product_to_cart (+4 more) If the quantity parameter is provided, it must be an integer greater than or equal to 1. ForAll([i1, c1, v1], Implies(And(call(i1, c1, TARGET), params(c1, quantity_f, v1)), And(Value.is_v_int(v1), Value.v_int_get(v1) >= 1)))
AppWorld, history rule applies to gmail__create_draft (+41 more) The access_token parameter must be the access_token returned by a prior gmail login call. ForAll([i1, c1, v1], Implies(And(call(i1, c1, TARGET), params(c1, access_token_f, v1)), Exists([i2, c2], And(i2 < i1, And(call(i2, c2, appworld_gmail__login), rfield(c2, access_token_f, v1))))))
AppWorld, outcome rule applies to amazon__place_order An Amazon place_order call must not be attempted while the cart has an invalid promo code applied; it must not return the invalid-promo-code failure message. ForAll([i1, c1, v1], Implies(And(call(i1, c1, TARGET), rfield(c1, message_f, v1), Value.is_v_str(v1)), Value.v_str_get(v1) != StringVal("The promo code applied to your cart is no longer valid.")))
$\tau^{2}$ retail, policy, history rule applies to calculate Before any calculate tool call, the user must already have been authenticated by a prior lookup using email or name plus zip code. ForAll([i1, c1], Implies(call(i1, c1, calculate), Exists([i2, c2], And(i2 < i1, Or(call(i2, c2, find_user_id_by_email), call(i2, c2, find_user_id_by_name_zip))))))
$\tau^{2}$ airline, no policy, history rule applies to update_reservation_passengers Before updating passengers for a reservation, the same reservation_id must have been looked up earlier with get_reservation_details. ForAll([i1, c1, v1], Implies(And(call(i1, c1, update_reservation_passengers), params(c1, reservation_id_f, v1), Value.is_v_str(v1)), Exists([i2, c2], And(i2 < i1, call(i2, c2, get_reservation_details), params(c2, reservation_id_f, v1)))))

Appendix

Table 5: Example constraints, copied verbatim from the catalogs used in our experiments: the natural-language rule (italics) and its SMT formula. The outcome rule is the one that fires in the warning example (Figure 4 ); nearly every repair in our runs enforces an access-token history rule like the gmail one shown.

Catalog	Rules #	Faithful%	Validity%
AppWorld	295	94	89
$\tau^{2}$ airline, policy	51	84	96
$\tau^{2}$ airline, no policy	44	91	100
$\tau^{2}$ retail, policy	63	81	95
$\tau^{2}$ retail, no policy	47	100	94
Argument rules	384	93	99

Appendix

Table 6: Rule audit by three LLM judges (majority vote). No rule was judged wrong or unsure for validity; every rule that was not correct (1-validity) is too strict .

Unfaithful (3/3 judges), correct (3/3) AppWorld, argument rule, applies to amazon__signup (+15 more) Every signup call must provide a first_name parameter that is a non-empty string. ForAll([i1, c1, v1], Implies(And(call(i1, c1, TARGET), params(c1, first_name_f, v1)), And(Value.is_v_str(v1), Length(Value.v_str_get(v1)) >= 1))) Judge (Opus): “The formula only checks first_name when it is supplied and never requires it to be present, while the rule says every signup call must provide it.”
Faithful (3/3), too strict (3/3) AppWorld, history rule, applies to amazon__place_order (+2 more) The address_id parameter must be an address_id returned by a prior Amazon add_address or show_addresses call. ForAll([i1, c1, v1], Implies(And(call(i1, c1, TARGET), params(c1, address_id_f, v1)), Exists([i2, c2], And(i2 < i1, Or(call(i2, c2, appworld_amazon__add_address), call(i2, c2, appworld_amazon__show_addresses)), rfield(c2, address_id_f, v1))))) Judge (Opus): “Address IDs could legitimately come from other sources, such as order details or IDs given in the task, so valid calls without a prior add_address or show_addresses would be rejected.”
Faithful (3/3), too strict (3/3) $\tau^{2}$ retail, no policy, history rule, applies to cancel_pending_order An order may not be cancelled more than once, so no earlier cancel_pending_order call may have used the same order_id. ForAll([i1, c1, v1], Implies(And(call(i1, c1, cancel_pending_order), params(c1, order_id_f, v1)), Not(Exists([i2, c2], And(i2 < i1, call(i2, c2, cancel_pending_order), params(c2, order_id_f, v1)))))) Judge (Opus): “The formula does not check whether the earlier call succeeded, so a legitimate retry after a failed attempt (e.g., one rejected for an invalid reason string) would wrongly be flagged.”
Faithful (3/3), correct (2/3) AppWorld, history rule, applies to gmail__create_draft (+41 more); the rule behind most repairs The access_token parameter must be the access_token returned by a prior gmail login call. Judge (Opus, correct): “The documentation says the access_token is ‘obtained from gmail app login’, so a valid call needs a token returned by a prior gmail login.” Judge (Astra, too strict): “A valid Gmail access token obtained before the recorded call history can authenticate a legitimate call without a prior login call in that history.”

Appendix

Table 7: Examples from the rule audit: the judges’ labels, the rule (italics) and its formula, and the judges’ reasons, quoted verbatim.

		Task success (%)			Failed calls per task
Benchmark (Setting)	Agent model	No constraints	+ Warning	+ Repair	+ Warning	+ Repair
AppWorld (Standard)	Qwen3.5-27B	49.9	49.4	51.1	6.9 $\to$ 6.6 ( $-$ 5)	6.9 $\to$ 5.0 ( $-$ 29)
AppWorld (40-call budget)	Qwen3.5-27B	44.6	45.1	43.4	1.0 $\to$ 0.8 ( $-$ 18)	1.0 $\to$ 0.8 ( $-$ 22)
AppWorld (Silent errors)	Qwen3.5-27B	48.4	50.1	52.3	2.3 $\to$ 1.3 ( $-$ 42)	2.3 $\to$ 1.8 ( $-$ 23)

Appendix

Table 8: Task success and failed tool calls for Qwen3.5-27B on AppWorld (417 test tasks), one run per cell. Same catalog, settings, and agent configurations as Table 2 . Failed calls: tool calls per task rejected by the environment (under silent errors: answered with an empty response), without constraints

\to

with the given mode (change in %).

Per task	Standard	40-call	Silent
Qwen3.5-27B
Tool calls	76 $\to$ 64 ( $-$ 17)	30 $\to$ 30 (0)	34 $\to$ 34 (+1)
LLM calls	66 $\to$ 52 ( $-$ 20)	20 $\to$ 20 (0)	23 $\to$ 22 ( $-$ 4)
Prompt (k)	1670 $\to$ 1399 ( $-$ 16)	440 $\to$ 440 (0)	553 $\to$ 523 ( $-$ 5)
Compl. (k)	16.4 $\to$ 16.3 (0)	5.1 $\to$ 5.3 (+4)	6.2 $\to$ 6.2 ( $-$ 1)

Appendix

Table 9: Cost per AppWorld task for Qwen3.5-27B without constraints

\to

with repair (change in %), one run per cell. Prompt / Compl. : prompt and completion tokens, in thousands. Shading: savings more than 10%. Same runs as Table 8 .

Agent model	Init+Refine	Init only	$\Delta$
	Task success (%)
GPT-5.5	89.3	85.9	$-3.5$
Qwen3.5-27B	59.7	57.3	$-2.4$

Appendix

Table 10: Ablation of refinement. AppWorld task success (%) in the warning mode with the catalog refined with agent traces (Init+Refine) and without (Init only);

\Delta

is the change from removing refinement.

Catalog	Model	Median	p95	Time-	Share of
		(ms)	(ms)	outs	ep. time
AppWorld	GPT-5.4-mini	351	5136	4.4%	3.9%
	Sonnet-5	133	1433	1.0%	1.9%
	GPT-5.5	211	5369	7.2%	3.2%
	Qwen3.5-9B	136	2814	0.7%	0.2%
Airline	GPT-5.4-mini	21	207	0.5%	1.2%

Appendix

Table 11: Checker cost per tool call over the no-constraint runs (AppWorld: 417 tasks;

\tau^{2}

-bench: 20 airline and 40 retail tasks). p95 is the 95th-percentile check time. A timeout is a check where Z3 returns unknown at the 5 s limit. Share of episode time is total check time divided by episode wall-clock time, averaged over tasks.

LLM Agent Verification

LLM agent verification checks whether agents’ actions, evidence, policies, and completion claims satisfy explicit requirements.

See all 148 papers

Symbolic Temporal Supervision of LLM Agents Using Contracts
Sep 16, 2026Yifeng Xiao, Pierluigi NuzzoRuntime Enforcement for AI Agents LLM Agent Safety
Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA, USA
Verified Tool Calls Improve LLM Agent Reliability Under Non-Atomic Failures
Jul 31, 2026Isham Kalappurackal Mansoor, Abhishek Phadke, Pratip RanaAI Agent Reliability LLM Tool Use
Department of Computer Science Old Dominion University Norfolk, VA 23529 · School of Engineering and Computing Christopher Newport University Newport News, VA 23606
MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
May 7, 2026Ashwani Anand, Ivi Chatzi, Ritam Raha +1Computer-Use Agent Benchmarks AI Agent Reliability
Max Planck Institute for Software Systems, Kaiserslautern, Germany

Sep 16, 2026J/K move · Enter open · S save

Symbolic Temporal Supervision of LLM Agents Using Contracts

Yifeng Xiao, Pierluigi Nuzzo

Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA, USA

Runtime Enforcement for AI Agents LLM Agent Safety Runtime Verification

Open paper AskPDF arXiv

Large language model (LLM) agents augmented by tools can automate complex, multi-step tasks, such as web navigation, code generation, and workflow orchestration, by acting on external systems through tool calls. However, hallucinations, distributional instability, and adversarial manipulations in LLMs, and the irreversible consequences of certain tool calls can lead to harmful outcomes. Existing safeguards either grade recorded trajectories post hoc with stochastic LLM judges or block unsafe actions one call at a time, and no single deterministic artifact supports both roles. We present ContrAgent, a contract-based framework for symbolic temporal supervision of LLM agents. ContrAgent captures an agent's behavior as a sequence of tool calls and formalizes it as a trace over a fixed set of checkable predicates. It then specifies required behaviors using assume-guarantee contracts in linear temporal logic over finite traces (LTLf). Each contract is compiled to a deterministic finite automaton (DFA) that serves two roles: gating agent actions online and evaluating recorded traces offline. A contract library, acting as a reusable knowledge base, is maintained independently of the agent's model and can be applied across different agents within the same task domain. We show the effectiveness of our approach on four benchmarks spanning both roles, where ContrAgent matches state-of-the-art LLM-judge and rule-based guardrail baselines while producing deterministic, reproducible verdicts and, in the online mode, orders-of-magnitude lower per-call latency.

Abstract

LLM Agent Verification

Explore similar work

Symbolic Temporal Supervision of LLM Agents Using Contracts

Verified Tool Calls Improve LLM Agent Reliability Under Non-Atomic Failures

MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents