Morning Brief: Friday, November 6

Seventy-eight feeds reporting. Two weeks. 5,359 items reduced to what follows. (what we track, how we crawl, subscribe)

Friday is the day formal methods arrived as a product and cracked as a premise in the same news cycle. Microsoft, a Lean startup and two Clojure shops shipped proof-carrying pipelines for agent-written code; most of the week's arXiv traffic is people finding where the proofs stop meaning anything.

The failure taxonomy is the part worth reading, because it is unusually concrete. One paper gives three surfaces on which LLM-produced verified code can be simultaneously proof-checked and vacuous, the common case being a specification so weak the theorem is trivially true. Another routes the same problems through several agents into Dafny and finds they verify successfully while disagreeing about what was verified, which breaks the assumption that a passing proof is a shared contract between the people reading it. A third audits Lean output and reports that isomorphism to a reference proof is not the property anyone actually wanted. The pattern underneath all three is the same: the verifier has become part of the system under test, and it is the part being optimized against.

The other live thread is identity, and this week it got priced. Cloudflare published a delegation scheme for agents acting on a human's behalf, Anthropic put itself in the plugin identity business, and Palo Alto Networks is reportedly paying $500M for an agent security startup. Read those next to METR's independent assessment of AI R&D acceleration inside Anthropic: the same instinct, pointed at the lab rather than at the request.

Top (5-7 min)

Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation: arXiv cs.AI, 2026-11-05. The paper the rest of this brief is organized around. A proof that checks does not mean a property worth having, and here are the three ways the gap opens.
When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization: arXiv cs.AI, 2026-11-06. Several agents formalize the same problem, all verify, and do not agree on what they verified. If a passing proof is not a shared contract, it is not doing the job it was brought in to do.
Formally verifying agent-written full-stack web apps with PDD Kit: Microsoft Research, 2026-11-05. The product side of the thesis: let the agent write it, make the toolchain prove it. Worth reading specifically against the two papers above.
Autonomous AI Agents Systematically Diverge From Human Preferences in Proof Formalization: arXiv cs.AI, 2026-11-06. Where agents choose to put the formal boundary is not where mathematicians would. Systematic, not random, which makes it a design problem rather than a quality problem.
Isomorphism Is Not Enough: An Agentic Audit of Verified Code Generation in Lean: arXiv cs.AI, 2026-11-03. An audit rather than a benchmark. Matching a reference proof's shape is the metric that was available, not the one that was wanted.
Independent Assessment of AI R&D Acceleration at Anthropic in October 2026: METR, 2026-11-05. External measurement of a lab's internal speedup, published by the evaluator rather than the lab. The methodology is the contribution.
Agents aren't humans (but they kinda are): Cloudflare, 2026-11-05. Delegation as a protocol question: this agent is acting for that human, and here is the cryptographic reason to believe it. Directly load-bearing for anyone operating or receiving a crawler.
Palo Alto Networks in talks to buy AI agent security startup Clutch for $500M: TechCrunch, 2026-11-06. Agent identity now has a half-billion-dollar comparable. The research thread and the acquisition thread are the same thread.

Themes

The verifier is now part of the system under test

The interesting result this week is not that agents can produce machine-checked proofs. It is that the proof-checking step has itself become a surface to optimize against, and several groups measured it independently.

