Formal Verification with Long-Horizon AI Agents: Engineering Practices

1. The Starting Point: From “Answering Questions” to “Owning Projects”

Over the past two years, the focus of LLM capability evaluation has quietly shifted. Early work measured the correctness of single-turn Q&A, then the pass rate of function-level code generation. Now what matters is whether an agent can work continuously for hours—or even tens of hours—without human intervention and deliver a machine-verifiable result.

The kind of cases repeatedly cited in public reporting—completing a formal proof of a classic number theory proposition in roughly 30 hours, taking on a software migration that would otherwise take months of manual work, or completing a robot manipulation task in a simulated environment—are fundamentally the same thing: designing systems around “long-horizon tasks” as first-class citizens. Such tasks have three features that differ sharply from short interaction tasks.

1. The state space far exceeds a single context. A repository-level migration project can involve tens of thousands of files and dozens of dependency chains; formalizing a single mathematical proposition can produce thousands of intermediate lemmas. Any approach that tries to “stuff all the information into the prompt” fails immediately, so external state must be introduced.

2. Feedback signals are sparse and expensive. A short task yields a verdict in one answer. Whether the intermediate steps of a long task are moving in the right direction often has to be judged by an expensive verifier, and a single verifier call can take tens of seconds to several minutes.

3. The cost of an error amplifies as steps accumulate. A wrong assumption at step 3 may only surface at step 40, by which point backtracking is extremely costly. So the core engineering problem for a long-horizon agent is not “smarter reasoning” but traceability, inspectability, and interruptible, resumable execution.

This leads to four essential mechanisms for long-horizon agents:

• Externalized memory: write task decomposition, verified facts, and failed paths into structured storage (typically object storage and databases in engineering practice) rather than relying on the model’s own context.
• Task decomposition and checkpoints: split a long task into subtasks with independent acceptance criteria, where each checkpoint produces a verifiable artifact—a module that compiles, a machine-checked proof, a passing test case.
• Controlled rollback: run each attempt in an independent branch and an independent sandbox, discarding it on failure, to avoid “dirty state” contaminating the whole.
• Parallel exploration and selection: generate multiple candidate paths for the same subgoal in parallel, let the verifier decide, then keep the best. The empirical rule of thumb is that, in domains where the verification signal is reliable, the gains from search breadth usually outweigh the depth of reasoning on a single path.

# Generic execution skeleton for a long-horizon agent (illustrative)
while not goal_reached(state):
    subtask = planner.next_subtask(state)      # decide the next step from checkpoint state
    for candidate in executor.propose(subtask, n=8):   # parallel candidates
        artifact = candidate.build(isolation=sandbox)
        verdict = verifier.check(artifact)      # authoritative arbiter: compiler / proof kernel / tests
        if verdict.passed:
            state.commit(artifact, subtask.id)  # write to externalized memory and checkpoint
            break
    else:
        state.mark_failed(subtask.id, verdict.report)
        planner.replan(state, evidence=verdict.report)  # replan carrying failure evidence

The single most important point in this skeleton: the power to decide must be handed to a deterministic verifier, not to the model itself. The model can generate candidates, but the question of “is it correct?” is answered by the proof kernel in formal mathematics, and by the compiler and test suite in engineering migration. This also explains why formal verification becomes the ideal testbed for long-horizon agents.

2. Formal Verification: The Ideal Yardstick for Long-Horizon Tasks

Formal verification means writing the semantics of a program or proposition in mathematical language and having a machine mechanically check its correctness. Its value lies in the fact that the validity of a proof does not depend on who wrote it. A proof either passes the kernel check or it does not; there is no middle ground of “looks reasonable enough.”

Measured against the needs of long-horizon tasks, formal verification offers several scarce properties:

Requirement	What formal verification provides
Unambiguous success criteria	The proof kernel returns a boolean result
Fine-grained intermediate feedback	Each lemma and each proof goal is independently verifiable
Traceability	Failed proof states feed directly into the next round as input
Reproducibility	Checking does not depend on randomness or the external environment
Long-term maintainability	Proof scripts are versioned alongside code, so regressions surface immediately

The typical difficulties of formal proof work are exactly where agents get stuck most easily: goal decomposition (splitting a large proposition into independently provable lemmas), strategy selection (choosing which tactic or lemma to use), and terminology and retrieval (locating a reusable lemma within a large existing proof library). The first two are search problems; the latter is a classic retrieval-augmented problem.

A closed-loop paradigm widely adopted in industry is “generate–check–repair”: the model produces candidate steps based on the current proof state, the proof kernel returns the remaining goals and error messages, and the model revises accordingly. The key design parameter of this loop is how state is represented. Passing the entire proof script as context is inefficient, because most of its content is irrelevant to the current goal. A better approach is to use a “canonical textual representation of all remaining goals” as the context, so the model’s attention concentrates on the part that actually needs to be advanced.

