One big reason is because it is highly likely they not only don't have one, but one couldn't even exist in any meaningful way, as their primary implementation is some turing-complete monstrosity where the only "formal" spec is their code as there is nothing "formal" about it: the cost of not using parser generators is essentially the same as the cost of using dynamic typing... it not only means you probably have inconsistency bugs all over the place, even if it made it feel easier to code without having to actually prove your program was correct all the time, but it further tends to lead you to relying on the dynamic typing features in places that make the resulting program not something that fits any known formal type model anymore even if it works perfectly.