This paper presents the design of \emph{Forge}, a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry.

Forge offers a \emph{progression of languages} that improve the learning experience by only gradually increasing in expressive power. Forge supports \emph{custom visualization} of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of \emph{testing features} to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and evaluate the effectiveness of each of them.