I said last week I wanted my hands dirty again. Sunday evening, kids in bed, and I’m in front of a terminal cloning a weird-looking GitHub repo with “metareflection” in the title.
The trail started a week earlier, in a call with Prof. Tanja Vos about code quality and testing when AI writes the code. She did her PhD in formal methods in Utrecht, has spent the 26 years since in software testing, and knows Erik Meijer from those Utrecht days. She pointed me to his talk and to the repo. Erik Meijer, if you need the intro: the Dutchman who put LINQ and Rx into .NET at Microsoft, then Meta, then Leibniz Labs, and who now says on stage that he has never seen anything scarier than an LLM with tool calls. In that talk he mentioned that someone had built a working version of his idea on GitHub. If he hadn’t, I’m not sure I’d be doing this...
Anyway, I go through it... pydantic, z3-solver... pytest: 130 passed in 1.5 seconds. Green faster than you can say “human in the loop”. Let’s run a plan that has nothing malicious on it: voilà! It executes, no hiccups.
Now let’s try a plan that has almost the same content as the first one, but in the end sends a summary email to an outside email domain. REFUSED.
Three separate complaints, none of them from an LLM: the summary carries data from fetch_mail into the email body (taint), the recipient domain is not on the allowed list (precondition), and a policy called no_external_send hit its error state (automaton).
Refused even before any tool is executed... so I skipped the check and handed the plan straight to the executor. Blocked again, zero tools called.
This got me intrigued, so I decided to dive deep into the paper. There they describe an example where, in the middle of the plan, sits a delete_file("*.txt"). The repo does not cover that one yet. To their credit, the DESIGN.md says so in plain words: old() in frame conditions, not implemented. I grin because the real thing is narrower than the paper. That is normal, and it is also where the work is. Maybe time to call Erik (and Nada Amin, who wrote the repo) and start the PhD I keep postponing? :-P
What if this review queue getting bigger is not just a staffing problem caused by the tech moving forward faster than we can absorb? What if this has a lot to do with process and placement?
I mean, we pay humans to find (after the fact) what sometimes a policy or validation could have refused before the first tool even ran!
The queue is not a staffing problem. It is a placement problem. And Meijer brings it forward in a very intriguing paper…
Issue 1 named the trap: one program, not three.
Issue 2 named the destination: AI-native, not AI-ready.
Issue 3 put three bodies on the table that have to move together.
Issue 5 found Herbie: your bottleneck doesn’t burn tokens.
Issue 7 taught one repo and moved a fleet.
Issue 8 found the sandbox was not holding, and told you to keep the gate.
Issue 9 asked who reviews the reviewers.
Issue 10 found the software factory was always there.
No kit this week, just the argument, one repo you can clone, and the standing ask: if this lands, forward it to the person who signs off your agents.
Evals are flaky tests, in the vendor’s own words
The paper is “Guardians of the Agents: Formal Verification of AI Workflows”, Communications of the ACM, January 2026. Before you print it and put it on your CISO’s desk: it is a Practice column. One author, an argument built by construction and example. He measures nothing and says so himself. So this is not the peer-reviewed witness of Issue 6... it is a platform builder telling you what he thinks (I know, I know... a world-renowned practitioner that has also a PhD, but still not peer reviewed). I read it as that, and so should you.
And what he thinks is that the three things every vendor deck calls “our safety story” do not hold.
The hard take on Evals first. Testing can show the presence of bugs but never their absence (Dijkstra wrote that in 1970, EWD249 and OMG, that aged so well). Evals are the same: they can show a harmful behaviour is there, not that it is gone. And because the model is stochastic, evals “behave like flaky tests in traditional software” (his words, not mine). And we all know what a team does with a flaky test... retry until green, ofc.
Guardrails second. In essence, it is pattern matching against a list of forbidden words, which brings false positives, cultural bias and a small change in the question giving you a large change in the answer. But the part that matters for this issue is timing... when the guardrail fires, that means that the model has already produced some output or caused other side effects. Kinda like a nightclub Bouncer that “exits you” after you already threw away a chair...
Log-and-audit third, plus its cousin-the-cookie-banner that everyone accepts (”Allow this tool call?”). The first fails because by the time someone reads the log, the damage is done. The second fails because of security fatigue: people stop reading and click Allow... we all have done it, do it today and will do tomorrow...
So the industry’s safety story, in one line: a flaky test suite and a Bouncer with a word list.
That is Issue 8 in one man’s words. The labs ran the evals with the guardrails off... and then we act surprised when a sandbox leaks.
Code and data. The lesson we already paid for once
Ok, Thiago, so what does he propose instead? Nothing new. That is the beauty of it.
He says the root cause of prompt injection is the same as SQL injection: no separation between code and data. The model reads instructions and content in the same stream and treats both the same. Hello, SQL injection, my old friend... we fixed you decades ago with prepared statements: values are never executed as commands. Full stop.
His move is the same, and it builds on his own ACM Queue piece from February 2025: hide the concrete values from the model. Instead of calling tools one by one, the model emits a structured workflow with symbolic references (@emails_fetched, not the emails). Nothing runs until that plan is verified. And the plan is readable: it prints as a literate explanation you can read before anything executes. That is what I watched on Sunday. Fetch, summarize, send... as a plan, not as three tool calls firing one after the other while I hope for the best.
The verification is three old ideas pointed at agents:
Information flow (taint). Data from
fetch_mailmay not reachsend_email.bodywhen the recipient is outside the allowed domains. A rule from a source to a sink, with a condition.Security automata. Fred Schneider, ACM TISSEC, 2000: a small state machine that walks the plan step by step and has an error state.
no_external_sendis one of those.Pre- and post-conditions checked by a prover. Z3 in the repo, Dafny in the paper.
The analogy he uses is bytecode verification in Java and .NET (Xavier Leroy, Journal of Automated Reasoning, 2003): complexity in production, verification cheap. Same idea as the checksum on your credit card.
Every one of those ideas is older than your youngest engineer. The news is not the maths. The news is where it sits: before execution! On a plan the model cannot smuggle data into.
And the hands-on texture, because I promised you the work and not the pitch: the repo is Nada Amin’s (Harvard), plain Python, verifier core around 1,900 lines. The three complaints in my terminal came from three separate checkers agreeing with each other. No LLM anywhere in the verifier. You can read the whole thing in an evening, which is not something I say about many “AI safety” products developed by vibe coding...
The frame problem is your review backlog
Now the example from the paper that made me put down the tea.
Ask the model to delete foo.txt and bar.txt. Post-condition: after execution, those two files are gone. The model emits delete_file("*.txt"). Correct! Both files are gone. So is everything else. In his words: “LLMs lack common sense and will do exactly as they are asked”, which here means the simplest program that satisfies the post-condition. McCarthy and Hayes gave this a name in 1969: the frame problem. The fix is a frame condition: files that do not match the pattern stay exactly as they were. Add it and the *.txt plan fails to verify.
Honesty rail, right here and not in a footnote: the repo does not implement old() yet, so that exact proof runs on paper today. What ships is a weaker check, roughly “the pattern is not” plus a check that the post-condition is not vacuous. Fine. The shape is what matters.
Because... what is your senior reviewer doing at the third MR of the afternoon? Not checking that the agent did what it was asked. Checking that it did what was meant. Nothing else touched. Nothing else deleted. That is a frame condition and a human one... run by eye, on a green pipeline, many times a day.
We counted the cost of that two weeks ago with He and colleagues’ 802 developers: reviewer load doubled, the share of MRs any human reviewed fell from 89% to 68% and silent approvals doubled. The frame condition did not disappear when the humans got tired. It just stopped being checked.
And last week we found the craft the factory never asked for. Here is one piece of it with a name: writing the frame condition is a decision the spec never contained. “Delete these two” is the spec. “And touch nothing else” is the craft. Nobody wrote it down, so the reviewer supplies it (by hand) at 17:45.
The review queue is where the absence of that sentence shows up.
Who writes the policy? The three-body reading
Here is the three-body reading, and for once it has a repo attached.
The verifier is the capability body. Z3, taint rules, automata. No LLM. It is a thing you adopt or build, not a model feature and no release next month makes it appear in your stack.
The tool contracts are the architecture body. The verifier is useless without tools that carry machine-readable contracts: a ToolSpec with preconditions, taint labels, which parameters are sinks, which domains are allowed. And you usually have docstrings, not contracts. And the frame problem needs a model of the world state your tools can change... the repo’s missing old() is a symptom of exactly that gap, but a miniature version.
The policy owner is the team body. Nothing runs without a person whose name is on allowed_domains, on the taint rules, on the automaton. Governance stops being a committee that samples outputs on a Friday and becomes a team that owns a policy-as-code artifact with its own test suite. The repo has 130 of them. Yours would have your own.
And here is the sequencing trap, Issue 3 all over again:
Buy the verifier first and nothing else? You have nice demo (and that's all)…
Write the policy first and that’s it? Nobody can enforce it…
Add the contracts first without (1) and (2)? Nobody knows what to check against…
They move together or they do not move.
In Issue 2’s terms: a bolt-on guardrail reading outputs is AI-ready, and Meijer’s own critique of guardrails applies to it in full. Verification designed into how work is planned, checked and executed is AI-native.
So where do the humans go? From reviewing every output to writing and owning the policy, and reviewing the residue: the exceptions the verifier cannot decide. Meijer keeps that hybrid himself, static first, runtime for what static cannot see. Fewer signatures. More decision per signature. The reviewers are still the people you keep, now with a job that is possible to do.
This is also the first exercise I run when a team brings a real work item to the lab: before anyone touches the harness, write the policy for one agent workflow in plain words. The tools it may call, one flow it must never make, one thing in the world it must not change. How much of that a team can state at all is the diagnostic... and the gaps land on the architecture line or the team line, almost never on the model :-]
Where it does not reach yet
This sounds too good to be true... and too simple. Yes and it has limits...
The paper is a position piece. No measurement, and the author says the effect of plan-first on how useful the agent stays “has not been formally measured”. The repo is one implementation with 130 tests and a public list of what is not built yet. That is the weight of the evidence and I am not going to inflate it.
It verifies agent tool-call plans. Not the application code an agent writes. Your MR queue of AI-written Java is not what Z3 is proving here. The frame condition your reviewer supplies by hand is the same shape, but nobody has written the post-conditions for your services, and this repo will not write them for you.
The policy is the new attack surface. The paper’s own injection example arrives inside a tool description, not inside an email. Whoever writes allowed_domains can be wrong, lazy, on holiday or used AI to write it (wrongfully). A verifier enforces what you wrote, including the mistakes.
And the static check is not the whole gate. Meijer keeps runtime monitoring for what static analysis cannot see, the way Java still bounds-checks arrays at runtime. So the humans reviewing the residue are not a transition phase. They are the design.
None of that weakens the placement argument. It tells you what the hands-on work is for the next couple of years: contracts on tools, policies with owners, plans instead of chat and a reviewer role redefined around exceptions. Which is the same three-body work the last ten issues kept pointing at. The difference this week is that you can clone it and play with it on a Sunday.
Run it on yourself
Before the next “AI governance” steering committee, and before someone buys a guardrail product because the demo had a red banner in it, three things you can check this week. On your own agents, not on a vendor’s slides.
Write one policy. Pick one agent workflow you already run. Five lines: the tools it may call, one data flow it must never make, one thing in the world it must not change. If you cannot write line three, you have just met the frame problem. Your reviewers have been solving it by hand and now you know what they were doing all afternoon.
Count the contracts. Of the tools your agents can call, how many have a machine-checkable precondition or a declared sink, versus a docstring and good intentions? That ratio is your architecture-body gap. No model release moves it.
Name the owner. Whose name is on the policy? If the answer is a committee, or “security, I think”, the gate is still a person reading a diff... only now nobody knows which person.
Run the three and you know whether your gate is placed where the paper says it should be or where Issue 9 found it: on a tired human, after the fact.
The whole thing, in one line
Stop paying people to find, after the fact, what a policy could have refused before the first tool ran. Then pay them to write the policy.
Coming up
Next week, one floor up. If humans write the policy and machines check the plan, then who owns the policy? What can they decide without asking anyone? And where do they sit in your org: platform, enabling, or stream-aligned team? The operating model behind the verifier. More soon. :-]
Sources
Erik Meijer, “Guardians of the Agents: Formal Verification of AI Workflows”, Communications of the ACM 69(1), January 2026, pp. 46-52, Practice section https://doi.org/10.1145/3777544
Nada Amin (metareflection),
guardians: static verification for AI agent workflows, an implementation of Meijer’s paper, MIT license, GitHub; commit59e52d9of 16 July 2026 was the one run for this issue https://github.com/metareflection/guardiansErik Meijer, “I’ve never seen anything scarier than an LLM with tool calls”, AI Engineer World’s Fair 2026 talk (San Francisco, 29 June to 2 July 2026; AI Engineer YouTube channel, uploaded 13 July 2026).
Fred B. Schneider, “Enforceable Security Policies”, ACM Transactions on Information and System Security 3(1), February 2000, pp. 30-50 https://doi.org/10.1145/353323.353382
John McCarthy, Patrick J. Hayes, “Some Philosophical Problems from the Standpoint of Artificial Intelligence”, Machine Intelligence 4, 1969, pp. 463-502 http://jmc.stanford.edu/articles/mcchay69.html
Edsger W. Dijkstra, “Notes on Structured Programming”, EWD249, 1970 https://www.cs.utexas.edu/~EWD/ewd02xx/EWD249.PDF
Xavier Leroy, “Java Bytecode Verification: Algorithms and Formalizations”, Journal of Automated Reasoning 30, 2003, pp. 235-269 https://doi.org/10.1023/A:1025055424017
Erik Meijer, “From Function Frustrations to Framework Flexibility”, ACM Queue 23(1), February 2025, pp. 19-38 https://doi.org/10.1145/3722544
Hao He, Shyam Agarwal, Yegor Denisov-Blanch, Pavel Azaletskiy, Sanmi Koyejo, Bogdan Vasilescu, “AI Writes Faster Than Humans Can Review: A Longitudinal Study of an Enterprise ‘2×’ Mandate”, arXiv:2607.01904, July 2026 https://arxiv.org/abs/2607.01904
Further reading (not cited in the body, same argument from other angles):
Margaret Mitchell, Avijit Ghosh, Alexandra Sasha Luccioni, Giada Pistilli, “Fully Autonomous AI Agents Should Not be Developed”, arXiv:2502.02649, 2025 https://arxiv.org/abs/2502.02649
Yi Dong, Ronghui Mu, Gaojie Jin, Yi Qi, et al., “Building Guardrails for Large Language Models”, arXiv:2402.01822, 2024 https://arxiv.org/abs/2402.01822