Are there any research papers on formal treatment of RAII and/or safe deallocations in C++?
Take a look at "A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management" (page, different PDF version), which has apparently been submitted to POPL 2012; but AFAIK has not yet been peer reviewed.
There is a section specifically on RAII, although it may not prove what you want:
We cannot prove a general result guaranteeing the proper encapsulation of resources in classes: this is a matter of program verification. We can, however, prove that in a terminating program every construction of a subobject is correctly matched by a destruction.
Disclaimer: I've only briefly skimmed the paper, and I know almost nothing about formal language semantics.