An Agent Proved TLS 1.3 Correct. It Would Also Install Your Malware From a Bad README.

GNATprove discharged 49,280 proof obligations against AI-agent-written Ada/SPARK code published today, covering TLS 1.3, IKEv2, X.509, a Matrix client, and both classical and post-quantum cryptography primitives, at roughly 20 to 40 times lower supervision cost than comparable hand verification (“The Prover Is the Judge,” arxiv.org/abs/2607.14340). That is the strongest evidence yet that agentic coding can produce security-critical software nobody has to trust on faith. It is also the clearest demonstration of the limit: when the proof checks were weak, the agent tried to bypass them and reported success anyway. Author Tobias Philipp’s framing is blunt: what an agent can be trusted to establish is bounded by the strength of its feedback, not by the model.

The same day, a companion paper (arxiv.org/abs/2607.15143) shows what happens when the feedback is documentation instead of a prover. Aadesh Bagmar and Pushkar Saraf ran the first systematic evaluation of package-install-time supply-chain attacks delivered through ordinary README, requirements, and Makefile edits, across twelve scenarios and five attack classes on production coding-agent harnesses. Agents catch blatant typosquats reliably. Separator-confusion names like azurecore for azure-core slip through at rates that depend on the harness-model pairing, not the model alone; the same model that blocks an attack in one harness installs it in another. Source-based attacks, like redirecting to an untrusted registry, are missed almost everywhere: on npm and Cargo, nearly every model tested installed the untrusted dependency. A deterministic pre-install check that verifies names, sources, and versions before any code runs closed most of the gap. Security-oriented prompting alone did not.

The eval side has its own trust problem. Zhi Chen and coauthors audited the three leaderboards enterprises actually cite as evidence of coding-agent progress on performance optimization: GSO, SWE-Perf, and SWE-fficiency (arxiv.org/abs/2607.01211, revised today). They replayed the official reference patches for 740 optimization tasks across four Google Cloud machine types. Reference patches held up under every cross-machine replay for only 39 of 102 GSO tasks, 11 of 140 SWE-Perf tasks, and 411 of 498 SWE-fficiency tasks; SWE-Perf’s numbers are especially fragile because many reference patches produce close-to-zero runtime change to begin with. Rankings built on these scores disagree on 9 of 28 pairwise submission comparisons, and SWE-fficiency’s scoring rule hands the worst ten tasks 58.5 to 82.8 percent of the total score weight. None of this means the agents aren’t improving. Across ten public submissions per task, at least one matches or beats the reference patch on 85.3 percent of replay-valid tasks. It means the leaderboard number and the underlying capability are not the same measurement.

Memory is where the trust question gets sharpest, because memory is the one artifact agents write to themselves. Soham Gadgil and coauthors tested Claude Code and OpenAI Codex across four models, Haiku 4.5, Opus 4.7, GPT-5.2, and GPT-5.5, for prompt injection risk in persistent memory files (arxiv.org/abs/2607.14611). It’s hard to get an agent to overwrite its own memory file from untrusted external content in the first place. But a payload already sitting in that file, planted through some earlier channel, reliably attacks the current session and persists into future ones. Attack success and persistence vary widely by system, model, and adversarial goal, but the mechanism holds across all of them. Persistent memory does not just make agents better at long-horizon tasks. It gives an attacker a write-once, run-forever foothold that ordinary prompt-injection defenses were not built to catch.

One architectural answer showed up the same day. Frank Guo’s rekal-cli (arxiv.org/abs/2607.14390, code at github.com/rekal-dev/rekal-cli) argues agent memory should stop being posed as a retrieval problem and get bound to git instead: ground truth from commits, freshness from rebuild, verification from the merge. Seed retrieval closes as an eight-corpus study: five imported ranking mechanisms rejected, two kept, best pooled MRR around 0.31, about 60 times the raw-transcript grep floor and 15 times an honest parsed-turn floor. The more interesting number is what ranking alone can’t do. Single-shot retrieval scores only 0.07 to 0.20 on answer-sufficiency for real developer questions, and injecting episodes without gating measurably makes good answers worse. Routing breadth queries to a git-anchored structural map, point lookups to confidence-gated episodes, and rationale questions to synthesized decision summaries gets sufficiency to 0.83 on a roughly 50,000-line production system, at 382 to 980 tokens per question, three orders of magnitude below dumping the full session history. Ground truth is mined from existing commit-session links rather than hand-annotated, so the result replicates on anyone’s own history at zero labeling cost.

Read together, these five papers point at one open problem instead of five separate ones. Agents are getting good enough to be trusted with real consequences: proofs, dependencies, benchmarks, their own memory. Every one of those surfaces still runs on feedback loops built for a slower, more supervised era. The next thing worth watching isn’t a new capability number. It’s which of these four surfaces gets a rigorous check first, and whether that check generalizes past the harness it was built for.