Daily D4 Digest — 2026-07-20
TL;DR
- Generative compilation embeds compiler feedback during LLM code generation, not after — a “sealor” transforms partial Rust programs into compilable forms mid-decode, with soundness proved in Lean
- Counterexample-supplemented sketches formalize a human-on-the-loop workflow where coding agents evolve spec-shaped sketches through operator-approved policy corrections — the spec, not the prompt history, carries domain knowledge
- Cache-Aware Prompt Compression (CAPC) achieves 49-90% cost savings over naive strategies by jointly optimizing prompt caching and compression, validated on three production workloads including a 94k-token schema prefix
- A cloud-scale MCP gateway scales agent tool access to 3,000+ tools with 23.8× token reduction and 8.9× faster selection, addressing real production pain in the MCP ecosystem
- MirrorCode benchmark shows frontier models can reimplement 16k-line codebases from behavior specs alone at 56% success rate — but at $2,600/attempt, the D4 cost question is inescapable
Call to Action
- Evaluate CAPC for your agentic pipelines: If you’re running tool-calling agents with large system prompts, the cache-aware compression approach could cut inference costs 50%+ — the tier-preserving ratio bound is the key insight to implement
- Prototype generative compilation for your Rust/typed-language codegen: The sealor technique works with black-box models, no constrained decoding needed — evaluate whether it reduces your agent code-fix loops
- Assess MCP gateway architecture for multi-tool agents: If your agents touch >50 tools, the gateway pattern with hybrid retrieval may be more viable than stuffing tool schemas into context
D1 — Agentic Engineering
Generative Compilation: Compiler-in-the-Loop Code Generation. This paper introduces a genuinely novel primitive for agentic coding: instead of the standard generate→compile→fix loop, a “sealor” transformation converts partial programs into compilable units during generation, feeding compiler diagnostics back before error cascades form. The technique is proved sound on a core Rust calculus (mechanized in Lean) and works with black-box models — no white-box constrained decoding required. On repository-level Rust tasks, it reduces non-compiling outputs and improves functional correctness versus post-generation feedback. This is a concrete instance of the SCE thesis: bringing formal verification tooling into the generation loop itself, rather than treating it as an afterthought. (Also relevant to D4 — fewer fix cycles means less inference cost.)
Counterexample-Supplemented Sketches: Evolving Specs Through Failure. This work formalizes something many teams do ad-hoc: when a coding agent fixes a bug, it often loses the rule behind the fix, leading to repeated mistakes. The method starts with a human-authored “sketch” (partial spec in code shape), lets the agent generate, then evolves the sketch through operator-approved counterexamples. The critical insight: periodic clean regeneration from the evolved sketch (without prompt history) tests whether the spec itself — not accumulated context — carries the learned policy. In a GPT-5.4-mini experiment, the evolved sketch passed 19/21 withheld cases vs. 15/21 from the initial sketch with all examples replayed. Retaining code across counterexamples cut API calls from 15 to 9 and artifact churn from 2,394 to 719 lines. This is spec-driven development emerging from practice. (D1/SCE cross-cutting.)
MirrorCode: Behavioral-Spec-Driven Full-Program Reimplementation. MirrorCode benchmarks whether AI agents can reimplement entire software projects (25 programs across Unix utils, interpreters, crypto, compression) from behavioral specifications alone — no source code access, just end-to-end test matching. The strongest model scores 56%, and can reimplement a 16,000-line bioinformatics toolkit. The benchmark design is notable: it’s structure-agnostic (no scaffold, no file hints) and uses black-box differential testing. The finding that agents produce overwhelmingly monolithic code structures despite being free to architect suggests current agents lack the software design reasoning needed for professional-grade engineering. (D1/SCE cross-cutting.)
CLI-Tool-Bench: 0-to-1 Generation Remains Hard. CLI-Tool-Bench complements MirrorCode with a structure-agnostic benchmark for ground-up CLI tool generation across 94 real-world repositories. The top model achieves only 43.8% success, and the paper surfaces an important anti-pattern: higher token consumption does not correlate with better performance. Agents tend toward monolithic generation and struggle with autonomous repository planning. The black-box differential testing methodology — comparing system-level side effects in sandboxes against human oracles — is itself a contribution to how we should evaluate agentic code generation.
ARC-AGI-3: Verification Beats Raw Model Power (But Barely). This ablation study on ARC-AGI-3 agents decomposes the contribution of executable world models, scheduled simplification, and exact replay verification. The most robust finding: stronger models and higher reasoning effort always help, and the differences between architectural variants are smaller than expected. The full verification treatment ranks first in all settings but uses substantially more resources. With gpt-5.6-sol, the verification variant saturates the public set — but this is a model-contamination-adjacent result. The implication for agent design: invest in verification infrastructure, but don’t over-engineer the representation when model scaling does most of the work.
D2 — AI in the Product
No significant standalone D2 developments today. The generative compilation work (D1) has D2 implications for IDE-integrated AI coding assistants — real-time compiler feedback during generation could transform the UX of AI pair programming from “generate-then-fix” to “generate-correctly.”
D3 — Build for Agents
Cloud-Scale MCP Gateway: The Enterprise Tool Access Layer. This production-deployed system addresses the real operational pain of MCP at scale: legacy service incompatibility, context window limits when mounting large tool sets, and session affinity for stateful backends. The gateway consolidates incompatible MCP variants, provides access control, and uses hybrid retrieval to achieve 98% Top-15 recall across 3,000+ tools — reducing tool selection time by 8.9× and token usage by 23.8×. This is the infrastructure layer that MCP needs to become enterprise-viable. The architectural decision to break the direct-connect model and route through a gateway echoes API gateway patterns from the microservices era. (Also D4-relevant for the token and latency savings.)
ToolVerse: RL Training Over 400 Real MCPs. ToolVerse builds agentic RL training environments from ~400 real-world MCP servers containing ~4,500 tools, addressing the chicken-and-egg problem of training agents to use tools they’ve never seen. The tool dependency graph approach for generating long-horizon tasks (GUST dataset) and the Turn-Aware Relative Advantage algorithm for credit assignment in multi-step tool chains are technically interesting. For the D3 lens: this validates MCP as the de facto interoperability layer by making it the substrate for agent training, not just inference-time tool access.
memorywire: Vendor-Neutral Agent Memory Protocol. memorywire proposes a JSON-Schema wire format for agent memory operations (remember, recall, forget, merge, expire) across four memory types, with an optional human-in-the-loop governance channel. The reference implementation includes adapters for sqlite-vec, mem0, Letta, Cognee, and pgvector. It explicitly positions itself as complementary to MCP rather than competing with it. The HITL governance surface — letting humans review writes before they enter long-term storage — is the most underappreciated feature. In a world of persistent agent memory, the provenance field and the ability to recover from poisoned stores (validated against PurgeBench) is a safety-critical capability.
D4 — Performance & Cost at Scale
Cache-Aware Prompt Compression (CAPC): The Joint Optimization Paper We Needed. This work resolves a tension that plagues every production LLM deployment: prompt caching and prompt compression are both cost-reduction primitives, but query-aware compression invalidates the cache on every call. The paper reveals that Anthropic’s Sonnet 4.6 cache has a two-tier architecture with a sharp threshold near 3,500 tokens (hit rate plateaus at ρ≈0.83), and builds a cost model around this reality. CAPC pairs query-agnostic compression with explicit cache_control and a tier-preserving ratio bound. Results: cheapest strategy in 16/16 LongBench-v2 configurations, 49% savings over cache-only, 64% over query-aware compression, 90% over vanilla — at quality within 0.05 of uncompressed. The enterprise tool-assistant validation (94k-token schema prefix, 51.7% cost reduction) is directly actionable for teams running agentic systems with large system prompts.
vLLM Configuration Tuning: Model Choice Dominates, But Config Still Matters. A 9,000-run study across 5 models and 5 tasks finds that attention kernel type and prefix caching are the primary levers for energy and latency in vLLM deployments, while chunked prefill has limited impact under default serving configs. The key takeaway: model choice dominates global trade-offs, but configuration tuning provides local Pareto improvements. The unexpected finding that inference configuration can affect model accuracy (not just speed/cost) deserves attention — it means your serving config is part of your quality assurance, not just your ops.
Software Civil Engineering Lens
Today’s selections paint a remarkably coherent picture of software engineering’s professionalization under agentic pressure, with advances across multiple SCE pillars:
Formal specification is emerging from practice, not theory. The counterexample-supplemented sketches paper is perhaps the most SCE-relevant work in weeks. It demonstrates the Specify → Plan → Verify → Apply → Observe lifecycle in practice: a human creates a partial spec (sketch), the agent builds, failures expose missing policy, the operator approves corrections, and the spec evolves. Crucially, the paper proves that the evolved spec — not the conversation history — carries the learned domain rules. This is the “blueprint” concept from Event Modeling manifesting in a coding-agent workflow. The periodic clean regeneration step is exactly “terraform plan for domain logic” — can we rebuild from the spec alone?
Simulation and verification are being integrated into the generation process. Generative compilation is the strongest evidence yet for the simulation pillar. By running the compiler on partial programs during generation (with soundness proven in Lean), it moves verification from a post-hoc check to a continuous constraint — analogous to how structural analysis runs continuously during civil engineering design, not just at the end. The sealor’s key property — never rejecting a possible-to-complete partial program — is a form of bounded autonomy: the agent retains creative freedom within proven-safe boundaries.
The “material datasheets” gap is becoming quantified. The vLLM configuration study and CAPC paper both contribute to understanding the “material properties” of our inference infrastructure — cache behavior, energy/accuracy trade-offs, configuration-dependent quality. Civil engineers don’t design with generic “concrete”; they design with C30/37 concrete whose properties are characterized in datasheets. We’re starting to build equivalent characterizations for LLM serving configurations.
The autoformalization pipeline is maturing. Monty automates the translation of natural-language specifications into formal executable assertions, improving precision by 20 points over naive LLM translation. This directly addresses the “codes and norms” pillar — the ability to express and verify compliance with domain rules. Combined with generative compilation and counterexample sketches, a pipeline is forming: natural language intent → formal assertion → verified code generation.
The human-on-the-loop transition is visible across today’s items: in CAPC, the human sets the caching strategy but the system optimizes within it; in memorywire, the human governs memory writes but doesn’t execute them; in counterexample sketches, the human approves policy corrections but the agent handles regeneration. We’re clearly in the 10% → 10× transition zone.
Sources
- Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code — Sealor transformation enables compiler feedback during partial Rust program generation, proved sound in Lean
- Agentic Synthesis against Counterexample-Supplemented Sketches — Evolving code-shaped specs through operator-approved counterexamples; spec carries policy, not prompt history
- Cache-Aware Prompt Compression — Joint optimization of prompt caching and compression achieving 49-90% cost savings on production workloads
- Scalable LLM Agent Tool Access in the Cloud — Production MCP gateway scaling to 3,000+ tools with 23.8× token reduction
- MirrorCode: AI can rebuild entire programs from behavior alone — Long-horizon benchmark for reimplementing entire codebases from behavioral specs
- ToolVerse: Unlocking Massive Environments for Agentic RL — RL training framework over 400 real MCPs with 4,500 tools
- memorywire: Vendor-Neutral Wire Format for Agent Memory — JSON-Schema protocol for agent memory operations with HITL governance
- CLI-Tool-Bench: Evaluating 0-to-1 Software Generation — Structure-agnostic benchmark for ground-up CLI tool generation; top model at 43.8%
- ARC-AGI-3 Agent Ablation Study — Verification treatment ranks first but model scaling matters more than architecture
- vLLM Configuration Trade-offs Study — 9,000-run study showing attention kernel and prefix caching dominate energy/performance
- Faithful Autoformalization of Natural Language Assertions — Monty framework improves LLM-based assertion generation precision by 20 points
- First-Order Modal Logic in HOL — Mechanized deep/shallow embeddings of first-order modal logic in Isabelle/HOL with automated faithfulness