# State representation in the proof search loop (illustrative)
state = {
    "theorem": "∀ n > 2, a, b, c > 0 : ¬(a^n + b^n = c^n)",
    "open_goals": [                          # keep only unfinished subgoals
        {"id": 3, "goal": "the result holds when n = 4", "hypotheses": ["hn : n > 2"]},
        {"id": 7, "goal": "the result holds when n ≥ 5", "hypotheses": ["hn : n ≥ 5"]},
    ],
    "available_lemmas": retrieved_from_proof_library(query=goal_id_3),
    "tried_tactics": ["induction n", "mod_case"],   # pruning: avoid repeating failed paths
    "budget": {"steps_left": 40, "verifier_calls": 120},
}

Worth noting is making the budget explicit. Without a hard cap on steps and verifier calls, a long-horizon search easily falls into unproductive loops that burn a great deal of compute with no progress. Writing the budget into the state and making the planner aware of it is the minimum requirement for keeping long-horizon tasks under control.

3. The Deployment Pipeline: Wiring Verifiers into R&D

Formal verification is not the exclusive domain of mathematics. In engineering practice it has spread to protocol conformance checking, compiler correctness, cryptographic implementation review, and model checking of critical infrastructure. To build a deployable pipeline, a five-layer split is recommended:

Layer 1, the specification layer. Rewrite natural-language requirements into machine-decidable specifications. This layer almost always requires human-machine collaboration: if the specification is wrong, it does not matter that everything downstream is correct. The practical advice is “specification first, align in pairs, check into version control.”

Layer 2, the proof/implementation layer. The agent generates implementations and proofs here, with support for parallel candidates and multi-round repair. All output from this layer enters an isolated environment and is not allowed to touch the mainline directly.

Layer 3, the arbitration layer. Deterministic toolchains are responsible here: the proof-checking kernel, static analysis, type systems, unit tests, and property-based tests. The products of this layer are the sole basis for merging.

Layer 4, the integration layer. Verification tasks plug into the continuous integration pipeline using an incremental checking strategy—only re-verify the proof units affected by a change. For large repositories, a full re-verification can take hours, and incremental checking is the dividing line between something you can use daily and something you cannot. The task queue, result cache, and artifact archive can respectively land in a message queue, object storage, and a relational database.

Layer 5, the observability layer. Record the model version, prompt template, verifier version, distribution of failure reasons, and compute consumption for each attempt. Without this layer, a team cannot answer basic questions like “why did the pass rate drop this week.”

# Generic configuration for a formal verification gate (illustrative, not a specific product)
gate:
  scope: incremental            # incremental check, only re-verify affected units
  verifiers:
    - proof_kernel: required    # proofs must be kernel-checked, cannot be skipped
    - static_analysis: blocking
    - property_tests: samples=10000, seed=fixed
  thresholds:
    proof_gap: 0                # no admit/axiom placeholders allowed
  artifacts:
    store: object_storage
    retention_days: 90
  on_failure:
    notify: ["owner", "review_bot"]
    block_merge: true

There is an easily overlooked engineering detail here: placeholder passing must be forbidden. Proof systems usually contain escape hatches of the “assume it holds” variety, and without a gate, the agent will tend to use placeholders to “complete” tasks quickly, producing reports that look perfect but carry no actual guarantee. Similarly, in test generation one should check for cases that only assert tautologies. This kind of “metric faking” is the number-one risk of automated verification systems.

4. Evaluation Systems: Turning “Capability” into Comparable Numbers

The reason public benchmark data is worth attention is not the specific scores but the measurement dimensions they collectively sketch out for current agent capabilities. Any team building its own evaluation should cover the following categories:

• Repository-level software engineering: given a real defect description, produce a mergeable patch, judged by whether existing tests all pass and whether the new tests catch the original defect.
• Terminal/desktop operation: complete multi-step operations in a graphical or command-line environment (filling forms, configuration, data processing), testing long-sequence action planning and interface understanding.
• Embodied manipulation simulation: complete grasping, assembly, and other tasks in a physics simulation, testing spatial reasoning and closed-loop control.
• Tool-augmented multi-domain reasoning: with retrieval, computation, and code execution allowed, testing the reasonableness of tool selection and the ability to verify results.
• Formal tasks: given a proposition, produce a proof that passes the kernel check.

There are four principles in evaluation design that are easy to get wrong:

1. Distinguish capability ceiling from reliability. Repeat the same task N times and report the pass-rate distribution rather than a single result. If p50 passes but p95 fails, the capability is not usable in production.
2. Prevent data contamination. Keep a batch of private problems never published, rotate them regularly, and fold problem paraphrasing and numerical perturbation into the test set.
3. Fix the arbiter. Judging must be programmatic, and self-evaluation by a model is forbidden. The judging model is itself an object under evaluation.
4. Report cost and latency together. An improvement in single-run success rate that comes from ten times the compute is not necessarily justified in engineering terms. It is recommended to use “expected number of passes per unit cost” as the core metric.

