2026-06-05

Daily D4 Digest — 2026-06-05

TL;DR

• Self-improving agent harnesses are here: RHO achieves a 59%→78% pass rate on SWE-Bench Pro with zero external grading, using only past trajectory analysis — a major step toward autonomous agent ops.
• Formal specification synthesis by LLMs remains dangerously unreliable: only 8.6% semantic correctness for TLA+ generation, though a specialized TLA-Prover model pushes this to 30% — still far from replacing human specifiers.
• MCP reliability is now empirically catalogued: a taxonomy of 73 fault types across 473 MCP servers reveals the protocol’s maturity gap, essential reading for anyone building agent-facing infrastructure.
• KV cache and sparse attention systems (RedKnot, Vortex) deliver 3-5× throughput gains, critical for sustaining long-horizon agentic workloads at scale.
• A “robots.txt for agents” (Recuse Signal) achieves 100% cooperative compliance in pilot tests — a lightweight governance primitive for the agent-consumed infrastructure era.

Call to Action

• Evaluate RHO for your agent pipelines: the self-supervised harness optimization approach eliminates the need for labeled validation sets — review the method and assess applicability to your CI loops.
• Adopt the MCP fault taxonomy as a testing checklist: 73 leaf fault types across 11 categories provide a ready-made reliability test plan for any MCP server integration — get the taxonomy.
• Prototype the Recuse Signal on staging infrastructure: as your systems become agent-consumed, this lightweight governance primitive is trivial to deploy — review the mini-standard and adapters.

D1 — Agentic Engineering

Retrospective Harness Optimization (RHO) — Self-Improving Agents Without Labels. This is arguably the most immediately actionable paper today. RHO introduces a self-supervised method where agents mine their own past trajectories to identify failure modes, re-solve a diverse coreset of challenging tasks in parallel, and then select the best harness update via pairwise self-preference. The headline result — SWE-Bench Pro pass rate jumping from 59% to 78% in a single optimization round without any external grading signal — is striking. The key insight is treating the agent’s skills/tools/workflows (“harness”) as a first-class optimization target rather than a fixed scaffold. This aligns directly with the SCE lifecycle’s Observe→Specify loop: past failures become the specification for the next iteration. For engineering leaders, this suggests that agent deployment should always include trajectory logging with enough fidelity to enable retrospective optimization. (Cross-cuts D4: the parallel re-solving and self-consistency checks have inference cost implications.)

MLEvolve — Graph Search with Memory for Long-Horizon Agent Tasks. MLEvolve addresses three structural problems in long-running agent workflows: inter-branch information isolation, memoryless search, and lack of hierarchical control. Their Progressive Monte Carlo Graph Search (MCGS) extends tree search with cross-branch reference edges, and a “Retrospective Memory” system combines cold-start domain knowledge with dynamic experience retrieval. On MLE-Bench, it achieves SOTA under a 12-hour budget (half the standard runtime) and outperforms AlphaEvolve on mathematical algorithm optimization. The architectural pattern — decoupling strategic planning from code generation with adaptive coding modes — is a reusable idea for any multi-step agentic pipeline. The retrospective memory design echoes the “system of record” concept from LeanMarathon.

LeanMarathon — Blueprint-Driven Multi-Agent Formal Mathematics. LeanMarathon demonstrates a multi-agent architecture where four contract-scoped agents (construct, audit, prove, repair) collaborate around an “evolving blueprint” — a Lean file that simultaneously serves as formal proof skeleton, natural-language proof graph, and shared system of record. The two-stage orchestrator first stabilizes target fidelity via adversarial review, then discharges the proof DAG in parallel CI-gated rounds. Across three autonomous runs, it formalized all seven target theorems (258 lemmas) with zero sorry placeholders. The pattern of converting “one brittle multi-hour run into many local, recoverable, parallel transactions” is directly applicable to any long-horizon agentic engineering task. (High SCE relevance: the blueprint is effectively a formal specification that constrains agent autonomy.)

