Yes but the number of nodes is n, and an "interaction" among m nodes might not be decomposable to a chain of pairwise interactions, which raises the ceiling back to exponetial (actually factorial, which is worse).

What corresponds to interactions that aren't decomposable as pairwise interactions? Race conditions? Resource utilization? Real bugs (and the nastier ones), but probably a minority. So factorial with a relatively small constant in front of it.

But obviously the real answer is to write a program that will correctly verify all other programs.