This sounds like a bad idea to me if taken too seriously. Makefiles come from a grammar not a 5th order markov process. The sampled strings from the markov chain are not likely to be representative of the makefiles encountered in practice. I suspect that the makefile language is probably too complex for formal verification so I understand the problem, but I would prefer their other approach where they take large numbers of real world makefiles and compare the output seems a better choice. Just spend the effort and get a larger and more diverse set of test makefiles.