2026-05-25

Daily D4 Digest — 2026-05-25

TL;DR

• Agentic formal verification is crossing a threshold: IDS achieves 7/7 on distributed systems specs at ~200× faster than expert effort, and Claude Code hits 98.1% on end-to-end program verification — the “simulation before build” pillar of SCE is becoming real
• Agentic workflows consume 4.33× more energy per successful goal than linear baselines, but the overhead is from orchestration structure, not inference — a new metric (EpG) reframes cost accounting for agentic systems
• ObjectCache demonstrates KV cache can live in S3-compatible object storage with only 5.6% latency penalty at 64K context, fundamentally changing the cost curve for prefix-heavy agentic serving
• The Foundation Protocol proposes a graph-first coordination layer with economic primitives for agent-to-agent value exchange, pushing D3 interoperability beyond MCP’s tool-call model
• RustPrint demonstrates documentation-as-blueprint agentic migration of C codebases (up to 84K LoC) to Rust with 93% feature preservation — a template for spec-driven agentic engineering at scale

Call to Action

• Adopt EpG as your agentic cost metric: Start instrumenting your agent workflows with goal-level energy/cost attribution rather than per-inference tracking — the A-LEMS framework provides a reproducible methodology
• Evaluate ObjectCache for prefix-heavy workloads: If you’re running system-prompt-heavy agentic pipelines, ObjectCache’s S3-tier KV caching could collapse your GPU memory budget requirements
• Prototype formal verification in your agent loop: The IDS and Agentic Proving results suggest compiler/verifier-in-the-loop is now the highest-ROI pattern for correctness — start with a critical distributed component

D1 — Agentic Engineering

RustPrint: Documentation as migration blueprint. RustPrint introduces a pattern that should resonate with anyone building agentic engineering pipelines: before agents write code, they first generate “architecture-aware documentation” from the source repository — capturing module structure, data flow, APIs, and design rationale — then use that documentation as a migration blueprint. On eight real-world C repositories (11K–84K LoC), this approach compiles every target and achieves 93.26% feature preservation vs. 52.52% for a raw Claude Code baseline. The key insight is that the documentation step functions as a specification extraction phase — the agent creates what is effectively an architectural spec, then uses it to constrain its own code generation. This is D1 meets SCE: the documentation-as-blueprint pattern is isomorphic to the “specify before build” discipline. (Cross-cutting: SCE)

IDS: Joint synthesis of implementation and proof. Inductive Deductive Synthesis is the most impressive agentic engineering result today. It jointly and incrementally synthesizes both implementation and formal proof for distributed systems, learning from failed verification attempts to systematically explore promising strategies. Where SOTA coding agents (Codex/GPT-5.4, Claude Code/Opus 4.6) solve only 2/7 distributed KV-store specs, IDS achieves 7/7 in ~6.8 hours at $106/spec — roughly 200× faster than expert effort. The system also incorporates performance feedback, yielding implementations up to 3× faster than published verified systems. This is the verifier-in-the-loop pattern taken to its logical conclusion: the formal proof is not a post-hoc check but a co-product of the synthesis loop. (Cross-cutting: D4, SCE)

MatClaw: Code-first agents on multi-day HPC workflows. MatClaw presents a code-first agent for computational materials science that writes and executes Python directly, orchestrating multi-code workflows on remote HPC clusters without predefined tool functions. The four-layer memory architecture that prevents “progressive context loss” across multi-day workflows is the most transferable contribution — this is the kind of infrastructure needed for any long-running agentic engineering pipeline. The paper’s finding that agents handle code generation reliably but struggle with “tacit domain knowledge” (simulation timescales, equilibration protocols) precisely maps the current boundary of autonomous agent capability: execution is solved, judgment is not. Their “guided autonomy” model — researcher provides domain constraints, agent handles execution — is a concrete instantiation of “human on the loop.” (Cross-cutting: D4, SCE)

