.md File is not a specification: Using formal analysis to find requirements gaps

A small salon booking example illustrates the main point: plain .md requirements written in EARS (R1: let stylists set schedules; R2: customers can book; R3: appointments must be within schedules) hide important behavioral details and leave invariants untestable. Using dynamic logic to express actions with preconditions and postconditions, a compact formal model was encoded in FizzBee with actions like Init, SetSchedule and BookAppointment and an invariant (BookingsInSchedule). Running the model checker produced a concrete counterexample - an appointment booked while the stylist was not scheduled - revealing that R2 needed a precondition and an explicit rejection case. Refining R2 into an enablement rule and a blocking/rejection rule turned the informal requirements into testable behavior.

The write-up argues that executable specifications catch omitted behaviors early, and shows how refinement and bisimulation criteria prevent trivially compliant implementations (e.g., rejecting everything). It outlines practical tooling: FizzBee’s model checker, model-based testing libraries, and integrations for AI coding assistants to generate, run, and refine specs. The demonstrated benefits are concrete: uncover requirement gaps, check consistency, describe behavior over time, let stakeholders explore traces, and use the same spec as a test oracle. The recommendation is to keep human-readable requirements but make them machine-checkable via executable formal specifications to drive specification-driven development.