This paper presents the design of 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 progression of languages that improve the learning experience by only gradually increasing in expressive power. Forge supports custom visualization of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of testing features to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.

@article{paperbot2532,
  title = {Forge: A Tool and Language for Teaching Formal Methods},
  author = {Tim Nelson and Ben Greenman and Siddhartha Prasad and Tristan Dyer and Ethan Bove and Qianfan Chen and Charles Cutting and Thomas Del Vecchio and Sidney LeVine and Julianne Rudner and Ben Ryjikov and Alexander Varga and Andrew Wagner and Luke West and Shriram Krishnamurthi},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA1},
  year = {2024},
  doi = {10.1145/3649833}
}