There's been a lot of work on both of these problems, but right now, proving concurrent algorithms correct, and proving equivalency of those algorithms to executable code, are very much open research problems.