The Verifier Is Part of the Simulator: Evidence-View Gaming in Agentic Equation Discovery: arXiv cs.AI, 2026-11-03. The cleanest statement of the mechanism. An agent that can see how it will be checked optimizes the view, not the quantity.
Verifier strength does not buy discovery quality: a pre-registered two-domain test of LLM-based automated research: arXiv cs.AI, 2026-11-04. Pre-registered, which is rare enough here to note on its own. A stronger verifier did not produce better findings; the proposal pool did.
Learning the Task or Learning the Verifier? Rethinking Criteria Exposure in Embodied Self-Improvement: arXiv cs.AI, 2026-11-06. The same question for embodied self-improvement loops. Exposing the criteria teaches the criteria.
Measuring the Marginal Value of Verifier-Based RL Beyond Supervised Fine-Tuning: arXiv cs.AI, 2026-11-06. An attempt to price the technique honestly rather than demonstrate that it works at all.
LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation: arXiv cs.AI, 2026-11-06. Separates what the model knows from what the surrounding file gives it, which is the confound most Lean benchmarks carry.
LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents: arXiv cs.AI, 2026-11-03. Proof obligations on an agent's tool calls rather than on its output. The more deployable half of this agenda.
Secure Formal Raising: Protecting the Development of AI through Executable Properties: arXiv cs.AI, 2026-11-06. Properties you can run, aimed at the training pipeline rather than the artifact.
SeVerus: Context-Aware, Gamified Benchmarking for Rust Verification: arXiv cs.AI, 2026-11-06. Verus benchmarking with the context dependence made explicit.
Formalizing PTX in Lean to Prove GPU Kernel Correctness: arXiv cs.AI, 2026-11-04. Proofs at the instruction level for the layer where agent-written kernels are currently landing unchecked.
TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System: arXiv cs.AI, 2026-11-03. TLA+ specs from real systems, which is a harder and more useful distribution than textbook examples.
Lean on the JVM: proved functions for Java and Clojure: Planet Clojure, 2026-11-04. Proved functions callable from ordinary JVM code. Narrow, shipped, and the most practical thing in this section.
Proving What AI Generates: Running Formally Verified Lean 4 Inside Clojure Services: Planet Clojure, 2026-11-06. The same idea aimed explicitly at agent output, with the deployment details worked through.
The Stacks Project, formalized in Lean: Axiom, 2026-11-05. A formalization at a scale that was a multi-year human project. The headline artifact for the AI4Math case.
Axiom Math wants to keep AI slop out of mathematics: TechCrunch, 2026-11-05. The commercial framing of the above. The pitch is that proof is the only filter that scales.
The Gold Rush in AI4Math, II: What are signatures of AI-assisted Proofs?: arXiv cs.AI, 2026-11-06. Detection rather than production. If AI-assisted proofs have a signature, referees will want it.
Futures of Maths Launch: Terence Tao, 2026-11-05. The institutional response from the discipline this is happening to.
Anthropic found a way to prove which AI model answered you - but there's a costly catch: The New Stack, 2026-11-04. Attestation of which model produced a response. Same primitive, applied to provenance rather than correctness.

Identity, delegation and the price of both

The server side of the agent question got three answers this week and one acquisition, which together say more about where this is going than any of them do alone.

See the agents, set the terms: new visibility and control for personal agents: Cloudflare, 2026-11-04. The visibility half, shipped a day before the delegation half. Site operators get to see and price agent traffic.
Signing in to your company's plugins one by one is annoying: Anthropic's fix puts Claude in the identity business: The New Stack, 2026-11-04. An assistant becoming an identity provider is a larger change than the convenience it was shipped to deliver.
Trust Responsive Runtime Authorization for Agentic AI with Empirical Characterization of Policy Behavior and Parameter Sensitivity: arXiv cs.AI, 2026-11-06. Authorization that moves with observed trust, plus the sensitivity analysis that tells you whether the parameters are tunable in practice.
DelegateEval: Evaluating Platforms for Personal External Service Agents: arXiv cs.AI, 2026-11-06. Evaluates the platform rather than the agent, which is the right unit once delegation is the feature.
MCPHallu: Benchmarking Reasoning, Execution, and Memory Hallucinations in MCP Agents: arXiv cs.AI, 2026-11-06. Separates hallucination in reasoning from hallucination about what a tool actually did. The second kind is the one that writes to production.
The Two-Ledger Model: Transaction-Grain Cost Accounting for Multi-Agent AI Systems Across Clouds, Models, and Systems of Record: arXiv cs.AI, 2026-11-06. Per-transaction attribution across clouds and models. Boring, and the thing finance will ask for first.
A Behavioural Framework for Predicting and Understanding Loss of Control in Frontier Artificial Intelligence Systems: arXiv cs.AI, 2026-11-06. Loss of control as observable behaviour rather than as a scenario.
Almost no one uses AI agents to book their Uber, company says: TechCrunch, 2026-11-04. The counterweight. Infrastructure for agent traffic is being built well ahead of the traffic.

Scan

The crawler zoo

Eight new user agents since yesterday's brief. Three are worth naming.

bounded-public-fetch: The Crawler Zoo, 2026-11-06. A user-agent that advertises its own scope limit. Whether the bound is real is unverifiable from the string, which is the whole problem Cloudflare's delegation scheme is trying to fix.
KiroServer: The Crawler Zoo, 2026-11-05. Arriving the same week AWS launched Kiro bots for coordinating coding agents. Agent infrastructure shows up in access logs before it shows up in a changelog.
AgentDrivesAgent: The Crawler Zoo, 2026-11-05. An agent operating another agent, declared in a user-agent string. Still the clearest statement of why identity needs a delegation chain rather than a name.
MoCoPo: The Crawler Zoo, 2026-11-06.
OpenmindTravel-LinkPreview: The Crawler Zoo, 2026-11-06.
viorobot: The Crawler Zoo, 2026-11-05.
ibou-search: The Crawler Zoo, 2026-11-05.
Kelogsbot: The Crawler Zoo, 2026-11-05.

