Forge: A Tool and Language for Teaching Formal Methods
Installation and Documentation
Forge is for everyone…
Forge has…
Modern Editor Integration
Edit Forge in your favorite text editor; we have added support in both Visual Studio Code and DrRacket.
Domain-Specific Visualization Support
Forge uses the Sterling visualizer to enable custom visualizations by both students and instructors.
Getting Started
We suggest that users install via Git, rather than using Racket’s package system. Our Github contains release tags that are useful for those who wish to use older versions of the software. Forge now uses semantic versioning; major version changes introduce breaking changes.
| Version | Textbook | VSCode Extension |
|---|---|---|
| 5.0.0 (docs) | Spring 2025 | forge-language-server |
| 4.2.1 (docs) | Spring 2026 | forge-fm |
Materials and Github
Forge was originally created for CSCI 1710, “Logic for Systems” at Brown University. The notes and materials (except for recordings, which we cannot release) are public and free to use. A textbook draft is also available.
Forge is open source and hosted on Github.
Example Models
Beyond the notes and documention, you can find many examples of Forge models in the forge/examples folder of the repository. See the README for an itemized list. We are adding to this collection regularly! A selection of these that we use for teaching includes:
Sample Systems- and Datastructure-Oriented Models
- Raft leader election
- Binary Decision Diagrams
- Prim’s algorithm
- Destination-based MAC-layer network forwarding
- Basic crypto-protocol domain model
Sample Mathematically-Oriented Models
Our Papers
To read more about our motivation and design, see our OOPSLA 2024 paper.
Contact
Got questions? Reach out to Tim_Nelson@brown.edu.
Thanks
We are grateful for support from the U.S. National Science Foundation (award #2208731) and Brown University.
