---
title: 'In the News: October 22, 2026 (Evening)'
description: 'Anthropic reports Claude proved no-crash properties on 123 open-source libraries at the machine-code level, and two engineering teams describe how they gate agent work with deterministic checks.'
canonical_url: 'https://darkfactory.dev/news/2026-10-22-evening'
markdown_url: 'https://darkfactory.dev/news/2026-10-22-evening.md'
collection: news
date_published: '2026-10-22T19:12:00-04:00'
date_modified: '2026-10-22T19:12:00-04:00'
---

# In the News: October 22, 2026 (Evening)


Anthropic says Claude wrote machine-checked proofs that 239 fuzz entry points across 123 open-source libraries cannot crash on inputs up to 64 MB, and found bugs along the way. Two engineering posts from Snap and Imprint describe the other half of the same problem: how much agent output can be trusted when the checks around it are written in code.

## 1. Anthropic and Theorem report Claude proving no-crash properties on 123 open-source libraries

**[LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification)** · Keane Lucas and co-authors, Anthropic, in collaboration with Theorem · Anthropic Research, October 22, 2026

The team turned existing fuzz tests from Google's OSS-Fuzz project into formal specifications over compiled RISC-V binaries, then had Claude write the proofs and a Rocq proof checker validate them. The post reports proofs for 239 entry points in 123 libraries, about 180 million lines of Rocq in total, with a typical proof near 600,000 lines. Where proving failed, Claude patched the bug it found and proved the patched version. The authors say some of those bugs are ones a fuzzer would be unlikely to reach, including a counter underflow that needed inputs of around 20 MB with one rare layout.

The cost figures are the part to read closely. The authors say proofs can take hundreds of millions of tokens. On 36 small tasks, they report Opus 5.5 proving half of them with about 40% fewer tokens than Opus 5, and agents that could copy each other's proofs used 17% fewer tokens than agents working alone.

The limits are stated in the post. The proofs assume a single-threaded static RISC-V binary on Linux, and the authors write that "formally verified" does not mean bug-free, since a proof is only as good as the spec and the machine model. These are first-party results. We read the post body; the appendix was not read and we did not check the published proofs.

**Why it matters:** If the cost keeps falling, a fuzz test becomes a spec and a proof becomes a check that does not depend on trusting the agent that wrote it. That is a different verification loop from reviewing generated code, and worth watching for anyone deciding what a factory should demand before merge.

## 2. Snap describes an experiment loop where the harness is deterministic and the agent works only at the edges

**[Alchemist: Agentic ML Experimentation](https://eng.snap.com/alchemist)** · Snap Inc. engineering blog, October 2026

Snap's ML engineers run an agent platform called Alchemist, built around a harness that validates plans, submits runs, polls results and enforces budgets as code the agent calls rather than behavior it improvises. The agent proposes hypotheses at the start and recommends next steps at the end. Per the post, each plan is approved by the sha256 fingerprint of its file, an edited plan counts as unapproved, and the harness never retries a failed step on its own.

For its first recipe, feature selection, Snap reports a drop from four weeks to two per cycle and 30% of model features removed with no regression in the study's evaluation metrics. The baseline was one manual study on a Story ads model: four weeks, 130 workflow submissions, one engineer. That is a single comparison reported by the team that built the system, and the post gives no independent measurement.

**Why it matters:** The design choice is the useful part. Snap puts the steps that must not vary into code and treats approval as a hash of the plan, which is a pattern a spec-and-verify pipeline can borrow without taking on Snap's numbers.

## 3. Imprint's "small-change" lets automated checks approve a narrow class of pull requests

**[Speeding up code review with small-change](https://lethain.com/small-changes/)** · Will Larson, Imprint · Irrational Exuberance, October 17, 2026

Larson reports that Imprint's average engineer merges 4x more pull requests than two years ago, and that median review time rose from 33 to 77 minutes. A pull request qualifies as a small-change if it is under 1,000 lines, has no P1 or P2 findings from the team's review bot, comes from an author with 10 or more prior merged PRs in that service, and stays within a limited number of services. Shared libraries are excluded. A review skill then approves or ignores qualifying PRs, and it never comments, which Larson says avoids "meat proxy review." Any error from a small-change is treated as a system failure to fix in the checks.

Larson says it is too early for results: about 10% of changes qualify so far. He also reports incidents down 42% and critical incidents down 78% half over half. Those figures describe the company's overall trend, and the post does not tie them to small-change.

**Why it matters:** This is a worked example of replacing per-PR human review with eligibility rules and a stricter standard for errors, with its limits stated. Whether it holds depends on how fast the verification coverage grows, which Larson says himself.