There's nothing to stop you from writing out a grammar in some form that is intelligible to a verification tool and then implementing the grammar by hand. I almost always write out the grammar anyway because that's the design—without it I'm flying blind. The cost of the generator isn't writing out the grammar, it's in using the runtime code it generates, which is optional even if you want to use it for verification.