Chronograph

Graph View

2026-09-18

10 min read

Martin Rosén-Lidholm
Martin Rosén-Lidholm

Daily D4 Digest — 2026-09-18

TL;DR

  • MAGS achieves 100% formal safety verification of agent-generated code across CUDA, terminal scripts, and robotics by using Dafny as an intermediate representation — the strongest SCE signal this quarter
  • A long-horizon agent architecture demonstrates 10-day autonomous operation with human attending once daily, using hierarchical time-scale levels and cascaded model escalation
  • SoL-Pi cuts coding agent token costs by 45-49% through recursive self-improvement of the harness layer, with estimated savings of $8-13/hour vs. native Codex/Claude Code
  • FINSKILLOPS introduces controlled skill lifecycle management for self-evolving agents — only 6 of 33 proposed patches survive promotion gates, reducing error rates from 20% to 12.5%
  • A proposed Internet of Agents trust architecture tackles the missing layer below MCP/A2A: scalable agent identity, registration, and capability-based discovery at 19K+ registrations/sec

Call to Action

  • Evaluate MAGS for your CI pipeline: if you’re generating CUDA or infrastructure scripts with agents, the Dafny-based verification loop is production-ready and addresses the spec-to-verify gap directly — paper
  • Adopt harness-level cost controls now: the empirical harness study shows rule-based elision before LLM summarization is the best context management strategy — implement this in your current agent harnesses before optimizing models — paper
  • Track the Internet of Agents identity layer: if you expose APIs to third-party agents, the registry-suffix identity scheme is a concrete proposal for the trust infrastructure you’ll need — paper

D1 — Agentic Engineering

Long-horizon agents need architecture, not bigger context windows. Nijkamp et al. present a hierarchical architecture with three components: levels indexed by time-scale (each maintaining a bounded summary file of the level below), clocked “ticks” as the atomic unit of autonomous action, and cascaded intelligence where work escalates to more capable models only after failing review. In a 10-day campaign reproducing an RL result with a human attending once daily, the agent maintained coherence across every context reset and session boundary. The key insight for D1 practitioners: operating knowledge written early changed later behavior with no weight changes — the harness is the memory, not the model. This directly supports the “human on the loop” transition. (Also D4: cascaded intelligence is an explicit cost-control mechanism.)

Empirical decomposition of coding agent harness design reveals component-level tradeoffs. Fan et al. fix the execution loop and vary three components — planning, action space, and context management — across 176 matched settings on SWE-Bench Verified and Terminal-Bench 2.1. Key findings: (1) context management’s primary value is preventing overflow failures, not improving reasoning; (2) rule-based elision staged before LLM summarization beats all other strategies; (3) planning shifts from accuracy scaffold for weak models to cost saver for strong ones; (4) bash-only interfaces achieve lower cost than predefined tools for bash-capable models. This is the kind of controlled experiment the agentic engineering field desperately needs — isolating variables in agent systems rather than benchmarking monoliths.

ScientistTwo demonstrates end-to-end autonomous research with multi-agent orchestration. This framework takes a research problem as input, establishes baselines, formulates hypotheses, coordinates specialized agents through an end-to-end discovery cycle, and validates via a simulated peer-review rebuttal engine. Benchmarked against ICLR/ICML/NeurIPS-accepted papers, it generates solutions that outperform human SOTA and receive higher automated review ratings. While the evaluation methodology (AI reviewing AI-generated papers) warrants skepticism, the orchestration pattern — specialized agents coordinated through a structured discovery lifecycle — is directly applicable to D1 engineering workflows beyond research.

FormalFlow coordinates AI proving agents for 126K-line Lean 4 formalization in 63 days. Lu et al. completed a machine-checked proof of a core theorem underlying MIP* = RE using a shared blueprint to guide nested planning, proving, and review loops. All 126,367 lines of Lean code were agent-generated. The system corrected side conditions and intermediate errors while preserving published error bounds. This is a compelling demonstration of agents operating within formal constraints — the blueprint-guided loop pattern maps directly onto spec-driven development. (Also SCE: strong evidence for the “shared blueprint” → “bounded autonomy” pipeline.)

D2 — AI in the Product

Self-evolving financial QA with controlled skill lifecycle management. FINSKILLOPS reframes post-deployment improvement of AI products as “controlled behavioral maintenance”: recurring failures become scoped skill patches that must pass targeted validation, regression checks against protected cases, and negative controls before promotion. In a 12-round operational study, only 6 of 33 proposed skills survived promotion — yet this disciplined admission drove non-correct rate from 20% to 12.5%. The pattern — typed failure diagnosis → scoped patch → regression gate → versioned deployment — is directly transferable to any production AI system that needs to improve without breaking. (Also D4: this is fundamentally about downstream reliability and reducing support-tier escalation.)

Auditing AI-generated hardware verification plans exposes the schema-acceptance trap. SecTB-RTL found that of 1,857 AI-generated verification responses accepted by the provider schema, only 9 passed production semantic validation. The authors preserve this as an “instrument-validation incident” rather than reporting results — a remarkably honest paper. The lesson for D2: provider or schema acceptance ≠ execution validity. If you’re shipping AI-generated artifacts into safety-critical pipelines, you need production-path validation, not just format compliance.

