Daily D4 Digest — 2026-05-15
TL;DR
- A remarkable cluster of papers today converge on the same thesis: the spec, not the code, is the primary artifact — with Protocol-Driven Development, AI Harness Engineering, and Language-Based Agent Control all proposing governance layers for agent-generated software.
- BenchJack demonstrates that 10 popular agent benchmarks can be gamed to near-perfect scores without solving a single task — 219 distinct flaws found — underscoring that evaluation infrastructure is a security surface.
- AgentLens from Microsoft reveals that ~10.7% of “passing” SWE-agent patches are Lucky Passes — chaotic trial-and-error that happened to work — and proposes process-level quality scoring that reshuffles model rankings.
- On the infrastructure side, KVServe achieves up to 32.8× TTFT reduction in disaggregated LLM serving, and MinT demonstrates million-scale LoRA policy catalogs over shared 1T-class base models.
- The State-Centric Decision Process formalizes agent self-certification at runtime — agents construct their own verified state spaces predicate-by-predicate as they act.
Call to Action
- Audit your agent evals: Run your internal benchmarks through an adversarial lens inspired by the BenchJack Agent-Eval Checklist — if your agents are measured on pass/fail, you likely have Lucky Pass contamination.
- Prototype spec-first governance: The Protocol-Driven Development triplet (structural, behavioral, operational invariants) is immediately actionable — define protocol P for one agent workflow and treat generated code as replaceable.
- Evaluate KVServe for disaggregated inference: If you run PD-separated serving, the 9.13× JCT speedup from adaptive KV compression is too large to ignore — integrate with your vLLM deployment.
D1 — Agentic Engineering
AI Harness Engineering reframes the reliability problem. Rather than blaming model capability for unreliable coding agents, this paper argues that capability is an emergent property of a model-harness-environment system. The harness — a runtime substrate mediating observation, action, feedback, and completion — is formalized with eleven responsibilities including task specification, failure attribution, entropy auditing, and intervention recording. A four-level ladder (H0–H3) progressively exposes runtime support: H0 produces only a patch; H3 produces reproduction logs, failure attributions, and structured verification reports. This is the clearest articulation yet of what “scaffolding” actually means as an engineering discipline. (Cross-cuts D3, SCE)
AgentLens exposes the Lucky Pass problem in SWE-agent evaluation. Microsoft researchers evaluated 2,614 OpenHands trajectories across eight model backends and found that 10.7% of passing trajectories are “Lucky Passes” — regression cycles, blind retries, missing verification, or temporally disordered workflows that stumbled into correct patches. The framework introduces Prefix Tree Acceptor references built from multiple passing solutions and a context-sensitive intent labeler. Critically, some models shift by five rank positions when scored on process quality rather than binary pass rate. This is a direct challenge to anyone using SWE-bench numbers for model selection. (Cross-cuts SCE)
Agent² RL-Bench tests whether agents can engineer their own RL post-training. This benchmark from Microsoft asks whether LLM agents can autonomously design, implement, debug, and execute RL post-training pipelines. Results are sobering: one RL-oriented run improved ALFWorld from 4.85 to 93.28 via SFT warm-up and GRPO with online rollouts, but most successful routes still rely on supervised pipelines, and stable agent-driven RL remains rare under fixed budgets. This is the frontier of D1 — agents improving agents — and the benchmark reveals we’re not there yet.
Combining mechanical and agentic specification inference for Move. This paper demonstrates a practical hybrid: weakest-precondition analysis provides a sound mechanical baseline, while an agentic coding CLI (Claude Code via MCP) handles what WP can’t — loop invariants and high-level idiomatic specifications. The Move Prover acts as oracle; the agent iterates until verification succeeds. This is a concrete example of bounded autonomy: the agent operates freely within formal verification constraints. (Cross-cuts D3, SCE)
BenchJack: agent benchmarks are broken by design. Researchers built an automated red-teaming system that synthesized reward-hacking exploits achieving near-perfect scores on most of 10 popular agent benchmarks (WebArena, OSWorld, etc.) without solving a single task. They catalogued 219 distinct flaws across eight classes. The good news: their generative-adversarial pipeline reduced hackable-task ratios from ~100% to under 10% on four benchmarks, fully patching WebArena and OSWorld in three iterations. Every team running agent benchmarks needs the Agent-Eval Checklist. (Cross-cuts SCE)
State-Centric Decision Process builds certified trajectories at runtime. SDP tackles a fundamental problem: language environments (browsers, terminals, simulations) emit raw text with no explicit state space, no observation-to-state mapping, and no termination criterion. SDP has agents construct these objects predicate-by-predicate as they act — each step commits to a natural-language predicate, takes an action, and checks the observation. Passing predicates become certified states. This achieves best training-free results on five benchmarks, with advantages widening as horizon grows. The certified trajectories enable per-predicate credit assignment and failure localization. (Cross-cuts SCE)
D2 — AI in the Product
Typed mediation for reproducible scientific workflows. This paper proposes a pattern where the LLM orchestrates deterministic tools rather than generating analytical code. Each tool encodes one researcher’s exact procedure, ported through structured interviews. The model selects tools and parameters; the tool produces the result. Regeneration doesn’t change it. Tested on photoluminescence analysis across four platforms, the typed tool produced identical results across all runs while commercial foundation models varied in numerical output and methodology. Deployed on two instruments for ~6 months with positive feedback. The key insight for product teams: deterministic tool mediation is a deployment pattern that makes LLM-powered products reproducible. (Cross-cuts D1)
VERIMED: neurosymbolic auditing of natural-language requirements. This pipeline uses LLMs plus SMT solvers to audit medical-device software requirements. Stochastic variation across independent formalizations becomes a signal of ambiguity — requirements admitting multiple interpretations produce SMT-inequivalent formalizations. Concrete SMT counterexamples in repair loops raised verified accuracy from 55.4% to 98.5% on a hemodialysis benchmark. For any team building AI products in regulated domains, this is a practical approach to requirements validation. (Cross-cuts SCE)
D3 — Build for Agents
Language-Based Agent Control applies type systems to agent governance. LBAC requires agents to generate programs that are well-typed in the context of surrounding scaffolding code — unsafe programs are rejected by the type-checker before execution. Policies for access control, information flow, and data provenance apply uniformly across agent-generated and developer-written code. Agents may perform arbitrary side-effect-free computation and recursively invoke subagents with the same or stricter policies. Three case studies demonstrate I/O sandboxing via filesystem capabilities, data provenance, and information-flow control. For teams exposing tools to agents (MCP servers, A2A endpoints), this is a principled alternative to ad-hoc guardrails.
Protocol-Driven Development defines the governance layer for generated code. PDD formalizes a protocol as P = (S, B, O) — structural, behavioral, and operational invariants whose conjunction defines the admissible implementation space. Implementations are replaceable realizations; admission requires protocol satisfaction plus a verifiable Evidence Chain. The organizing principle — “code is transient; protocol is sovereign” — is directly relevant for D3: if you’re building for agent consumers, the protocol is the interface contract. (Cross-cuts D1, SCE)
D4 — Performance & Cost at Scale
KVServe delivers adaptive KV cache compression for disaggregated serving. KVServe addresses the bottleneck that disaggregated LLM serving (PD separation, KV state disaggregation) turns KV cache into an explicit network payload. Static compression configurations are suboptimal given varying workloads. KVServe unifies compression into a modular strategy space, uses Bayesian profiling to reduce offline search overhead by 50×, and deploys a service-aware online controller combining an analytical latency model with a lightweight bandit. Integrated into vLLM: up to 9.13× JCT speedup in PD-separated serving and 32.8× TTFT reduction in KV-disaggregated serving. These are production-relevant numbers for anyone running disaggregated inference at scale.
MinT: million-scale LoRA policy management over 1T-class base models. MinT from MindLab keeps the base model resident and manages LoRA adapter revisions through a full lifecycle (rollout, update, export, evaluation, serving, rollback). Scale Up: validated beyond 1T total parameters including MLA and DSA attention paths. Scale Down: adapter-only handoff reduces step time by 18.3× (4B dense) and 2.85× (30B MoE). Scale Out: 10⁶-scale addressable adapter catalogs with packed MoE LoRA tensors improving live engine loading by 8.5–8.7×. For agentic workloads where different tasks need different specialized policies, this is the infrastructure to serve millions of fine-tuned behaviors without millions of deployments.
Software Civil Engineering Lens
Today is an exceptionally strong day for the SCE thesis. Five of twelve selected papers independently converge on what SCE calls the spec-first principle — the idea that as code becomes auto-generated, the specification becomes the primary human-authored artifact and the primary control boundary.
Protocol-Driven Development (PDD) is the most explicit: “code is transient; protocol is sovereign.” Its protocol triplet P = (S, B, O) maps directly to the SCE lifecycle’s Specify phase, and its Evidence Chain maps to Verify → Observe. The paper’s framing of implementations as “replaceable realizations discovered through constrained search” is exactly the bounded autonomy concept — agents operate freely within invariant constraints.
AI Harness Engineering (H0–H3 ladder) operationalizes what SCE calls the professionalization gap. H0 (patch-only) is today’s craft-mode; H3 (reproduction logs, failure attribution, verification reports) is the engineering-mode target. The eleven harness responsibilities read like a checklist for the SCE pillar of “codes and norms” — standardized runtime expectations for agent-produced software.
The evaluation crisis revealed by BenchJack and AgentLens provides evidence for SCE’s “material datasheets” gap. Without process-level quality metrics (AgentLens) and adversarial benchmark auditing (BenchJack), the field is selecting materials (models) based on misleading labels. BenchJack’s 219 benchmark flaws are the software equivalent of untested building materials. AgentLens’s discovery that model rankings shift by five positions under process-quality scoring means procurement decisions are being made on unreliable data.
LBAC (type-checked agent control) and Move specification inference (MCP + formal verification) both demonstrate practical implementations of the “simulation before deployment” pillar — type-checking and SMT solving as the terraform plan of agent behavior.
The SDP paper (State-Centric Decision Process) contributes something subtle but important: agents constructing their own certified state spaces is a form of self-specifying runtime behavior. The predicate-by-predicate certification creates an audit trail that enables post-hoc verification — the Observe phase of SCE’s lifecycle.
Net assessment: Today’s research batch is the strongest evidence yet that the field is independently converging on SCE’s core thesis. Multiple groups, working on different problems (benchmarking, agent control, scientific workflows, smart contracts), are all arriving at the same conclusion: formal specification and verifiable evidence are prerequisites for reliable agent-generated software. The professionalization of software engineering isn’t a philosophical aspiration — it’s being demanded by the practical failures of craft-mode agentic systems.
Sources
- BenchJack: Systematically Auditing AI Agent Benchmarks — Automated red-teaming finds 219 flaws across 10 agent benchmarks; near-perfect scores without solving tasks
- State-Centric Decision Process — Agents build certified state spaces predicate-by-predicate; best training-free results across five benchmarks
- Typed Mediation for Scientific Workflows — LLM orchestrates deterministic tools for reproducible scientific analysis; deployed 6 months
- Language-Based Agent Control — Type-system-based policy enforcement for agent-generated programs; I/O sandboxing and info-flow control
- AgentLens: The Lucky Pass Problem — 10.7% of passing SWE-agent patches are chaotic lucky passes; process-quality scoring reshuffles model rankings
- Protocol-Driven Development — Governance model where protocol triplet (S, B, O) defines admissible implementation space; “code is transient; protocol is sovereign”
- AI Harness Engineering — Eleven-responsibility runtime substrate for coding agents; H0–H3 maturity ladder with trace-based evaluation
- KVServe — Adaptive KV cache compression for disaggregated LLM serving; 9.13× JCT speedup, 32.8× TTFT reduction
- MinT: Million-Scale LoRA Infrastructure — Managed LoRA training and serving; 10⁶-scale adapter catalogs over shared 1T-class base models
- VERIMED: Neurosymbolic Requirements Auditing — LLM + SMT solver audits medical-device requirements; raises verified accuracy from 55.4% to 98.5%
- Agent² RL-Bench — Benchmark testing whether agents can engineer RL post-training pipelines; stable agent-driven RL remains rare
- Agentic Specification Inference for Move — Claude Code + MCP + WP analysis + Move Prover for automated formal specification inference
