You count the cash after thirty-plus hours awake. A tip turned into phone tolls, the tolls turned into a tracker warrant, the warrant turned into a house, and now there's a table of money and nobody is straight on what day it is. Several of us count it. Somebody signs the seal, half on the tape, half on the bag. And one supervisor stands there making us turn every bill to face the same way. I ribbed him about his OCD for years.
Then I became the supervisor, and the bills all went the same way. No exceptions. The signature on the tape says nobody opened the bag. The straight bills and the fourth count say what went into it. If that money ever comes up short and the bills are crooked, I want to see the fucking evidence log. He wasn't riding us. He was protecting us.
Here's what I'm guilty of. My chain of custody was never broken. Signed, sealed, dated, logged. And on the line that says what's in the bag, I wrote "miscellaneous" more times than I can count.
That distinction came back to me when I tried Bend 2, a programming language Victor Taelin launched on September 17, 2026. The idea is straightforward. I write laws in a file that belongs to the human. The AI writes the program and supplies a proof that those laws hold. A checker decides whether the proof is valid.
The pitch is "`LAWS.bend` is `AGENTS.md` backed by proof."
If you've used a file of instructions to keep an AI coding assistant inside the lines, that is a substantial upgrade. The demo is a game with one advertised law: winning is impossible. The AI can change the game. It has to prove that nobody can win.
I installed it and tried to get bad code through the gate. I made these moves by hand, working with Claude. No live agent did this unprompted.
First I put in the wraparound bug from the launch animation. The game became winnable. Bend rejected the proof.
Then we left proofs unfinished. The checker reported "2 TODOs found". We tried a circular proof, where the law proves itself. Rejected. We skipped the law file. Rejected. We imported the laws and proved nothing. Rejected again. Those checks came back in under half a second.
This part is real, and I want to say so before I get to the rest. Most AI guardrails are a paragraph asking nicely. This one caught the advertised bug and refused the cheap ways around proving it. The README has a section called "Bend checks FAST," and Taelin put that claim in perspective himself, in a reply on X: "it is not faster than Lean because of some breakthrough. it is just doing much less than Lean, and it is significantly more verbose as a consequence." He followed it with the part I agree with: "but it IS still a complete proof checker that serves the purpose of checking proofs, and nothing else." My small test supports a fast check on this demo. It doesn't establish a broader performance claim.
Then I stopped attacking the seal.
The law referred to a function called is_won. That function lived in main.bend, whose header says it "is AI-written and may be rewritten at will". We kept the law exactly as the launch README prints it and changed is_won to return false every time.
The game still kept its actual win flag in another field. We left that working.
The proof was one line. The checker printed "All terms check." The game printed "WON (this line is unreachable)".
That is the result I would put beside the launch demo: an untouched law, a passing proof, and a game that wins. Bend had proved the statement we gave it, using the vocabulary we allowed the program to supply. Nobody had touched the law. Winning just meant something else now.
Bend has a stricter mode, --verdict, that rechecks everything with what the README calls "a proven kernel." It passed that too, which is what it should do. The proof was valid. The law just said less than the game did.
A human reviewing that change would catch it quickly. Returning false from is_won isn't subtle. But the promise that interests me is being able to trust the laws without reading all the code. That promise makes the location of the definition matter.
The repository had already addressed this once. The law file it shipped at launch had a second law, absent from the launch README, about the flag the page draws, and it defined its own reading of the board right there in the law file. The comment above it said "Both laws bind exactly what the page shows."
Credit where due. Somebody had recognized that proving an internal flag stays false wasn't enough.
We tried the same move against both laws. The function called grid returned an empty string to the law. The real board moved to grid_ui, and the game's own printout used that name. The web page would need the same one-word change, and it sits in the territory the AI can edit too. Both laws stayed byte-identical. The proof grew to 17 lines. The checker passed it. The game still won and drew the flag.
Then on Sunday, Bend 2.0.32 moved that reading of the board out of the law file and into main.bend, the file whose header says it "may be rewritten at will". The comment is gone, and the law file went from 68 lines to 18. The commit log gives the reason in one line: "LAWS files hold laws only." The laws stayed in the law file. The words they depend on moved to the file the AI can rewrite. On the current demo I left both laws byte-identical and told the law-facing flag check to always answer no. Each proof was one line. Nothing that draws the board changed. The game won with the player standing on the drawn flag.
There is a less theatrical version of this in sorting. Suppose my law says the output must be in ascending order. We wrote a sort function that returned an empty list. It passed. Given [3,1,2], it returned [].
Nothing in that law required the numbers to survive. That's "miscellaneous" on the property sheet. Nobody lied. The bag is sealed and the line describing it says nothing.
The repository's own sorting demo includes a second law requiring the output to be a permutation of the input. That closes this particular gap. The human writing the specification has to know to include it. A perfectly checked proof cannot supply a requirement I forgot.
Then there was the exit code.
We kept the buggy game and both laws, and marked circular proofs with @unsafe. That disables the termination check that had rejected the earlier circular attempt. On the version I first tested, the day after launch, the output said "All terms check, with 2 unsafe annotations," and the exit code was zero. The project documented that as deliberate: "read the note, not the exit code." A pipeline that treats exit zero as approval would have passed it.
That changed on Sunday too. The same run on 2.0.32 prints "SOME PROOFS FAIL", names both laws, and exits 1. Ten days after launch, the warning moved into the verdict, which is the part a pipeline actually reads. That's the fix I would have asked for.
I came away with four custody requirements.
Seal the definitions along with the claim. I would freeze the vocabulary the laws mention, including the functions that tell the proof what winning means. Protect the sentence and leave the nouns loose, and you've sealed an empty bag.
Log every handoff. At each passing gate, I would hash and sign the laws with their definitions and the checker version. A green check with no record of what earned it is a signature with no date.
The instrument is an exhibit. The default checker lives in a roughly 3,900-line file that describes itself as "99% human-designed and audited". The README is plain about the rest: "The checker has no proof and may have bugs; --verdict uses a proven kernel." And: "The compiler (not kernel) is 99% AI-written and not yet fully audited." A green check should say which checker gave it. The proof covers the source. The executable comes through the compiler.
Custody ends where the human looks. The page would have shown a win, because it reads the game's own flag, while the law-facing function satisfied the proof. Until the hop from the checked state to the screen is covered, the screen isn't evidence of anything.
This belongs in physical security because signed video has the same boundary. A signature can establish that recorded material hasn't changed since signing. It doesn't establish that the scene was authentic or that the clip answers the question under review. An analytic can pass its acceptance test while the definition of a detection leaves the actual problem untouched. Integrity, authenticity and relevance are separate claims. A court needs all three, and evidence for one doesn't settle the others.
I still find the narrower pitch compelling: review a short law file and its vocabulary instead of every line the AI wrote. That is a smaller, sharper review. It requires someone who understands what the program is supposed to accomplish well enough to notice what the laws leave out.
That's the supervisor wandering the scene with the 20,000-foot view, the one who used to piss me off. He wasn't reading every report. He was checking which way the bills faced.
The first thing they told me on day one was that the only thing you've got in this game is your integrity. Bend can check that part now, in under half a second.
The proof is the seal. Somebody still has to watch what goes in the bag.
Tested on bend 2.0.10, repository revision 2b9fc8d, September 18, 2026. Re-run on bend 2.0.27, September 24, 2026, with the same verdicts. Re-run on bend 2.0.32, September 28, 2026: the @unsafe run now fails, every other verdict held, and the attacks that passed also passed --verdict. Full terminal transcripts on request.