Machine learning-based network intrusion detection methods often rely on statistical summaries of traffic, causing a disconnect between the traffic space and the feature space that is difficult to bridge [13]. Realistic adversarial attacks are hard to generate because natural well-formedness constraints at the traffic level aren’t respected at the feature level with usual adversarial attack generation methods. We use a novel attack generation method combining two tools: (1) a bespoke synthetic traffic generation suite, PackGen, and (2) a formal verification tool for neural networks, Vehicle [7]. PackGen produces aggregated Markov chain representations of network traffic which allows us to reconstruct valid packet sequences that are modified by realistic perturbations on an input specification. Vehicle’s formal specification language lets us represent granular threat models such as adversaries who can only manipulate packet timings. Unlike other methods, Vehicle’s formal verification is guaranteed to find counterexamples if they exist, which correspond with evasive adversarial examples. We feed these feature-level counterexamples into modified PackGen representations to generate PCAP files containing reconstructed, evasive network flows, generating adversarial examples that cross the gap between the traffic and feature spaces. We evaluate PackGen by replicating DoS traffic using a variety of timing distributions, before testing our full pipeline by producing evasive counterexamples, outperforming projected gradient descent.