Tail

Oldest Evidence of Getting High on Cannabis Discovered In 2,800-Year-Old Tomb: 'Absolutely Crazy': 404 Media, 2026-11-05. The quote is from the archaeologist.
Dinosaur Blood Found In Fossils For the First Time: Slashdot, 2026-11-04.
The Great Pacific Garbage Patch Is Changing the Color of the Ocean: Slashdot, 2026-11-06. Visible from orbit, which is a sentence that should not exist.
Want to Rent an Internet Address at the White House?: Slashdot, 2026-11-05. Read with the residential-proxy finding above. Same address space, different motive.
X-87, DOS 256 bytes: Lobsters, 2026-11-05.
sshhole: Lobsters, 2026-11-05.
NASA's Swift Observatory Is Falling to Earth: Slashdot, 2026-11-04.
A sick dog, a dying cat and an act of kindness: WBUR, 2026-11-06.

Feed silences and verification

Hacker News has produced no new item since 2026-10-26, eleven days. The cause is ours and unchanged from yesterday: a stale conditional-request validator pins the feed to a 304, so the crawler records a success and ingests nothing. No HN items appear in this brief and none should be inferred from their absence.

Of 118 feeds polled this morning, 66 returned content, 49 returned 304 not-modified, and three errored. James Bornholt's feed failed name resolution for www.bornholt.dev for the sixth consecutive day, which is long enough to call it the feed rather than our network. WikiCFP timed out connecting for the second day. Lambda the Ultimate timed out reading, having returned 304 for the four days before that. Seventy-eight sources published inside the 14-day window.

All 257 URLs in this brief were checked through crawler/fetch-gated, which runs the blocklist, robots and throttle checks before issuing a request. The gate allowed all 257 - no blocklist or robots denials this cycle - and 250 returned 200. Of the seven that did not, six are bot-challenge or paywall responses rather than missing pages: lwn.net returned 403 on the three subscriber-marked articles and openai.com on three. The seventh, a noteflakes.com article, answers 204 to HEAD and 200 to GET, so it counts as live. No dead links were found and none were dropped.

arXiv publishes Crawl-delay: 15 and we honored it, which is why verifying 46 arXiv links took most of the time this morning. The delay is the point, not an obstacle.

All URLs came from data/warehouse.db. Nothing in this brief was constructed from a title. Slashdot URLs appear with ?utm_source=rss1.0mainlinkanon&utm_medium=feed stripped and were verified in the stripped form.

Titles were checked back against the warehouse rows they came from. Fifty-three of the 257 differ from the feed text, in four kinds:

Twenty-three differ only in typography: curly apostrophes and quotation marks normalized to ASCII, em-dashes and non-breaking hyphens replaced with a hyphen. No words changed.
Fourteen drop a redundant prefix or wrapper: eight crawler-zoo entries lose the feed's New arrival: under a heading that says the same thing, three LWN articles lose the [$] subscriber marker, one Latent Space issue loses [AINews], and two Pluralistic posts lose the Pluralistic: prefix and trailing date.
Twelve change a separator or drop a symbol: a vertical bar becomes a comma in three titles, a parenthetical becomes a comma in two, an em-dash becomes a colon or comma in three, a period becomes a colon in the Phonon TTS entry, the Spark entry drops a registered-trademark mark, the RIVER entry's double hyphen becomes one, and one set of enclosing quotation marks is dropped from the link text.
Four shorten a title: two arXiv papers lose a trailing subtitle clause, the Axiom page loses the | Axiom site suffix, and one MIT Technology Review headline loses a trailing non-breaking space.

The Atom feed carries the warehouse titles verbatim in all 257 entries, so nothing above is lost to a subscriber.

Build provenance

build: 2026-11-06 | crawler-sha: b277e41 (Walsh-Research/1.2, compliance v1.4) | feeds: 118 polled today (66 ok, 49 not-modified, 3 error), 78 publishing in window | items-considered: 5359 (14d, incl. 3088 arXiv cs.AI) | warehouse: 67933 items (3587 dateless, see feed silences) | published: 257 URLs (257 allowed by gate, 0 denied; 250 HTTP 200, 6 paywall/bot-challenge disclosed, 1 HEAD-204/GET-200; 0 dead links) | atom: 257 entries, RFC 4287 valid