I think it might be an interesting experiment to try to duplicate as much of the functionality of IKOS as possible in vanilla Rust using a no_panic-like [0] technique. My guess is that most of the checks are already done by Rust or can be covered by such a technique, albeit perhaps with more hand-holding than for IKOS. The pointer alignment and comparison checks are the ones I'm least certain about since Rust is relatively lax with those.
I think it might be an interesting experiment to try to duplicate as much of the functionality of IKOS as possible in vanilla Rust using a no_panic-like [0] technique. My guess is that most of the checks are already done by Rust or can be covered by such a technique, albeit perhaps with more hand-holding than for IKOS. The pointer alignment and comparison checks are the ones I'm least certain about since Rust is relatively lax with those.
[0]: https://docs.rs/no-panic/latest/no_panic/