Model checking

Stream: Lean for Scientists and Engineers 2024

[Alessandro Pinto]

Hello,
is there an effort to interface Lean4 to a model checker? Something similar to lean-smt, but for discharging proofs of temporal properties to an external model checker.
Thanks

[Tyler Josephson ⚛️]

I’m not sure! You could try asking in https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification

[Alessandro Pinto]

Thanks!