Formal software specification deserves a place in the introductory computing curriculum. Many courses covering software specification use proof assistants that are powerful, but often have a steep learning curve. A great deal of such classes must be dedicated to the peculiarities of using a proof assistant, rather than the art and science of software specification itself. This talk presents a teaching language designed for students learning how to write formal specifications. The language uses contracts, property-based testing, and symbolic execution to provide a smooth path from informal specifications all the way to statically verified formal specifications. Students come away with techniques and skills relevant to software engineering, and are also prepared for further coursework in formal methods.