I wasn't thinking primariy of pure vs. impure, but of user vs. computer. You generally cannot formally verify users, and they often want the dumbest, most illogical things. Like asking that null vs. singular vs. plural cases all be separated out, or that you should filter porn out of their results (what's porn to a computer? hell, what's porn to the supreme court?), or that you should render things brokenly if there's no doctype but do it correctly if there is.

One of my cubemates at Google is a project manager who used to work at Microsoft. She said that one of the biggest differences between the engineering cultures of the two companies was that engineers at Google are encouraged to make "product" decisions themselves, while Microsoft engineers basically stuck to code. If a spec was unclear on some point at Microsoft - say, what color of blue to use for the border on some dialog box - the engineer would throw it back over the wall to the PMs and wouldn't work on it until they got further clarification. While at Google, the answer was likely to be "Use your judgment, and we'll fix it if it's terribly bad." That implies some amount of knowledge about what users want, and you generally can't prove what users want.

Assuming that the compiler, any libraries you use, the hardware, and the interfaces to that hardware all behave correctly, yes, you can formally verify code.