What you guys think of Theorem Provers like Z3?

General
1

Ever used any SMT like Z3, F*, Isabelle, Lean, …?
What’s your experience with them?

2

For those like me :wink: who have no idea, those seem to be related to formal verification : Z3 Theorem Prover - Wikipedia

2 Likes
3

I know SeL4 uses theorem provers but I don’t know about the rest of the kernels.

1 Like