Hardware Trojans are malicious circuit modifications and are a rising threat to the integrated circuit supply chain. There are a number of trojans directed specifically at microprocessor designs. This paper examines the threat of invalid opcodes being used as trigger mechanism for trojans in microprocessors. We demonstrate the effect of such trojans and propose an automated formal verification methodology to detect such trojans. The methodology was tested on processor models based on MIPS and RISC-V architecture. Processor benchmark circuits with as many as 400,000 gates were verified using our approach.