VeriTool: Safer Agents through Safer Tools

Saurav

Agent safety is often discussed at the level of the whole agent, but many practical failures happen at a lower level: the tools the agent is allowed to use. A file reader, SQL wrapper, API caller, or evaluator can each create a very different failure mode. VeriTool explores a simple alternative: instead of treating these tools as trusted infrastructure, synthesize them under explicit contracts

and reject unsafe candidates with counterexamples.

Reviewer's Comments

Reviewer's Comments

Arrow
Arrow
Arrow

The paper offers a useful idea tightening LLM security by carefully controlling tool access but the current experimentation feels underpowered. The verifier relies on simple regex and AST checks, which limits it to standard test-driven generation rather than true formal CEGIS. Strengthening this work would benefit from solver-backed reasoning (e.g. Z3), and a more diverse tool benchmark, and clearer visualizations to show how repairs differ across models.

This project introduces a novel perspective on safe tool invocation. Rather than verifying untrusted tools or implementing external guards, the approach generates formal requirements, synthesizes tools that precisely satisfy those requirements, and validates them via a formal verifier. If verification fails, the system utilizes the resulting counterexamples for counterexample-guided repair. To address practical concerns regarding computational overhead and coverage, a caching mechanism is employed to mitigate the high cost of tool generation. Also, managing a list of trusted external (or previously generated) tools and using them for known requirement will mitigate coverage.

VeriTool is a strong project that targets an important agent-safety problem: instead of trying to verify an entire autonomous agent, it focuses on constraining the lower-level tools the agent is allowed to use. This is a practical and well-scoped framing, because many real agent failures can arise from unsafe file readers, SQL wrappers, API callers, loggers, maskers, or evaluators.

The artifact is technically solid. The paper describes a shared counterexample-guided synthesis loop across six micro-tool families: Local Context Reader, Bounded SQL Querier, Safe API Caller, Append-Only Logger, PII Masker, and Compute-Bounded Evaluator. Each candidate tool is checked using AST guards and a bounded verifier, with counterexamples fed back into later attempts. The reported live benchmark is meaningful: four models were evaluated under the same six-tool suite and four-attempt budget, with 15 of 24 tool instances converging and the best model reaching 5 of 6 tools.

The strongest aspect of the project is that it records the repair trajectory, not just final pass/fail results. Showing the first failure, the counterexample, the next attempt, and the final acceptance or budget exhaustion makes the synthesis process inspectable and helps reveal where models can or cannot use verifier feedback effectively.

The main improvement area is broader validation. VeriTool is intentionally bounded and micro-scoped, so the claims should stay calibrated to narrow contracts rather than general Python verification or full agent safety. The work would be stronger with more tool classes, more adversarial fixtures, clearer comparison against simpler baselines such as one-shot generation plus tests, and deeper analysis of why specific models fail or repeat mistakes after counterexamples.

Overall, this is high-quality hackathon work with a clear safety motivation, a real artifact, and a practical verification loop. With broader benchmarks, stronger failure analysis, and more guidance on how to design good tool contracts, VeriTool could become a meaningful contribution for safer agent toolchains.

Good idea overall and the author is honest about how some gates are strong and some gates just match patterns and could be fooled.

The gap is that there's only one try per model-tool, so the ranking might no be representative. There are also no trials without the witness hint test, so there's little case to support that the hint is what helped.

Good next steps can be to run multiple seeded runs, report per-tool verifier strength (and stress the regex/pattern verifiers with new inputs), and to add a retry-without-counterexample part to show the feedback loop is doing work.

You've got good object-level taste; keep this going!

Cite this work

