An error message in one of my tests turned into ZZZZZZZZ7000ZZZZ….
Pipit, my Go interpreter, runs a program inside another Go program, the host. The host had kept an error after the interpreted function returned.
A few dozen runs later, it read the error again and got those Zs. Nobody had changed the error. Later runs had reused the memory holding its text.
My fix cleared all eight hazards the tests could reproduce. Then an AI wrote a model of the design. It used Coq, a proof assistant. The model found four more ways to reuse storage while something still pointed into it.
That is why I'm throwing my hat in the ring on how to build software with AI. I'm calling this proof-led development. Now I've got rules I can check while the code changes, and sequences I hadn't thought to test.
I lean on linters, research papers and proofs to question the model's work. The proofs were never on my list.
Something I can check
Ask a model for the same fix twice and it can suggest two different implementations, which is fine if I have a way to judge them that doesn't change with the next answer. Alternatives are welcome. I'd also like to know which one works. With the same inputs and version a linter applies the same rules. A proof checker checks the formal argument it receives. I can change the proposed implementation and run those checks again, without asking the model whether it still thinks its answer is good. That's why I want deterministic checks. Pin down the rule or source, then let the model work against it. A repeatable check can enforce the wrong rule too, so choosing what it checks remains my job.
In Joining the Jev hype, I give the model small statements to assess and keep the evidence beside its answers. Here I want rules I can rerun against the implementation, so I can find the disagreement while I'm still working on the change.
A linter for every rule
Writing a linter used to feel like a project in itself.
Now I can ask an AI to turn some obscure rule of mine into a check and have something to try in minutes. Even a fairly involved rule can be quicker to cover than I'd expect.
Go does a lot of the groundwork. go/ast exposes the program's structure, and the analysis framework supplies type information too. I check what the generated linter accepts and rejects. Then I can run the rule with every change instead of explaining it again.
Hand it the paper, even if it's read it
A model may have seen a paper during training. Did it keep the exact numbers and arguments, or only the gist of them? Being trained on them doesn't mean it can recall them accurately when I ask. I put the PDF in front of it anyway, so we can both return to the actual argument. Papers do a different job. They give me a definition, result or passage to inspect. My interpretation can still be wrong, but I can return to the page and work out where I got it from, because the source is there independently of the conversation.
I keep my own corpus of papers, and AI helps me find things to put in it. It's particularly useful when another community has a name for the problem I'm trying to describe, because then I have existing work to learn from and assumptions I can inspect. And the problem I'm describing may already have an entire literature. I'd rather read that than ask the model to keep elaborating my version of it. The source lets me separate what the authors established from what we're inferring about my code.
Proofs were never on the list
Writing enough tests used to be a chore, and AI has taken a lot of that chore off my hands. Wait, proofs? I would never have thought to write those as well, that wasn't a chore I was putting off, it was a different career.
OpenAI has released Lean formalisation alongside its claimed Navier–Stokes result. Its later collection contains hundreds of maths manuscripts. Some of their headline results have formal proofs.
That makes me interested in trying formal tools on a small piece of my own system.
For the error message that piece is permission to reuse memory. Pipit allocates values in arenas, groups of storage it manages together. An arena can contain several slabs, blocks holding things such as string bytes or slice elements. Reuse can avoid fresh allocations each run.
Go keeps referenced memory alive, but reachability doesn't stop my arena overwriting it. Is that storage still mine to reuse?
The fix gives it a licence. When a value escapes to the host, Pipit revokes permission to reuse the storage behind it. Revoked storage is left to Go's garbage collector, which can reclaim it when it is no longer reachable. Within that lifetime revocation only goes one way.
I can explain that rule without any Coq. Do the operations keep it true? A return is an obvious place to look for an escape. A later store through a pointer takes more following.
AI makes it practical for me to try this without first learning to write all the proof steps myself, but I still have to understand the system it writes down. What can retain a reference? Which operations may reuse storage? What has the model left out?
The AI wrote around 3,400 lines of Coq, with 25 kinds of step covering allocation, stores, returns, callbacks and the other relevant operations.
The policy describing the prototype cites the Go file and line behind each choice. I can follow a questionable rule back into the engine and compare them.
I have to inspect that mapping. Coq can check an argument about those rules without knowing whether I've described Pipit faithfully.
If the model is too large for me to read, I've lost the ability to judge that description.
The safety condition says that nothing the host or interpreter can still reach points at storage reused underneath it. The model calls retained references roots and its units of storage chunks. A reference becomes stale when the storage it names is reused.
Here's the condition in Coq:
(* Invariant G: no root is stale and no reachable chunk holds a stale reference. *)
Definition InvG (s : state) : Prop :=
(forall v, In v (all_roots s) -> stale v = false) /\
(forall c ck, get_cell s c = Some ck -> reach_roots (st_cells s) (all_roots s) c ->
stale (ck_slot ck) = false).
I can follow that without knowing how to prove it. The meanings of roots, reachability and reuse have to match the behaviour I care about, though. An agreeable-looking final sentence can't supply the missing operations.
Was the proof checker asked to take the missing step on trust? Coq permits Admitted, which leaves a claim unproved, and axioms, which introduce assumptions.
My proof gate rejects those shortcuts. It checks that each audited result is closed under the global context, with no unproved assumptions left behind.
I deliberately inject an Admitted to check that the gate refuses it.
The Replay Lattice's public proof gate audits assumptions too. Its model permits eight named assumptions, while this arena model's audit permits none.
An explorer tries sequences of operations in the Coq model within a fixed size and depth limit. It found four families of storage-reuse failures.
A proof that I was right would have been more convenient.
A pointer can outlive the protection
One sequence keeps a pointer to a slice element, then writes a new string into that element. I could protect the slice when the pointer escapes and call that done, until the later store gives the outside pointer new bytes to reach. The string doesn't exist when the pointer escapes. Those bytes are still available for reuse. That write needs to protect the new value too.
Trying the sequences in Go
In the Go tests all four failures reproduced on the old code. None reproduced on the repaired experimental branch. In the model the repaired policy passes the bounded checks too. I haven't yet proved that it keeps the model safe in general.
Check what was formalised
The model itself needed correcting too. An early safety condition rejected a legitimate chain of nested callbacks even though no memory had been reused. The condition had to change, rather than the implementation.
Proof of what, though? In the OpenAI example, Alexander Bastounis, Fabian Circelli and Anders Hansen argue that its Lean proof doesn't correspond to the paper's proof. A proof checker can accept the formal argument while the connection to the written one remains disputed. I have to read what was formalised to judge that connection.
For Pipit I now have failure sequences and rules the repair needs to preserve. That gives the AI a much better brief than "please fix the arena". I can write the implementation myself and still use AI for the formal work. I'd take that over most bug reports.