At Facebook we have been working on automated reasoning about concurrency in our work with the Infer static analyzer. RacerD, our new open source race detector, searches for data races — unsynchronized memory accesses, where one is a write — in Java programs, and it does this without running the program it is analyzing. RacerD employs symbolic reasoning to cover many paths through an app, quickly.

This sounds extremely interesting...

good trick -- exploit eventual consistency and a lack of distributed transactions by launching race-condition-based attacks

Race conditions, and errors at startup, seem to be particularly problematic