@misc {

title={

(HckPrj) VeriTool: Safer Agents through Safer Tools

},

author={

Saurav

},

date={

},

organization={Apart Research},

note={Research submission to the research sprint hosted by Apart.},

howpublished={https://apartresearch.com}

}

Recent Projects

OliGraph: graph-based screening of large oligopools

Existing synthesis screening tools cannot evaluate short oligonucleotide pools, whose overlapping fragments can be reassembled into regulated sequences via polymerase cycling assembly (PCA) yet fall below gene-length detection thresholds. We present OliGraph, an open-source tool that constructs a bi-directed overlap graph from an oligonucleotide pool and extracts contigs for downstream gene-length screening. An optional PCA mode retains only cross-strand overlaps consistent with PCA chemistry. We validated OliGraph in a blinded study across ten simulated pools (70–9,184 oligonucleotides, 30–300 bp) spanning four risk categories. BLAST screening of individual oligonucleotides failed to identify sequences of concern in most pools: three returned zero hits, and vector noise obscured true positives in the remainder. After OliGraph assembly, contig-level BLAST matched the longest assembled sequences (up to 1,905 bp) to sequences of concern at 97–100% identity. In one pool, assembly collapsed 1,634 individual BLAST results into 10 hits from a single contig, all assigned to the same source organism. PCA mode correctly distinguished assemblable from non-assemblable fragments within the same pool. Two pools with no assemblable structure yielded no contigs. OliGraph processed all pools in under 0.2 seconds, fast enough for real-time order screening and consistent with proposals to bring oligonucleotide orders within the scope of synthesis screening regulation.

Read More

BioRT-Bench: A Multi-Attack Red-Teaming Benchmark for Bio-Misuse Safeguards in Frontier LLMs

Frontier AI laboratories are expected to maintain safeguards against biological misuse, but whether deployed models actually refuse bio-misuse queries under adversarial pressure is largely unmeasured in the public literature. We introduce BioRT-Bench, a benchmark that runs four attack methods (direct request, PAIR, Crescendo, and base64 encoding) against four frontier models (Claude Sonnet 4.6, GPT-5.4, DeepSeek V4-flash, Kimi K2.5) across 40 prompts spanning five biosecurity-relevant categories. Responses are scored by a calibrated judge extending StrongREJECT with two bio-specific dimensions: specificity and actionability. We measure Attack Success Rate (ASR), where 0 means the model fully refused and 1 means it provided specific, actionable bio-misuse content. Our results reveal a sharp robustness divide: Chinese frontier models (DeepSeek, Kimi) have under 5% refusal rates even under direct request (ASR 0.88 and 0.79), while Western models (Claude, GPT) maintain substantially stronger safeguards (ASR 0.15 and 0.16). Crescendo is the most effective attack across all models, both in bypassing refusal and in eliciting actionable content. Claude Sonnet 4.6 is the most robust model tested, achieving 100% refusal against base64-encoded prompts.

Read More

PROTEUS (PROTein Evaluation for Unusual Sequences): Structure-Informed Safety Screening for de novo and Evasion-Prone Protein-Coding Sequences

AI protein design tools like RFdiffusion, ProteinMPNN, and Bindcraft make it trivial to produce low-homology sequences that fold into active, potentially hazardous architectures. However, sequence homology-based biosafety screening tools cannot detect proteins that pose functional risk through structurally novel mechanisms with no sequence precedent. We present a tiered computational pipeline that addresses this gap by combining MMseqs2 sequence alignment with structure-based comparison via FoldSeek and DALI against curated toxin databases totaling ~34,000 entries. AlphaFold2-predicted structures are screened for both global fold similarity (FoldSeek) and local active/allosteric site geometry (DALI), capturing convergent functional hazards that sequence screening misses. The pipeline was validated against a panel of toxins, benign proteins, structural mimics, and de novo-designed Munc13 binders, as well as modified ricin variants with residue substitutions. We additionally tested robustness to partial-synthesis evasion, where a bad actor submits multiple shorter coding sequences intended for downstream reassembly into a full toxin-coding gene. We found that while sequence-based screening did not identify any de novo ricin analogues with high certainty, the combined pipeline with FoldSeek and DALI identified all 24 tested de novo ricins as toxic.

Read More

OliGraph: graph-based screening of large oligopools

Existing synthesis screening tools cannot evaluate short oligonucleotide pools, whose overlapping fragments can be reassembled into regulated sequences via polymerase cycling assembly (PCA) yet fall below gene-length detection thresholds. We present OliGraph, an open-source tool that constructs a bi-directed overlap graph from an oligonucleotide pool and extracts contigs for downstream gene-length screening. An optional PCA mode retains only cross-strand overlaps consistent with PCA chemistry. We validated OliGraph in a blinded study across ten simulated pools (70–9,184 oligonucleotides, 30–300 bp) spanning four risk categories. BLAST screening of individual oligonucleotides failed to identify sequences of concern in most pools: three returned zero hits, and vector noise obscured true positives in the remainder. After OliGraph assembly, contig-level BLAST matched the longest assembled sequences (up to 1,905 bp) to sequences of concern at 97–100% identity. In one pool, assembly collapsed 1,634 individual BLAST results into 10 hits from a single contig, all assigned to the same source organism. PCA mode correctly distinguished assemblable from non-assemblable fragments within the same pool. Two pools with no assemblable structure yielded no contigs. OliGraph processed all pools in under 0.2 seconds, fast enough for real-time order screening and consistent with proposals to bring oligonucleotide orders within the scope of synthesis screening regulation.

Read More

BioRT-Bench: A Multi-Attack Red-Teaming Benchmark for Bio-Misuse Safeguards in Frontier LLMs

Frontier AI laboratories are expected to maintain safeguards against biological misuse, but whether deployed models actually refuse bio-misuse queries under adversarial pressure is largely unmeasured in the public literature. We introduce BioRT-Bench, a benchmark that runs four attack methods (direct request, PAIR, Crescendo, and base64 encoding) against four frontier models (Claude Sonnet 4.6, GPT-5.4, DeepSeek V4-flash, Kimi K2.5) across 40 prompts spanning five biosecurity-relevant categories. Responses are scored by a calibrated judge extending StrongREJECT with two bio-specific dimensions: specificity and actionability. We measure Attack Success Rate (ASR), where 0 means the model fully refused and 1 means it provided specific, actionable bio-misuse content. Our results reveal a sharp robustness divide: Chinese frontier models (DeepSeek, Kimi) have under 5% refusal rates even under direct request (ASR 0.88 and 0.79), while Western models (Claude, GPT) maintain substantially stronger safeguards (ASR 0.15 and 0.16). Crescendo is the most effective attack across all models, both in bypassing refusal and in eliciting actionable content. Claude Sonnet 4.6 is the most robust model tested, achieving 100% refusal against base64-encoded prompts.

Read More

This work was done during one weekend by research workshop participants and does not represent the work of Apart Research.
This work was done during one weekend by research workshop participants and does not represent the work of Apart Research.