Prediction: AI Will Make Formal Verification Go Mainstream ↗
Kleppmann argues AI removes the human bottleneck from formal verification — the same thesis driving our work, arrived at independently.
Our notes →Readings
Papers, posts, and talks that shape our thinking — with notes on what they mean for our work.
LLMs Bring a New Nature of Abstraction ↗
Fowler argues LLMs create a new kind of abstraction — probabilistic rather than deterministic — and explores what that means for how we build software.
Our notes →Towards Formal Verification of LLM-Generated Code from Natural Language Prompts ↗
Proposes using formal verification to check LLM-generated code against natural language intent — closing the gap between what you asked for and what you got.
Our notes →Augmented Coding: Beyond the Vibes ↗
Beck distinguishes 'augmented coding' from 'vibe coding' — AI that amplifies engineering discipline rather than replacing it.
Our notes →Formal Requirements Engineering and Large Language Models: A Two-Way Roadmap ↗
A roadmap for how LLMs and formal requirements engineering can strengthen each other — LLMs make formal specs accessible, formal specs make LLM output verifiable.
Our notes →Use Cases are Essential ↗
Jacobson and Cockburn argue that use cases remain the most effective way to capture requirements — actors, goals, scenarios, and what can go wrong.
Our notes →Assigning AI: Seven Approaches for Students with Prompts ↗
Defines seven pedagogical roles for AI — Mentor, Tutor, Coach, Teammate, Student, Simulator, Tool — each with distinct benefits and risks. The framework behind our Persona concept.
Our notes →Working Backwards: Insights, Stories, and Secrets from Inside Amazon ↗
The definitive account of Amazon's Working Backwards process — write the press release before building the product. The methodology PR/FAQ implements.
Our notes →The Birth of Refactoring: A Retrospective on the Nature of High-Impact Software Engineering Research ↗
Opdyke and Griswold reflect on how refactoring went from two PhD theses to a universal practice — and what was lost when the formal definition was dropped.
Our notes →How Amazon Web Services Uses Formal Methods ↗
AWS engineers used TLA+ to find subtle bugs in DynamoDB, S3, and other core services — proving formal methods work at industry scale.
Our notes →Formal Methods: Practice and Experience ↗
A survey of 62 industrial projects using formal methods — evidence that formal specification works in practice, not just in theory.
Our notes →The Cost of Interrupted Work: More Speed and Stress ↗
Interruptions don't just cost time — they cost cognitive quality. Workers compensate by working faster but produce more errors and experience more stress.
Our notes →A Refactoring Tool for Smalltalk ↗
The first automated refactoring tool — built at UIUC by Ralph Johnson's group, proving that Opdyke's formal definitions could be mechanized.
Our notes →Refactoring Object-Oriented Frameworks ↗
Defines refactoring as behavior-preserving program transformation with formally specified preconditions — the intellectual foundation for Refactory.
Our notes →The Z Notation: A Reference Manual ↗
The definitive reference for Z — the formal specification notation grounded in set theory and first-order predicate logic that Z Spec puts into practice.
Our notes →