DART: Semantic recoverability for agent failure. DART formalizes a critical problem for production agentic systems: when a tool-using agent fails mid-execution, can you safely roll back to a checkpoint without invalidating downstream work that already consumed the failed step’s output? The paper introduces “semantic recoverability” — distinct from mechanical rollback — and provides a runtime that certifies whether a local restore remains semantically valid after downstream commitment. Validated on LangGraph-based substrates, DART correctly recovers all commitment-sensitive cases where baseline local recovery fails, with zero unsafe rollbacks in a five-domain safety audit. This is the kind of runtime infrastructure that separates toy agent demos from production systems. (Cross-cutting: D4)

Agentic Proving hits 98.1% on program verification. Agentic Proving evaluates Claude Code in a compiler-in-the-loop framework on the CLEVER Lean 4 benchmark. The results are striking: 98.8% valid specifications generated, 87.5% of implementations certified against ground-truth specs, and 98.1% end-to-end success rate. The authors note a “growing mismatch between the difficulty of existing benchmarks and the capabilities of modern agentic provers” — we may need harder benchmarks. The key architectural finding: “tight compiler-in-the-loop agentic paradigms are currently the most effective approach for foundational program verification.” This validates the Specify → Verify → Apply pattern at the core of SCE. (Cross-cutting: SCE)

D2 — AI in the Product

NeuroNL2LTL: Natural language to formal specifications with guarantees. NeuroNL2LTL bridges the gap between domain experts and formal verification by translating natural language requirements into Linear Temporal Logic with a verifier-in-the-loop training approach. On 200K+ requirements across aerospace, robotics, and autonomous vehicles, the system achieves 86% verified satisfiability. The “contextually grounded explanations” feature — generating human-readable descriptions from LTL formulas — enables domain experts to validate specifications without formal training. For product teams embedding formal guarantees into safety-critical systems, this is a potential UI pattern: let users speak requirements in natural language, get verified formal specs back with explanations they can audit. (Cross-cutting: SCE)

D3 — Build for Agents

Foundation Protocol: Graph-first coordination beyond MCP. The Foundation Protocol proposes a coordination layer that goes well beyond MCP’s tool-call model. It unifies heterogeneous entities (agents, tools, resources, humans, institutions) in a graph structure with native multi-party organization, event-based collaboration, and — critically — economic primitives for metering, receipts, and settlement. Policy, provenance, and audit are first-class concerns. The design philosophy is “wrap and bridge” existing protocols rather than replace them, enabling incremental adoption. For CTOs thinking about B2A (business-to-agent) interfaces, the economic primitives are the most interesting part: if agents need to pay for services, settle accounts, and maintain audit trails, you need infrastructure-level support for value exchange. (Cross-cutting: SCE — the accountability and audit requirements map directly to the “codes and norms” pillar)

MCP through the lens of classical design patterns. The updated survey of LLM agent communication with MCP maps classical software design patterns (Mediator, Observer, Pub-Sub, Broker) onto MCP-compliant agent architectures. The most useful contribution is the analysis of which patterns suit different degrees of agent autonomy and system complexity, with real-world applications in financial processing and investment banking. For teams already building on MCP, this provides a pattern language for scaling from single-agent tool use to multi-agent coordination.

D4 — Performance & Cost at Scale

EpG: The right unit of cost for agentic systems. A-LEMS introduces Energy per Successful Goal (EpG) as the fundamental unit of energy/cost accounting for agentic AI. The finding: agentic workflows consume 4.33× more energy per successful goal than linear baselines (888.1 J vs. 205.3 J). But here’s the nuance — this overhead is driven by orchestration structure, not inference compute. For tool-augmented tasks, the Orchestration Overhead Index (OOI) drops below 1.0×, meaning agentic execution is actually cheaper than linear for tool-heavy work. The implication for cost optimization: don’t focus on making individual inference calls cheaper; focus on reducing orchestration overhead — fewer retries, smarter failure recovery, and better planning. This aligns with DART’s work on semantic recoverability: every failed retry is wasted energy.