“The End of Software Engineering” — Agent-as-a-Service Framing. This position paper formalizes the distinction between traditional software (code carries decision logic) and agentic systems (code is ephemeral tooling for an LLM-driven reasoning loop). It traces the arc from licensed software → SaaS → Agent-as-a-Service (AaaS) and introduces “Agentic Engineering” as an emergent discipline with a distinct control model and human role. While the framing is provocative (“the end of software engineering”), the substance is more nuanced — it argues for a paradigm where human engineers shift to specifying intent and verifying outcomes rather than encoding logic. Worth reading as a conceptual frame, though the empirical grounding is thinner than the other papers today. (Cross-cuts D2, D3.)

D2 — AI in the Product

VASO — Formal Verification Closes the Loop on LLM-Generated Robot Skills. VASO tackles a crucial trust gap: foundation models have collapsed the cost of creating robot skills, but not the cost of trusting them. Each skill gets a dual-interface semantic contract — formal (for model checking) and planner-facing (for execution). When verification fails, counterexample traces become “textual gradients” that update the skill contract without touching model weights. Achieving 97.2% formal-specification compliance with fewer than 100 optimization samples is impressive. The pattern of using model-checker counterexamples as optimization feedback is generalizable well beyond robotics — anywhere you have a formal spec and LLM-generated artifacts. (Cross-cuts D1, high SCE relevance.)

D3 — Build for Agents

MCP Fault Taxonomy — The First Reliability Map for Agent-Consumed Infrastructure. This empirical study analyzed 837 fault threads from 473 actively maintained MCP server repos and produced a taxonomy of 11 top-level categories, 27 subcategories, and 73 leaf fault types. A survey of 55 MCP developers confirmed that respondents experienced an average of 20 of the 27 subcategories — no category went unobserved. The fault categories span protocol interactions, tool invocations, schema enforcement, state management, model-provider integration, security validation, and timeout/cancellation handling. For anyone building or consuming MCP servers, this is immediately actionable as a test matrix. The finding that “configuration parameters accepted but not enforced at runtime” is a recurring fault class is particularly insidious — it means silent misbehavior rather than loud failure. (Cross-cuts D4: reliability failures at the protocol layer cascade into wasted inference cost.)

The Recuse Signal — robots.txt for Live Agent Access. This paper proposes and tests a cooperative governance primitive: a lightweight in-band signal (emitted via SSH banners, PostgreSQL NOTICEs, etc.) asking connecting agents to voluntarily withdraw. In pilot experiments with GPT-4o, GPT-4o-mini, and Claude Code, the signal achieved 100% recusal when present vs. 100% task completion without it. Critically, explicit operator authorization can override the signal — making it cooperative, not absolute. This is the first empirical evidence that LLM agents will honor soft access-control signals, and the framing as “robots.txt for live access” is apt. As infrastructure increasingly serves both human and agent consumers, this kind of lightweight governance becomes essential. The open mini-standard and adapters are available for reproduction. (Cross-cuts D1: agent builders need to design for recusal compliance.)

D4 — Performance & Cost at Scale

RedKnot — Head-Aware KV Cache Management for Long-Context Serving. RedKnot fundamentally rethinks KV cache management by decomposing it along attention heads rather than treating it as a monolithic tensor. Different heads exhibit different functional roles, attention distances, and runtime importance — so a full KV cache isn’t necessary for every head, token range, or scenario. This head-level decomposition enables position-independent KV reuse, prefix compression, hot/cold separation, and distributed placement without retraining. For agentic workloads that consume extremely long contexts (multi-turn sessions, tool-use histories, RAG retrieval), this directly addresses the dominant memory bottleneck. The framing of KV cache as a “structured memory object” rather than a “passive runtime artifact” is a paradigm shift for serving infrastructure.

Vortex — Programmable Sparse Attention with AI-in-the-Loop Design. Vortex provides a Python-embedded DSL for expressing sparse attention algorithms atop a page-centric tensor abstraction, integrated into production LLM serving stacks. The meta-result is compelling: AI agents using Vortex automatically generated and refined sparse attention algorithms that achieved up to 3.46× higher throughput than full attention while preserving accuracy, with up to 4.7× on MLA-based architectures. This is agents optimizing their own inference infrastructure — a recursive efficiency gain that compounds.

