Here is a preprint of fun paper that I've been working on which investigates the utilization of formal descriptions of instruction semantics to perform symbolic binary-level program analysis: https://doi.org/10.48550/arXiv.2404.04132
It includes a prototype implementation in Haskell which performs symbolic execution of RISC-V binary code without requiring the transformation to an intermediate representation (like LLVM IR).
This paper also includes an empirical comparison with prior work which I attempted to design in a reproducible way by using #Guix for the evaluation artifacts: https://doi.org/10.5281/zenodo.10925791