For the bug in the commit linked up? I don't see how: the issue is a logic error causing a data race which depends on a whole bunch of factors a higher level la

For the bug in the commit linked up? I don't see how: the issue is a logic error causing a data race which depends on a whole bunch of factors a higher level language can't model directly. The next step up for that is formal verification which is staggeringly time consuming (read: expensive) and hard to understand in the first place.