thirdsummerofai.org
The Third
Summer of AI
Neural meets symbolic.
Language meets logic.
Generation meets verification.
Formal requirements for complex software systems are expensive to write, hard to verify, and surprisingly easy to get wrong. As we move into the third AI summer , I’m documenting my attempt to fix that — combining neural systems like Claude with symbolic reasoning tools like TLA+, Z3, and Alloy — and building a public resource for anyone trying to understand how these two approaches converge.