When testing a concurrent program, you never know if it really works or if you got lucky. As the famous Dijkstra quote says: "Program testing can be used to show the presence of bugs, but never to show their absence!".

Full model checking or formal correctness proofs remain largely intractable: too expensive, too slow to develop (even with AI assistance), and too hard to maintain over time. However, not all hope is lost: a growing body of tools is available to help you gain more confidence with your concurrent programs.

These tools work by instrumenting the bytecode and executing a series of thread interleavings deterministically. It's not a correctness proof, but it might boost your confidence just enough to ship the code.

In the talk, I'd like to present two such tools: Lincheck and Fray, compare their functionalities, demonstrate how they work, identify the kinds of problems they might detect, discuss their applications, and highlight the issues they have already helped uncover.