D3 — Build for Agents

A DNS-like architecture for agent identity and discovery at Internet scale. Zhang et al. propose a three-layer trust discovery architecture for the “Internet of Agents”: Agent Root (trusted registry governance), Agent Registry (registration and metadata), and Agent Resolver (distributed capability discovery). The system introduces registry-suffix-anchored composite identities and dual-certificate authentication. A prototype achieves 58ms registration latency, 25ms discovery latency, and 19K+ registrations/sec. This addresses a real gap: current protocols (MCP, A2A) handle tool invocation and communication but assume you’ve already found and authenticated the agent you want to talk to. This is the missing DNS/PKI layer for B2A.

CoreSense provides auditable decision gating for robotic agents. This architecture combines traceable episodic evidence with a conflict-aware belief gate that checks scope, provenance, time, contradiction, and support before permitting action, requesting re-observation, abstaining, or escalating. On safety benchmarks, belief gating reduced unsafe proceeds from 20-40% to 0%. While robotics-focused, the pattern — a structured gate between recalled evidence and action that can PROCEED/ABSTAIN/ESCALATE — is directly applicable to any agent making consequential decisions. (Also SCE: this is bounded autonomy with explicit escalation paths.)

D4 — Cost of Ownership

Pattern-level inference cuts LLM costs by ~1000× while maintaining equivalent accuracy. This deployed pipeline at a major Japanese bank recasts user profiling from per-user to per-transaction-pattern LLM inference, achieving a close to three-order-of-magnitude reduction in inference targets when profiling tens of millions of users. The resulting database is statistically indistinguishable from per-user inference in AUC. This directly serves the 2× output / ½× cost equation: same analytical output, radically lower inference spend. The architectural insight — identify the natural deduplication boundary in your domain and run inference there — is broadly applicable beyond banking.

Recursive harness self-improvement yields 45-49% token reduction at equivalent performance. SoL-Pi takes an RSI-inspired approach to optimizing coding agent harnesses, discovering four reusable mechanisms (action execution, context compaction, observation handling, delegated reading) that survive selection across diverse environments. On EdgeBench, it matches Pi performance on GPT-5.6 Sol and Opus 5 while cutting token traffic by nearly half and API cost by about a third — estimated hourly savings of $8.75-$13.50 vs. native Codex/Claude Code. This is the agentic factory cost side: as agents run continuously, harness-level token efficiency compounds into significant OpEx reduction.

FINSKILLOPS’ controlled skill promotion reduces downstream error rates. The FINSKILLOPS skill lifecycle — where only 6 of 33 proposed patches survive regression gates — demonstrates that disciplined admission control for self-improvement directly reduces downstream support burden: the non-correct rate falling from 20% to 12.5% means fewer escalations to human review tiers. The “protected-case regression check” pattern is essential: without it, self-improving systems create exactly the kind of unpredictable behavior that drives support costs up.

Software Civil Engineering Lens

Today is one of the strongest days for the SCE thesis in recent memory. Three papers independently converge on the same core insight: formal specifications as the control surface for autonomous agent work.

MAGS is the headline. Using Dafny as a verification-aware intermediate representation with frozen, human-audited API specifications, it achieves 100% success in producing formally verified programs across CUDA, terminal scripts, and robotics. This is the Specify → Plan → Verify → Apply → Observe lifecycle made concrete: humans audit the spec (Specify), agents generate code (Plan), Dafny checks it mechanically (Verify), violations are repaired via verifier feedback (the ralph loop), and verified code compiles to executable output (Apply). The honest caveat — failures occur “when the auto-formalized semantics do not fully capture the target behavior” — is itself an SCE lesson: the specification is the ceiling of the guarantee.

FormalFlow reinforces this from the mathematical formalization side. A shared blueprint guiding nested planning-proving-review loops is exactly the “blueprints for software” analogy made literal: 126K lines of Lean 4, all agent-generated, all machine-checked. The 63-day timeline for a landmark proof — previously a multi-year effort — demonstrates the 10% → 10× transition when human judgment is relocated to the specification level while agents handle proof engineering.

S4L→Prolog (the traffic rules formalization work) shows structured reasoning prompts improving NL-to-logic translation from 60% to 75% for legal rules — modest accuracy, but the approach of semantic role extraction → scene completion → logical mapping → rule generation mirrors the four-stage pipeline civil engineers use when translating building codes into structural calculations.

The FINSKILLOPS skill lifecycle and SecTB-RTL instrument-validation incident both point toward the “codes and norms” pillar. FINSKILLOPS implements what amounts to a building code for agent self-improvement: regression gates, negative controls, versioned retirement. SecTB-RTL demonstrates why you need them — schema acceptance without production-path validation is the software equivalent of approving a blueprint without checking it against local building codes.

The through-line: we’re seeing the emergence of verification-aware intermediate representations (Dafny, Lean 4, Prolog) as the “material datasheets” of software construction — machine-checkable contracts between human intent and agent execution. The gap is narrowing on formal spec and simulation pillars; licensure and education remain wide open.

Sources