A tool for formal software modeling. Similar to Alloy, but designed to be teachable.