Secure Program Synthesis / Vericoding

Do not trust the agent. Verify the environment it acts through.

VeriTool is a counterexample-guided synthesis pipeline for building narrowly scoped agent tools with explicit safety invariants. Instead of asking whether a model is aligned, we ask whether each capability it receives is constrained, inspectable, and verifier-approved.

See live results See the vision

Core Idea

From model alignment to capability verification

Recursive language models and autonomous coding agents become dangerous when they inherit broad REPL access to the filesystem, network, databases, and arbitrary computation. VeriTool inverts the framing: rather than proving the agent's reasoning is safe, it synthesizes the environment interfaces the agent can use and rejects unsafe tool implementations with concrete counterexamples.

The loop is deliberately simple and legible: write a formal safety invariant, generate a candidate tool with the LLM, verify it under bounded checks and policy guards, then feed the counterexample back into the next iteration.

Where VeriTool Fits

RLMs become safer when tool access flows through a verified boundary

The key intervention is not inside the model weights. VeriTool sits between the RLM and the external capabilities it wants to use, turning raw tool access into a constrained synthesis-and-verification gate.

Without VeriTool

RLM with direct tool access

Context + task Recursive Language Model

Plans, reasons, and decides when to call tools.

Direct access layer Filesystem / DB / Network / Compute

Broad capability surface, difficult to reason about, easy to misuse.

Risk surface

Unsafe reads, unsafe writes, unsafe queries, unsafe outbound calls.

With VeriTool

RLM routed through a verified tool gateway

Context + task Recursive Language Model

Requests a capability instead of getting unconstrained tool access.

VeriTool boundary Spec → Generate → Verify → Counterexample

Synthesizes a narrow tool and admits it only if the invariant holds under bounded checks.

Safe reader

Safe SQL

Safe API

Safe eval

Effect

The RLM can still act, but only through approved tools with explicit safety invariants.

Vericoding Loop

One shared synthesis loop, six safety lanes

Specification

Write a narrow tool contract and formal invariant.

Generation

Prompt the LLM to produce candidate Python code for the tool.

Verification

Run AST guards, policy checks, and bounded executable verifiers.

Feedback

Inject the concrete counterexample into the next generation step.

Completed Runs

Live benchmark results across finished models

This view summarizes the completed live runs for `claude-sonnet-4`, `gpt-4o`, `deepseek-v3.2-exp`, and `gemini-2.5-pro`. Every model was evaluated on the same six-tool suite with the same four-iteration budget per tool.

How to read pass / fail

Each tool gets at most 4 generation attempts. After every attempt, VeriTool runs the verifier. A tool is marked pass if any candidate satisfies the full safety and behavioral spec within that budget. It is marked fail if no verifier-approved candidate is found before the 4-call limit is exhausted.

The aggregate view makes the comparison legible: some models converge reliably on most tool families, while others burn through the budget on verifier violations or fail to repair the right counterexample in time.

Aggregate pass rate 62.5%

Claude Sonnet 4

5 / 6

Best completed run so far, finishing with five verified tools in 17 total iterations.

GPT-4o

4 / 6

Middle of the pack: four verified tools, with failures concentrated in API safety and bounded evaluation.

DeepSeek V3.2 Exp

4 / 6

Also reached four verified tools, but with a different profile: it solved API calling and bounded evaluation.

Gemini 2.5 Pro

2 / 6

Completed, but converged on only two tools before exhausting the verifier budget on the rest.

What the benchmark reveals

The easy lanes are bounded logging, local file reads, and small SQL fragments once the model internalizes the guardrail. The hard lanes are outbound API policy enforcement and tiny arithmetic evaluators, where small structural mistakes keep triggering the verifier.

Explore live trajectories Compare model leaderboard Open results note Open report draft

Long-Term Vision

Runtime tool synthesis for adaptive but bounded agents

Intent recognition

An agent encounters a new API, schema, or file format and proposes a tool it wishes it had.

Global invariants

The system applies universal rules like no arbitrary network calls, no raw disk writes, and no unsafe escalation.

On-the-fly verification

The CEGIS loop synthesizes and rejects candidates until it finds a bounded-safe interface.

Dynamic integration

Only the verified tool is injected back into the agent environment for immediate use.

The destination is not a static “safe tool belt.” It is a runtime compiler for agent capabilities that expands what the system can do without relaxing the environment boundaries that keep it safe.

Limits and Honesty

What this does not claim

VeriTool is not a universal proof system for arbitrary Python. The current evidence is bounded and tool-specific, combining AST restrictions, policy checks, regex guards, and executable reference oracles.

The completed runs span outcomes from 2 of 6 to 5 of 6 tools. That spread is the useful result: the mechanism is strong enough to expose real differences in repair behavior, but still narrow enough that failures remain concrete and diagnosable.