ContrAgent: Symbolic Temporal Supervision for LLM Agents via LTLf Contracts
September 17, 2026
ContrAgent uses assume-guarantee contracts in linear temporal logic over finite traces (LTLf) to supervise LLM agent tool calls. This framework formalizes agent behavior as checkable predicates to prevent irreversible tool-call errors and hallucinations through deterministic verification.
HOW THIS AFFECTS YOU
●
builderYou can implement deterministic safety guards for agents using symbolic logic rather than relying on stochastic LLM judges.
●
researcherThis provides a formal method for verifying agentic trajectories using temporal logic.