Alloy* is a fully automatic higher-order solver over finite relational domains. Alloy* retains the language of Alloy (predicate logic + relational algebra); it implements CEGIS on top of Kodkod to permit higher-order quantification. Alloy* imposes no restrictions on where higher-order quantifiers may be found or how deeply they may be nested.
More documentation can be found at: https://aleksandarmilicevic.github.io/hola/
Please contact Aleksandar Milicevic aleks@csail.mit.edu for instructions.