One danger I can see coming up is that if someone writes incorrect code it could end up propagating throughout other codebases. I guess this is still an issue without automatic tools, but I feel like this might make it easier…
(Thinking specifically of the "binary search in the Java API was broken for X decades" one with the integer overflow.)