Forge: A Tool and Language for Teaching Formal Methods

Forge is a lightweight formal-methods tool, similar to Alloy 6, built with teaching in mind. Forge provides a progression of sub-languages that gradually build in expressive power to match students' experience and expertise.

Installation and Documentation

Forge is for everyone…

from beginners...

to domain experts...

to domain-specific language authors.

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.

Rust Lifetimes and Borrowing

Thomas Castleman and Ria Rajesh

(class project)

Cryptographic Protocols

Abigail Siegel and Mia Santomauro

(link to paper)

Network Reachability

Tim Nelson and Pamela Zave

(link to lab)

Getting Started

To get started with Forge, follow these instructions.

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, and the first version will be finalized and used in Spring Semester 2025.

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!

Our Papers

To read more about our motivation and design, see our upcoming paper in OOPSLA 2024.

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.

This site is open source. Improve this page.