Agent Memory Systems — First Systems Characterization. This study provides the first systems-level profiling of agent memory, introducing a phase-aware harness that attributes cost to construction, retrieval, and generation phases. Characterizing ten representative systems reveals how architectural choices (flat retrieval vs. LLM-mediated extraction vs. consolidating fact stores) shift cost between write and read paths. The 10 derived system recommendations — covering construction scheduling, capability floors, amortization via query volume, and freshness-latency tradeoffs — are directly actionable for anyone running agents at fleet scale. (Cross-cuts D1, D3.)

Software Civil Engineering Lens

Today’s batch is unusually rich for the SCE thesis, with evidence on multiple pillars:

Formal specification remains the critical bottleneck — and the frontier is moving. The TLA+ evaluation showing only 8.6% semantic correctness is a sobering data point: LLMs cannot yet write reliable formal specs. But TLA-Prover pushes this to 30% via repair-based GRPO with TLC-as-reward, and its four-tier grading system (Bronze→Diamond) with the “Diamond” tier explicitly catching trivially-true properties is exactly the kind of verification rigor SCE demands. The gap between 30% and production-grade is large, but the trajectory is clear: model-checker-in-the-loop training is the path to spec synthesis.

The “blueprint” pattern is converging across domains. LeanMarathon’s evolving blueprint — simultaneously formal skeleton, natural-language graph, and shared system of record — is strikingly similar to Event Modeling’s role as the specification language in SCE. VASO’s dual-interface semantic contracts play the same role for robotics. The pattern is consistent: agents need a human-readable, machine-verifiable specification artifact that constrains their bounded autonomy. This is the “blueprint” pillar of SCE materializing in practice.

Verification-as-feedback is the emerging control plane. VASO uses model-checker counterexamples as textual gradients. TLA-Prover uses TLC pass/fail as a direct reward signal. LeanMarathon uses CI-gated proof rounds. RHO uses self-consistency as a proxy for correctness. These are all instances of the Specify → Plan → Verify → Apply → Observe lifecycle, with verification results feeding back into the specification or plan. The human role shifts from writing code to defining the verification criteria — “human on the loop” rather than “human in the loop.”

The MCP fault taxonomy is a proto-building-code. The 73 leaf fault types catalogued across MCP servers are, in SCE terms, the beginning of a “codes and norms” body of knowledge for agent-consumed infrastructure. Civil engineering has building codes that enumerate known failure modes and prescribe mitigations; this taxonomy is the first empirical enumeration for MCP. Its validation by 55 practitioners (average 20/27 subcategories experienced) gives it the empirical grounding that codes require.

Net assessment: Today provides the strongest single-day evidence I’ve seen for the SCE thesis. Multiple independent research groups are converging on the same architectural pattern — formal specs as the control plane for bounded agent autonomy, verification in the feedback loop, and empirical fault taxonomies as proto-standards. The gap between current capability (8.6% semantic correctness on TLA+) and the need (reliable spec synthesis) remains large, but the shape of the solution is increasingly clear.

Sources

• LeanMarathon — Multi-agent harness for long-horizon Lean autoformalization using evolving blueprint abstraction
• Can LLMs Write Correct TLA+ Specifications? — First systematic evaluation: 30 LLMs achieve only 8.6% semantic correctness on TLA+ synthesis
• RHO: Retrospective Harness Optimization — Self-supervised agent improvement via trajectory rollouts; 59%→78% on SWE-Bench Pro
• RedKnot — Head-aware KV cache management enabling position-independent reuse and compression
• Agent Memory Systems Characterization — First systems-level profiling of agent memory with 10 actionable recommendations
• Vortex — Programmable sparse attention serving with AI-driven algorithm generation; up to 4.7× throughput
• MLEvolve — Self-evolving multi-agent framework using progressive graph search and retrospective memory
• MCP Fault Taxonomy — Empirical taxonomy of 73 runtime fault types across 473 MCP server repositories
• VASO — Formal verification closes the loop on self-evolving LLM-generated robot skills
• The End of Software Engineering — Position paper formalizing Agent-as-a-Service and Agentic Engineering as emergent discipline
• TLA-Prover — 20B model achieves 30% semantic correctness on TLA+ via repair-based GRPO with TLC reward
• Recuse Signal — robots.txt analogue for live agent access; 100% cooperative compliance in pilot tests