Once we land support for @NullMarked, it seems the AnnotatedPackages option would no longer be absolutely necessary. If we end up adding a flag for "JSpecify mode", we could say that at least one of the JSpecify or AnnotatedPackages options should be given (and giving both would of course be supported). We could instead just make AnnotatedPackages optional, but I'm concerned that could lead to confusion for users who are also not using @NullMarked.