Writing threat detection signatures directly from informal reports is error-prone and may omit critical details. Attack trees provide a rigorous model for specifying complex threats, but bridging the gap between attack trees and implementable detection logic requires a formal methodology. In this paper, we present a correct-by-construction approach for generating threat detections from attack trees. We formalize the trace semantics of attack trees, defining precisely the sets of event traces corresponding to successful attacks. We also provide a formal semantics for the Generic Threat Detection Language (GTDL), a simplified fragment of a production detection language used in a commercial security product (Bitdefender ( https://www.bitdefender.com )), focusing on detection logic essential for practical deployment. We then give a structural translation from attack trees to GTDL, encoding sequencing, choice, and parallelism directly at the level of event traces. We prove that this translation is sound: every event trace detected by the GTDL signature corresponds to a valid attack trace permitted by the original attack tree semantics, and vice versa. By aligning high-level threat models with executable detection logic in operational security products, our results enable the automated synthesis of provably correct and robust detection signatures for real-world environments.