Who checks the agent's code?

Verify the intent, not the lines

Microsoft Research introduced PDD Kit, a tool designed to formally verify AI-generated full-stack web applications. The premise is that AI agents generate code at a scale that is difficult for humans to review line by line, so the review has to move up a level. PDD Kit converts developer intent into a Verus specification, proves that AI-generated code meets specifications for every input, and uses testing for scenarios where formal proofs are not practical. Developers review intent rather than every line of code. m:…4529

The idea matters because it reframes what verification means for agent-written software. Traditional code review assumes a human can read the code. When an agent writes thousands of lines, that assumption fails, and the choice is between trusting the agent or checking something else. PDD Kit's answer is to check the specification: if the code provably satisfies the intent for every input, the individual lines matter less. It is a bet that formal methods, long considered too expensive for everyday software, become economical exactly when the code is cheap and the review is the bottleneck. m:…4529

Long horizons break the agents

The Multi-step SWE preprint tests the assumption from the other side, and the results are sobering. Most existing coding benchmarks evaluate agents on single-turn tasks, failing to capture the iterative, long-horizon nature of real-world software development. The new benchmark has 69 complex engineering tasks that require agents to build upon their own previous outputs across 5 to 15 dependent steps. Current frontier models achieve a maximum solve rate of 18.5%, and 38 out of 69 tasks are not solved by any of the nine tested frontier models. m:…2459

The mechanism is compounding error. Multi-step SWE tasks require agents to build upon their own previous code, causing early design decisions and errors to propagate across dependent steps. A wrong choice in step two becomes the foundation for step seven. This is the same failure mode that shows up in production agent deployments: the agent does not fail loudly on one task, it builds a tower on a crooked foundation. The benchmark gives that failure a number, and the number is low. m:…2459

Tests that run and lie

The third preprint, on mock objects and stubs, finds a subtler failure. MockBench, a dataset of 165 real-world Java and Python tasks, shows that coding agents improve mock artifact executability compared with base LLMs — the generated test code runs — but executability gains do not consistently translate to higher behaviour fidelity or better interaction-fault detection. Ten distinct error types exist in LLM and agent-generated mock artifacts that can conceal behavioural deviations. The mocks run. They just do not simulate the dependency faithfully. m:…2465

That is a dangerous combination in a CI pipeline: green tests that do not test what they claim to test. The authors' implication is that developers should prioritise behavioural validation over simple executability when integrating agentic testing tools. A test suite full of unfaithful mocks is worse than a smaller suite of honest ones, because it converts real risk into false confidence. m:…2465

Teaching agents to write maintainable code

BoundaryML's post offers a more optimistic note, and a practical one. The company observed that AI agents produced lower-quality BAML code compared with their output in TypeScript or Rust, and responded by implementing new coding guidelines and a baml codequality tool. It evaluated agent performance on four program skeletons — a POSIX extended regex engine, chess move generation, a Conduit blogging API and GTFS transit feed lookups — and found each treatment level, from no skill through new skill plus codequality, improved the cognitive complexity of the final outcome. The team reports the new skill and codequality tool resulted in code that is anecdotally better and closer to hand-written code. m:…7824

The codequality tool uses cognitive complexity, cyclomatic complexity, NPath, nesting and exit counts as metrics. BoundaryML considers the core BAML language nearly complete after over a year of design work. The lesson is transferable: agents write better code when the language and the tooling tell them what good looks like, and when quality is measured rather than assumed. Guidelines plus a checker beat a prompt alone. m:…7824

The new bottleneck

Taken together, the four pieces describe a shift in where coding-agent value is decided. Writing code is no longer the scarce resource; checking it is. PDD Kit checks it with proofs. Multi-step SWE measures how badly it fails over long horizons. MockBench shows the tests themselves can be unfaithful. BoundaryML shows that measured quality feedback improves the output. The teams that win the next phase of coding agents will not be the ones with the fastest generation, but the ones with the best verification. m:…4529 m:…2459 m:…2465 m:…7824

For engineering leaders, the practical question is what verification layer to buy or build first: formal specs for the highest-risk paths, long-horizon benchmarks for agent selection, behavioural validation for generated tests, or quality metrics for generated code. The evidence this week says all four matter, and that none of them is yet standard practice. The gap between what agents can write and what teams can trust is now the product opportunity. m:…4529 m:…2459 m:…2465 m:…7824