Modern programming platforms, such as Microsoft’s .NET, provide libraries of efficient concurrent data structures, which are used in a wide range of applications. In this talk, I will discuss some of the challenges in implementing such concurrent data structures, what correctness of these libraries means, how one can formally prove that a given library is correct, and the extent to which these proofs can be carried out automatically.