Alloy is a software tool that alloys for the specification of models and the verification of assertions about those models with the use of SAT solvers. For my capstone, the models were abstract algebraic structures like groups, which are sets of elements with an addition operation satisfying some basic constraints. The main assertion on these models was the first isomorphism theorem. In short, the project was to ‘prove’ the first isomorphism theorem for groups with Alloy. Since this involved verifying claims for all possible homomorphisms between groups, the more advanced tool Alloy* was used, which allows higher-order quantification. We were successful in verifying the first isomorphism theorem for small groups with Alloy*.

more here: https://cs.brown.edu/research/pubs/theses/capstones/2017/varga.alexander.pdf