Is it possible to prove thread safety?
Proving that a program is "thread safe" is hard.  It is possible, however, to concretely and formally define the term "data race."   And it is possible to determine whether an execution trace of a specific run of a program does or does not have a data race in time proportional to the size of the trace.  This type of analysis goes back at least to 1988:  Barton P. Miller, Jong-Deok Choi, "A Mechanism for Efficient Debugging of Parallel Programs", Conf. on Prog. Lang. Dsgn. and Impl. (PLDI-1988):135-144.

Given a trace of an execution we first define a happens-before partial-order between events in the trace.  Given two events $a$ and $b$ that occur on the same thread then $a &lt; b$ or $b &lt; a$.  (The events on the same thread form a total order given by the sequential semantics of the programming language.)  Synchronization events (these could be mutex acquires and releases, for example), give an additional inter-thread happens-before partial order.  (If thread $S$ releases a mutex and then thread $T$ acquires that mutex we say that the release happens-before the acquire.)

Then given two data accesses (reads or writes to variables that are not synchronization variables) $a$ and $b$ that are to the same memory location, but by different threads and where either $a$ or $b$ is a write operation we say that there is a data-race between $a$ and $b$ if neither $a &lt; b$ nor $b &lt; a$.

The C++11 standard is a good example.  (The relevant section is 1.10 in the draft specs that are available online.)  C++11 distinguishes between synchronization objects (mutexes, and variables declared with an atomic&lt;&gt; type) and all other data.  The C++11 spec says that the programmer can reason about the data accesses on a trace of a multithreaded program as if it were sequentially consistent if the data accesses are all data-race free.

The Helgrind tool (part of Valgrind) performs this kind of happens-before based data-raced detection as do several commercial tools (e.g., Intel Inspector XE.)  The algorithms in modern tools are based on keeping vector clocks associated with every thread and synchronization object.  I think this technique of using vector clocks for data-race detection was pioneered by Michiel Ronsse; Koen De Bosschere: "RecPlay: a fully integrated practical record/replay system", ACM Trans. Comput. Syst. 17(2):133-152, 1999.