Hacker News Reader

What is the state of the art in building high assurance lock free components? Are there type systems or proof assistants that are workable?

View on HN

SPIN is a nice tool for modeling them. You can extract code from a coq model. You can go into the world of dynamic instrumentation to try to verify invariants in implementations.

Reply on news.ycombinator.com