You are correct --- PCC (AFAIK) has not come about in the sense of carrying along a proof object that a formal verifier can validate is both correct and corresponds to the code payload.
As the other commenter pointed out, the SLAM tools are part of the Windows Device Driver Development Kit. The last time I talked to the kit's dev manager (~2003), they were talking about making it mandatory that you pass the formal verification in order to have your driver signed by Microsoft. Since those signatures are then verified at driver installation time, that feels very close to it!
I have to confess I'm only familiar with the publications on Native Client and not the actual product. From what I'd read, I understood that the verifier did some basic static analysis to prove that all possible executions did not validate some properties. In that case, no proof object is required, as the source code itself is the proof object. Assuming, of course, that they're actually doing the stuff talked about in the papers and in practice don't just "grep for dangerous instructions."
As the other commenter pointed out, the SLAM tools are part of the Windows Device Driver Development Kit. The last time I talked to the kit's dev manager (~2003), they were talking about making it mandatory that you pass the formal verification in order to have your driver signed by Microsoft. Since those signatures are then verified at driver installation time, that feels very close to it!
I have to confess I'm only familiar with the publications on Native Client and not the actual product. From what I'd read, I understood that the verifier did some basic static analysis to prove that all possible executions did not validate some properties. In that case, no proof object is required, as the source code itself is the proof object. Assuming, of course, that they're actually doing the stuff talked about in the papers and in practice don't just "grep for dangerous instructions."