[throwalean]

Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-;

Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138