I'm not sure what fire has been put out here. IMO, a more convincing proof for the usefulness of this approach would be that it allows to find whole new classes of exploitable vulnerabilities that can then be corrected ahead. That's how static code analysis tools typically demonstrate their value. Without such proof, the description that they make of a hardware platform is mentally interesting but not clearly useful.