Summary
Kleppmann (author of Designing Data-Intensive Applications) predicts that AI will make formal verification mainstream by handling the tedious parts — writing proof obligations, generating invariants, translating between notations — while humans focus on what the system should do. He draws a parallel to how compilers made assembly language accessible: the hard part wasn’t the machine code, it was the human effort to produce it.
What it means for our work
This is independent convergence on our core thesis. Kleppmann arrives at “AI makes formal methods economically free” from the verification side; we arrived at it from the specification side. The overlap validates the direction. His framing of AI as a “compiler for formal methods” is particularly useful — it captures why Z Spec wraps fuzz and ProB rather than replacing them. The formal tools do the hard mathematical work; AI handles the notation gap between human intent and formal expression.