I don't think that fuzzing and formal methods are opposed. First, formal verification is only as good as the specifications and the extraction / equivalence pro

I don't think that fuzzing and formal methods are opposed. First, formal verification is only as good as the specifications and the extraction / equivalence proofs. Likewise, fuzzing by its very nature never reaches full coverage of a code base. However, they are complementary. Adding fuzzing to a formally verified system is a great way to find gaps in the specification or the proofs. Humans write specs and proofs. Humans are fallible. Fuzzing is a great way to explore the health of the specification and implementation. Likewise, building toward a formal specification is a great way to convert errors found by the fuzzer into a class of error, and then build up a means by which that class of error can be eliminated entirely from the code base. The WPA2 protocol -- not its implementation -- was partially verified using formal methods. Unfortunately, there was a flaw in this specification, which led to a poorly crafted state machine. This led to the KRACK attacks. Complementing these specifications with fuzzing could have found these attacks sooner. Researchers have since refined formal modeling of WPA2 to prove that the patches to the KRACK attacks prevent them. https://www.usenix.org/conference/usenixsecurity20/presentation/cremers https://www.usenix.org/conference/usenixsecurity20/presentat... These tools are defense in depth for design. None of them are complete on their own.