Formal methods notes

Start here

A path that moves from specs → checks → protocol structure.

1. Specs, invariants, and contractsA practical mental model for what specifications are and how they constrain implementations.
2. Model checking primerHow state exploration and properties work, and how to interpret counterexamples.
3. 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.
• MCP, A2A and ACP: The Emerging Protocols Powering Multi-Agent AI SystemsA technical comparison of the Model Context Protocol, Agent-to-Agent protocol, and Agent Communication Protocol, with analysis of their design assumptions, interoperability, and formal properties.
• Formal Verification Goes Mainstream: LLM-Driven Proofs and VericodingHow large language models are lowering the barrier to formal verification by generating proof sketches and specifications, and what 'vericoding' means for engineering practice.
• Integrating Formal Methods with AI Models: Neuro-Symbolic Techniques for Reliable SoftwareHow neuro-symbolic approaches combine neural network capabilities with formal reasoning to produce software systems that are both adaptive and verifiable.

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.