I think the description in the kani::mem module is wrong:

A null pointer is never valid, not even for accesses of size zero. […] ZST access is not OK for any pointer. See: rust-lang/unsafe-code-guidelines#472

According to the link, and according to the documentation of Rust's std::ptr module, all pointers are valid for ZST accesses. Kani itself seems to treat ZST pointers correctly:

#[kani::proof]
fn check_zst_pointer() {
    let ptr_1 = 0 as *mut ();  // null pointer
    unsafe {
        ptr_1.read();
        ptr_1.write(());
    }

    let ptr_2 = 5000 as *mut ();  // non-null but doesn't point to valid allocation
    unsafe {
        ptr_2.read();
        ptr_2.write(());
    }
}

This harness is successfully verified by Kani 0.62.0.