Proving a compiler to be secure is costly, and even testing its security often requires domain knowledge about potential attacks. In this work, we present a tool to synthesize examples of compiler insecurity from just specifications of the languages and the compiler between them. The tool also provides evidence of how severe discovered vulnerabilities may be by synthesizing gadgets that represent composable exploitation APIs within implementations.