This talk will give an introduction to Alloy, a formal specification tool for bounded analysis. Originally Alloy was developed as a lightweight approach to formally verify software, and indeed, many case studies show its strength in finding non-trivial bugs. Today we will start small by using Alloy to solve a simple puzzle. Once we are familiar with the language and the analyser, we will focus on another application, which is spotting errors in formal theories. This is based on recent work, where we automatically reproduced known counterexamples to partial-order reduction (POR) theories. It turns out, at least in the case of POR, that simply formalizing the definitions and theorems in Alloy is enough to find an example that contradicts the soundness of the theory. This contrasts the pen and paper approach, where a deep understanding of the theory (and the proofs) is required to find such an example. We will also touch on some of the fundamental limitations of Alloy.