Hardware Trojans that degrade performance, change functionality, leak information, or halt service, have been problematic in synchronous circuits. Asynchronous circuits are gaining popularity due to their lower power consumption, and better immunity against PVT (process, voltage, temperature) variations. In this paper, we show some designs to realize hardware Trojans in NULL Convention Logic (NCL), which is a Quasi-Delay Insensitive (QDI) asynchronous digital circuit paradigm. We also present a formal verification methodology to detect such Trojans, and validate our technique on an RSA decryption circuit.