Hi! Is there any work/experiments underway to prove formal properties, via eg. k-induction/PDR? From what I've seen so far, the API can only describe safety properties (please correct if I'm wrong), so it seems like at least implementing k-induction isn't that far away from what's currently there for BMC.

Thanks!