Verifiable Coding-Agent Execution

Teams that let coding agents create commits can add a pre-push or CI gate that accepts QA claims only when the run contains replayable evidence. A browser QA claim should point to a successful browser tool call, target URL, rendered-page artifact, console output, and network record. A file-corruption or measurement claim should point to the command, inputs, and captured output.

ProcGrep gives this gate a practical query surface: ordered actions, counts, conditions, and missing actions over traces such as read_file, search_repo, edit, run_test, and submit. The paper reports deterministic trace search at F1=1.000 with 1.1 µs latency per decision, while LLM judges were much slower and less accurate on the same episodic search task. A postmortem from a coding harness shows the failure mode: an auditor agent wrote specific browser QA and file-measurement claims that had never happened, and a push gate blocked the work because the required evidence was absent.

Teams with privacy-sensitive C code can pilot a local invariant-synthesis step in the verification workflow. The useful build is narrow: run ESBMC first, enumerate simple symbolic invariant atoms, then ask a local open-weight model for candidate invariants only when the symbolic phase stalls. Every candidate must be accepted by ESBMC before it reaches a proof artifact or review.

VerIbmc is a concrete template. It keeps stores of provable, disprovable, and unknown atoms, feeds that structured verifier feedback back into later prompts, and accepts only checked invariants. In its reported evaluation, the best setup solved 431 of 499 usable benchmark problems, and the symbolic phase alone solved 75 problems with no model call. The small-code-model measurement study points in the same operational direction for local tools: fix extraction and signature alignment before adding semantic rerankers. Its M1 harness fix raised DeepSeek-Coder-1.3B from 29 to 41 HumanEval+ tasks and from 128 to 161 MBPP+ tasks.

Organizations routing coding-agent traffic through a shared LLM API gateway should test whether the gateway can read or modify prompts, tool definitions, tool outputs, provider responses, and secrets. If it can, the concrete adoption change is a client sidecar that verifies an enclave measurement before releasing the request body, with the request and response data path confined to the TEE.

Aegis shows this as a small data-path change, with authentication, scheduling, account selection, accounting, and management left on the host. The paper’s plaintext-router baseline allowed four malicious-router attack classes, including tool-call rewrite, typosquatted dependency swaps, trigger-gated attacks, and passive secret exfiltration. Aegis blocked all four in the authors’ tests and reported about 6 ms local relay overhead per request. This matters most for coding agents that can run shell commands or install packages on a developer machine.