Markdown 文件不是规格说明：用形式化分析发现需求缺口

文章以美发沙龙预约系统为例，演示用 Dynamic Logic 和 FizzBee 将 EARS 需求转成可执行形式化规格，并通过模型检查发现预约后发型师修改排班、已有预约被覆盖等需求缺口。文中还说明角色建模、可交互规格、基于模型的测试，以及 FizzBee 对 Go、Java、Rust、TypeScript 和 Claude Code、Cursor、Gemini CLI 的支持。