Alloy is a formal specification language used to model software systems. It can be used to both check models and find them. Alloy can also output visualizations, making it very useful for communication and domain modeling.
Alloy is a specialty of mine. I am on the Alloy board and currently in charge of writing the online documentation. I also offer consulting services.
- Related Tags
-
- TLA+: Another formal method I specialize in.
- Formal Methods: The general discipline that TLA+ falls under.
- Case Study Highlights
-
- Formally Modeling Database Migrations: Using Alloy to verify that two database schemas have the same properties, and that migrating from one to the other will not corrupt data.
- Proving Games are Winnable with Alloy: Showing that a randomized video game can’t generate impossible levels.