To me fuzzing still helps finding problems the Formal method of choice doesn't cover. Typically my favorite example is stack use or runtime-duration. I can writ

To me fuzzing still helps finding problems the Formal method of choice doesn't cover. Typically my favorite example is stack use or runtime-duration. I can write a parser guaranteed to have no runtime error (bounds, over/underflow, divide by zero) and still make it crash because of stack or heap exhaustion. Or I can find tortuous cases of denial if service. Because the tool doesn't handle (at the moment) stack or heap size, or execution duration. Fuzzing still helps a lot in those cases! Especially if you focus on those kinds of problems.