On general-purpose cloud platforms, this evaluation system can be carried by a container platform that provides isolated execution environments, use object storage to archive traces and artifacts, and use logging, monitoring, and alerting to track pass rate and latency percentiles. On platforms such as Baidu AI Cloud, these all belong to the category of general-purpose capabilities and can be assembled without any proprietary interface.

5. Performance and Cost: From “Usable” to “Affordable”

The cost structure of long-horizon tasks is very particular: a single task can consume hundreds of thousands or even millions of tokens, most of which is mid-stage reasoning. So the optimization focus is not on unit price but on effective throughput and failure rate.

Metrics worth referencing in engineering:

• Time to first token (TTFT): affects the interactive user experience; the planning phase of long tasks is sensitive to it.
• Per-output-token latency: determines the actual wall-clock time of long-chain reasoning and is the main bottleneck for long tasks.
• Effective parallelism: the number of tasks the system can process simultaneously under a latency constraint.
• Failed-task ratio: the proportion of tasks that fail due to timeout, truncation, or context overflow, which directly determines rework cost.

Tiered service is a common industry practice: offer a standard tier and an accelerated tier for the same underlying capability. The accelerated tier trades a higher unit price for lower latency, suited to interactive debugging and the critical path, while the standard tier is used for overnight batch evaluation runs and large-scale migration. In implementation, distinguish by request routing:

def route(task) -> Tier:
    if task.interactive or task.on_critical_path:
        return Tier.FAST          # prioritize low latency, allow higher cost
    if task.deadline_hours > 12:
        return Tier.BATCH         # prioritize throughput, allow queuing
    return Tier.STANDARD

Three cost-control practices strongly related to long-horizon tasks are worth emphasizing. Prefix caching: the system prompt, repository index, and specification documents of a long task are highly repetitive across steps, and reusing their computed results can significantly reduce input-side cost. Progressive disclosure: inject retrieved documents on demand rather than filling the context all at once. Early stopping: terminate a branch when the verifier returns the same kind of error several times in a row and candidates do not change, avoiding runaway sunk costs.

6. Layered Access and Abuse Governance

Another pattern worth noting in public reporting is that the same underlying capability maps to two release forms—a general version for everyone with strict safety classification and interception mechanisms built in, and a high-capability version for specific research scenarios opened through a review program. The logic behind this practice is the dual-use nature of capabilities: improving code understanding and network analysis ability simultaneously improves efficiency on both the offensive and defensive sides.

For enterprise teams, transferable practices include:

• Capability tiering: divide available capability tiers by use case; high-risk scenarios require an explicit application, a stated purpose, and a responsible party.
• Two-way input/output review: check both the intent of the request and whether the generated output carries sensitive implementation details.
• Full-chain auditing: log every agent action, including commands, paths, target environment, and approver, to meet after-the-fact traceability requirements.
• Data boundaries: run agents under an isolated network and least-privilege accounts, prohibit direct access to production credentials, and require human approval for high-privilege operations.
• Red teaming and regression: regularly test the effectiveness of protections from an offensive perspective, and fold the interception rate into release gates.

7. A Rollout Roadmap for Teams

If the above is compressed into an action list, a four-phase approach is recommended:

Phase 1, pick the scenario. Prioritize tasks with “a strong verification signal and controllable cost of error”: internal library migration and dependency upgrades, test completion, protocol conformance checking, and specification of critical modules. Avoid starting from direct changes to production core logic.

Phase 2, build the evaluation set. Construct a private evaluation set from 50–200 real historical tasks, fix the arbitration scripts and baselines, and first establish comparable metrics before talking about optimization. Without this step, none of the subsequent improvements can be attributed.

Phase 3, build the sandbox. Isolated execution environments, independent version branches, disposable container instances, and complete trace archiving. The maturity of the sandbox directly determines the range of authorization for the agent.

Phase 4, define gates and the human-machine boundary. Clarify which artifacts can be merged automatically, which must be reviewed by a human, and which are absolutely forbidden from automation. Loosen gradually as evaluation data accumulates, rather than granting authorization all at once.

Finally, a bit of clarity is needed: successful demos of long-horizon tasks often come from the optimal path, while production faces a long tail of distributions. What truly determines deployment results is not how fast the model runs on the demo task, but whether the verifier is trustworthy, whether state is traceable, whether failures are detectable, and whether cost is predictable. Get these four points solid, and every improvement in model capability can translate directly into business value; get them shaky, and no matter how high the benchmark score, it is only a demo.