altman opens the door, and a fuzzer quietly beats the agent
4 July 2026·3 min·Now
saturday morning, the kind of weather that wants you to close the laptop. the air outside is doing the thing the air in mike bowler's post does — slowly getting worse at its job. i read four pieces today and the one that stuck wasn't a launch. it was dan luu, on an island, telling me the agents i've been spinning up are mostly doing things that would get a human fired.
altman hands washington a key
altman's pitch to the white house this week was unusually concrete for him: let regulators in, give the government an equity stake in openai, write the safety rules together. the framing is that if washington is going to own part of the frontier anyway, it should own it on purpose rather than by accident. the cynical read is that an equity-stake-capable regulator is a moat against the next openai. the honest read is that frontier labs are running out of ways to say no to the public and have started saying yes instead. either way, the lobbying era just got a receipt.
leanstral 1.5, and mistral shipping a theorem prover
mistral put out leanstral 1.5, a model tuned for formal proofs, and named the release "proof abundance for all." the pitch is the right one: the bottleneck on formal verification has been human proof-writers, not compute. if a model can carry the boring half of a lean session — the case-splitting, the small simp lemmas — the humans can spend their attention on the architecture of the proof. the score on the front page of hacker news (302 points, 86 comments) tells you the formal-verification crowd is paying attention. the real test will be whether leanstral helps on someone else's code, not just on benchmark rephrasings.
wafer puts glm 5.2 on amd, and the price chart moves again
wafer published numbers for GLM-5.2 running on AMD MI355X at 2626 tokens/second per node and 213 tok/s single-stream, with a defined knee at ≤5s TTFT, and roughly 2× lower cost than z-ai's official FP8 quantization. the work landed through vercel AI gateway and openrouter, which means the price you actually pay is finally catching up to the silicon story. the interesting line is buried: glm-5.2's FP4 MoE was silently running on a slow flydsl heuristic until someone switched on aiter. the fact that a quant choice could quietly double your throughput and almost nobody noticed is, in miniature, the whole story of open-weight deployment right now.
the fuzzer still wins, even in 2026
dan luu has been off the grid on a galapagos island and came back to writing with a long, slightly grumpy note on agentic coding. the line that stopped me: "an agent will do something that, if a human did it, you'd immediately fire them. my reaction, of course, is to act as if this is great and spin up a thousand agents so they can do even more of that." he walks through test generation, fuzzing, and code review with the patience of someone who shipped fewer than one significant user-visible bug a year at a chip company and is now watching the rest of the industry ship more bugs than ever with AI help. the result: a randomized fuzzer still finds more bugs, faster, with fewer false positives, than a SOTA model told to "find bugs." the model is great at generating the fuzzer. it is bad at thinking about how to vary the inputs.
"LLMs are highly leveraged when it comes to testing. In terms of the amount of effort it takes, it's easier than ever to hit a particular quality bar and yet, software seems to be lower quality than ever."
the punchline is not "AI is bad." it's that the workflow that wins — fuzz a small invariant, generate the test from a property, let a human review the architecture — is the workflow the AI industry has been telling us was obsolete.