This appears to be a corollary: "Beware of bugs in the above code; I have only tried it, not proved it correct."