Start here
A path that moves from specs → checks → protocol structure.
- Specs, invariants, and contractsA practical mental model for what specifications are and how they constrain implementations.
- Model checking primerHow state exploration and properties work, and how to interpret counterexamples.
- Session types and protocolsStructured communication as a lightweight correctness tool for concurrent systems.
All notes in this topic
- Specs, invariants, and contractsHow to write constraints you can review, test, and monitor—not just “requirements” prose.
- Model checking primerStates, transitions, safety vs liveness, and why abstraction is a first-class design decision.
- Session types and protocolsProtocols as types: allowed messages, orderings, and branches that prevent whole classes of bugs.
- Behavioural equivalence in plain EnglishWhat it means for two systems to “behave the same” and why the chosen observations matter.
Common pitfalls
- Confusing specification with implementationA good spec constrains behaviour without baking in accidental design choices.
- Writing properties that can’t failVacuous truth is common: the property holds because the model forbids the interesting scenario.
- Over-indexing on notationSymbols are not the point; clear assumptions and checkable constraints are.
- Ignoring the environmentMost failures happen at boundaries; formalising assumptions makes those failures legible.
Related topics
- Performance notesSpecifications and invariants often translate into concrete latency budgets and measurable SLOs.
- Distributed systems notesProtocols, time, and failure semantics are the core interface of distributed reliability.