Amalgam is an extension to the Alloy Analyzer that provides explanations for the instances it finds. Concretely, if an element of an instance cannot be consistently removed, Amalgam will say so and provide a justification in the form of a proof.


Download the Amalgam JAR archive here. If you are running Linux and have Java 8 or later installed, you should be able to run the JAR archive directly. We have tested this on Ubuntu 16.04, Mac OSX 10.11.6, and Windows 7.

You can run the JAR file by typing: "java -jar amalgam.jar" at your terminal.

Example Specifications

The Alloy specifications used in our FSE 2017 paper can be found here.

Using Amalgam

Amalgam extends the Alloy Analyzer with new explanatory features. These features are largely accessed via the evaluator. (To reach the evaluator, run a satisfiable predicate, click on "Instance" to view the instance, and then press the "Evaluator" button in the top bar.)

Provenance Commands

Amalgam adds several new commands to the evaluator:

  1. @ln+ : lists the locally-necessary positive literals;
  2. @ln- : lists the locally-necessary negative literals;
  3. @why : generates provenance(s) for a positive literal;
  4. @whynot : generates provenance(s) for a negative literal;
  5. @prov # : displays the #th provenance for the last @why or @whynot command. The evaluator will print only debugging information; the structured provenance tree and highlighting will appear in the model-editing window.


Amalgam supports most of the Alloy language. It does not currently support higher-order quantification (that cannot be Skolemized) or arithmetic.
If Amalgam reports that a literal is locally necessary but produces no provenances, then the necessity is likely a result of the analysis bounds.

Provenance Detail

Amalgam adds an important new setting to Alloy's options menu: Provenance Detail.

The default of "1" provides less information than "2"; to see more information about each alpha formula and derivation, change this setting to "2". Different users may prefer different settings.

New Instance-Viewing Options

Buttons in the instance-viewing screen allow users (e.g.) minimize and maximize instances. The "next" button functionality remains unchanged.