Projects

This is the most interesting thing I have linked all week, and it is a polygon library.

Multipolygon intersection, formally verified in Lean 4. The author states plainly that the implementation and the proofs were written autonomously by agents and never reviewed by any human, including him. Opus 4.5 through 4.8, with the later model able to formulate and execute large proof strategies on its own.

So why is this not the horror story it sounds like?

Because of what a human does review: three specification files, eighty-seven lines of Lean, defining polygon interiors by ray-casting parity. That is the entire trusted surface. If those eighty-seven lines say what you meant, then the Lean checker guarantees the implementation satisfies them — for every input configuration, not for the cases someone thought to test. The implementation is more than twice that size and considerably harder to follow, and it does not matter, because nothing rests on a human understanding it. As the README puts it, trust comes from the checker and a small specification, not from the model.

Sit with that, because it is a genuine answer to the problem this site keeps circling. Every other route out of the verification bottleneck has been about making review faster — better diff tools, AI reviewers, risk scoring. All of them are still asking a human to look at generated code and decide. This changes what gets reviewed: not the code, but a statement of what the code must be true of, in a form a machine can check exhaustively.

The catch is the obvious one. It works here because "these two polygons intersect correctly" is expressible in eighty-seven lines of maths. Write the specification for your billing system and see how far you get. The domains where this applies — geometry, parsers, compilers, crypto primitives, data structures — are exactly the domains where formal methods already worked, and the contribution is that the expensive part, the proofs, has got dramatically cheaper.

That is not nothing. That is the barrier that kept formal verification out of industry for forty years, and a model in a loop with a proof checker just walked over some of it. If the specification-writing gets easier too, this stops being a niche result.

Mac Budkowski built Cryptosaurus, a small app that turns your profile picture into a dinosaur. The prototype took an hour. Shipping it took about a hundred.

The value of this writeup is entirely in the itemisation, because "the last 10% takes 90% of the time" is a cliché until someone tells you exactly which hundred hours. His: design iterations on palette and layout; over two hundred prompt iterations to make image generation survive the range of real profile pictures; AWS plumbing, S3, Lambda, domains, deployment; access control, a multisig wallet and nonce handling for the contract; rate limiting and load testing; five hundred beta users; and then a launch-day scramble when concurrent transactions broke the thing.

Not one of those is the part an agent was good at.

His framing — that AI accelerates the first 90% and leaves the rest — matches what everyone reports, but I think the split is slightly wrong, or at least badly named. It is not that the last 10% is harder. It is that the first 90% is the part with a specification, and the remaining work is where the specification gets discovered: by hitting a profile picture that breaks the prompt, by watching a stranger misuse the interface, by two transactions landing at once. You cannot delegate discovering what you are building. You can only delegate building it once you know.

Which is why "I built this in an afternoon" and "I shipped this" remain different sentences, and why the gap between them is not closing as fast as the demo videos suggest.

Two things I would hold onto. The two hundred prompt iterations is the real number in this piece — an enormous amount of the work was iterating on the instructions, not the code, and nobody's productivity metric captures that. And the launch-day concurrency bug is exactly the sort of defect that no test suite you would have thought to write catches, which is the argument for Rootly's blast-radius approach rather than for more careful review.

An honest post about a silly app is worth three serious posts about transformation.

Jonathan Corbet on a submission to OpenBSD's tech list: Thomas de Grivel sent in an ext4 implementation with full read and write support that passes e2fsck, lacking only journalling. He was straightforward about where it came from — generated with ChatGPT and Claude, with, in his words, careful code review and error checking on his part.

It was rejected, and the reasons are more interesting than the rejection.

Theo de Raadt went to provenance: "the chances of us accepting such new code with such a suspicious Copyright situation is zero." Damien Miller pointed at the liability of shipping code whose ownership is unsettled. Christian Schulte raised the GPL-licensed ext4 documentation and what that might mean even for an independently written implementation.

But the objection that will outlive the legal ones came from Tyler Anderson, who asked who maintains code when its original "author" does not understand it and has no personal investment in it.

That is the question, and it is not really about AI. A filesystem driver is a thirty-year commitment. Somebody has to be there at 2am in 2034 when a corruption report comes in against a code path nobody has looked at since it was written. The reason projects care who wrote something is not credit — it is that authorship has historically been a decent proxy for somebody understands this and will still be here. Generated code severs that proxy in a way a copyright-assignment form cannot restore.

Worth noting what this is not. It is not a claim that the code is bad. It might be excellent; passing e2fsck with read-write support is not nothing. OpenBSD declined it anyway, because a project that accepts code on the strength of "it seems to work" has already lost the thing that makes it OpenBSD.

The copyright argument will get resolved eventually, one way or another. The maintenance argument will not.

Nir Barak at Reco had a JSONata problem: the reference implementation is JavaScript, their policy engine is not, and crossing that boundary cost about 150 microseconds per evaluation across billions of events — roughly $300k a year in compute to keep an RPC fleet alive purely as a language adapter.

So he had a model rewrite JSONata 2.x in Go. Seven hours. $400 in tokens. Thirteen thousand lines, passing all 1,778 test cases from the reference suite. They call it gnata, and it is in production.

Every instinct I have says to be sceptical of this post, and every specific thing in it survives the scepticism. Look at what they actually did before promoting it: code review, then preprod in shadow mode, then live only after three consecutive days of zero mismatches against the reference implementation while processing billions of real events.

That is the part to steal. This was not "the tests pass, ship it" — the tests passing was table stakes, and 1,778 of them is a luxury most projects rewriting something would kill for. The actual verification was a differential oracle running on production traffic, where the existing implementation votes on every result the new one produces. You cannot always get that. When you are reimplementing a specification that already has a reference implementation and a conformance suite, you can, and this is what it looks like done properly.

Which is also the limit of the story. This is the friendliest possible shape of problem for an agent: a closed, well-specified language with an executable definition of correct, and a free oracle sitting right there. Almost nothing in your codebase looks like that. The seven hours is not the transferable part.

On the money: $500k/year is $300k of RPC fleet plus about $200k from a later refactor that gnata made possible. The second number is doing a lot of work in the headline, and it is a projection of a projection. The $300k is the one I believe.