 The Alloy Analyzer was specifically developed to support so-called "lightweight formal methods".As such, it is intended to provide fully automated analysis, in contrast to the interactive theorem proving techniques commonly used with specification languages similar to Alloy.Development of the Analyzer was originally inspired by the automated analysis provided by model checkers.