Salt chose Z3 because it felt right for a compiler. The 100ms timeout means it's not sound, but it's useful. Lean could be the right choice when a proof is a hard requirement?