- Clark Barrett argued that once AI writes code easily and, he hopes, proves it soon, the hard part left is writing the specification.
- He conceded a gap remains between an AI-written specification and what the developer actually intends, and called closing it an open research area.
Clark Barrett, a Stanford professor who co-directs the Stanford Center for AI Safety, made a simple argument on the Y Combinator show's YC Paper Club. AI already writes code well, and he hopes proving code correct will soon be easy too. If so, the hard part left is the specification: a precise statement of what the code must do.
What was said
Barrett described a demo tool from his lab. A user types in English what they want built. The tool drafts a structured specification, and a person approves it. The tool then writes Rust code and checks it against that specification.
He said his team used an automated agent on a 30,000-line Rust cryptography library. The job took experts months by hand. The agent finished it in 11 hours, fully automatically.
Asked how this works on real company code that has no specification, he answered: "the thing that's left that's hard is the specification." He said some specifications are easy and universal. A rule that code must be memory safe can be written once for everyone. A bank might want a rule of no loss of funds: after any run of transactions, the total money stays the same. He added that AI agents are quite good at proposing specifications, often suggesting requirements he then agrees he wants.
Why it matters
Our reading: if proof gets cheap, the weak point moves upstream to whoever states and approves the requirements. For engineering leaders, that is judging work rather than making it. It means spotting the missing edge case and asking whether a written rule really captures the business need.
Buyers can ask a sharper question of any vendor that says its code is verified: who wrote the specification, and who checked that it matched what the customer wanted? Teams that train people mainly to write code may need to train them to state intent just as carefully.
The other side
Barrett conceded the central weakness. An audience member asked how anyone knows an AI-written specification matches the developer's intent. Barrett replied, "there is a gap there," and called closing it an interesting research area. He argued that even without closing it, code that an agent proves against its own specifications is likely better than code without them.
His timing was hedged too. He said he hoped verification would be easy "in the next couple of years," so it is not yet. The 11-hour result is also his team's own account of its work.
Fellow guest Mykel Kochenderfer was more cautious. He said there is no single silver bullet and formal methods probably won't take you the whole way.
Written by the WebPulse Newsroom with AI assistance, and checked by our editorial review: every quotation was verified against the recording's transcript. How we use AI.
The conversation this talking point comes from
- Y Combinator: AI Safety Fact vs. Fiction | YC Paper Club (2026-10-17)
