The transaction ordering problem of the original PCI 2.1 standard bus specification violates the desired correctness property of maintaining the so called ‘Producer/Consumer’ relationship between writers and readers. In [3], a correction to this ordering problem was proposed and informally proved (called the “HP solution” here). In this paper, we present a formalization of the PCI 2.1 protocol in PVS. We formalize the fact that with Local Master ID added to the protocol no completion stealing is possible and the Producer/Consumer property is provided even in the presence of multiple readers. The state of our proofs leading to this result, as well as some of the much needed enhancements to theorem-proving frameworks that will greatly facilitate similar proofs, are also elaborated.