At the moment, x86 verification is possible but requires writing proof scripts in Haskell code. Exposing that infrastructure in a way similar to crucible_llvm_verify would significantly reduce the effort of doing x86 verification. Having #553 done first would be very valuable.
