Maybe a dumb thought: is SAT solver good for verifying concurrent system design? (e.g. locks, distributed systems, etc.) Or are systems like TLA+ a must for these cases?
Sadly I don't think it's possible to represent an infinite trace as a SAT problem, so you can't check any liveness properties (will a good thing eventually happen) unless you use something more powerful. Promela/Spin and TLA+/TLC use model checkers, TLA+/TLAPS and B/Rodin use theorem provers, Electrum uses an SMT solver.