- Author
- Ivan Gavran
- Published
- 15 August 2026
- Kind
- Personal blog essay revisiting a 1979 paper
- Original
- ivan-gavran.github.io/0-social-processes-paper
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work
What it is
Ivan Gavran is a formal methods practitioner. The essay notes growing excitement about verification, driven by AI coding. It then tests the 1979 paper's arguments one by one.
What it says
- Gavran says AI agents leave gaps in understanding. They also make verification faster, so interest is rising.
- Gavran says specs sit closer to informal requirements than code does. Mistakes are therefore easier to spot.
- Gavran says only a human can change the specification. A human decides what correct means.
- Gavran says LLM-powered tools are closing the gap on automatic verification. Human effort still matters.
- Gavran calls the claim that automatic verifiers harm understanding a weak argument. It assumes the worst case.
- Gavran agrees that reliability is more than verification. The paper wrongly dismisses how useful different parts of formal methods are.
What evidence it gives
The essay is argument, paragraph by paragraph. It cites one experience report, Igor Konnov proving the Ben-Or protocol in Lean. It cites a Google Trends spike and a talk by Will Wilson.
Interests and limits
Gavran is a formal methods practitioner and says so. The essay calls itself a fun exercise rather than a completely serious one. Nothing was measured or tested. It also notes that interest in verification may not become a regular part of engineering.