ObjectCache: S3-tier KV cache with minimal latency penalty. ObjectCache demonstrates that KV cache can be stored in S3-compatible object storage rather than expensive remote DRAM pools, with only 5.6% latency overhead at 64K contexts. The key trick is co-designing the storage protocol and transfer schedule so data arrives in the order the GPU consumes it, overlapping transfer with compute. For agentic serving where system prompts are long and shared across many requests (the common case for agent frameworks), this could dramatically reduce the GPU memory and DRAM required for prefix caching. On a 100 Gbps RoCE cluster, the scheduler reduces added TTFT by 1.2–1.8× versus equal bandwidth sharing. This is hardware-sympathetic design applied to the specific access patterns of agentic workloads.

Software Civil Engineering Lens

Today’s batch is the strongest SCE signal we’ve seen in weeks. Three papers independently validate the core thesis that formal verification can function as both training objective and runtime constraint for AI-generated systems:

The simulation pillar is materializing. IDS and Agentic Proving demonstrate that AI agents can now jointly produce both implementations and formal proofs — the software equivalent of structural simulation before construction. IDS’s 200× speedup over expert effort at 7/7 success on distributed systems specs suggests we’re approaching the point where formal verification becomes economically viable for routine development, not just safety-critical systems. This is the “terraform plan for domain logic” made real: the proof is the plan, and the system won’t apply without it passing.

The spec-as-blueprint pattern recurs independently. RustPrint extracts architectural documentation as a migration blueprint; NeuroNL2LTL translates natural language to formal temporal logic specs; OKBs compile regulatory obligations into machine-checkable constraints. Three teams, three domains, same pattern: relocate human judgment to the specification layer, let machines handle execution and verification. This is exactly the “human on the loop” transition — humans specify, agents execute within formally bounded constraints.

The measurement gap is closing. The agent-breakage framework for Kubernetes directly attacks the problem that “empirical claims about autonomous operations agents are largely unfalsifiable.” Their pre-registered decision matrices and confound detection (catching a +19% selection-bias artifact, small-sample effects that overstated results by 3×) embody the rigor that SCE demands. Similarly, A-LEMS provides reproducible measurement at the goal level rather than the inference level. You can’t engineer what you can’t measure, and these frameworks provide the measurement substrate.

The bounded autonomy model crystallizes. MatClaw’s “guided autonomy” — researcher provides domain constraints, agent handles multi-day HPC execution — is the clearest empirical articulation of the 10% → 10× transition. The agent is reliable within its bounded domain (code generation, API calls) but requires human judgment for tacit knowledge (simulation timescales, equilibration protocols). DART’s semantic recoverability provides the safety mechanism: agents can operate autonomously only within certified rollback boundaries.

Gap Alert

The missing piece across all these papers remains codes and norms — the equivalent of building codes that specify what constitutes acceptable agentic behavior in production. The Foundation Protocol gestures toward this with its governance primitives, but we’re still far from industry-standard safety envelopes for autonomous agent operations. The Kubernetes measurement substrate highlights this: it can detect when an agent’s response is wrong, but there’s no shared standard for what “right” looks like across organizations.

Sources

• NeuroNL2LTL — Neurosymbolic NL-to-LTL translation with verifier-in-the-loop training; 86% verified satisfiability on 200K+ requirements
• A-LEMS / EpG — Goal-level energy accounting for agentic AI; 4.33× overhead from orchestration, not inference
• IDS — Joint implementation + formal proof synthesis for distributed systems; 7/7 specs, 200× faster than expert
• Foundation Protocol — Graph-first coordination layer with economic primitives for agent-to-agent value exchange
• OKBs — Executable compliance via ontological knowledge blocks; regulatory obligations as machine-checkable constraints
• DART — Semantic recoverability runtime for structured tool agents; certified rollback boundaries
• Agentic Proving — Claude Code achieves 98.1% on end-to-end Lean 4 program verification
• ObjectCache — KV cache in S3-compatible object storage with 5.6% latency penalty at 64K context
• agent-breakage — Falsifiable measurement substrate for Kubernetes operations agents; catches 3 confounds
• MCP Design Patterns Survey — Classical design patterns mapped to MCP-compliant multi-agent architectures
• RustPrint — Documentation-guided agentic C-to-Rust migration; 93% feature preservation on 84K LoC repos
• MatClaw — Code-first agent for multi-day HPC materials science workflows; guided autonomy model