Rust is a modern programming language marrying the best of language design by offering fine-grained control over system resources (thus enabling efficient implementations), while simultaneously ensuring memory safety and data-race freedom. However, ensuring type safety in \emph{internally unsafe} libraries remains an important and non-trivial challenge, where unsafe features enable low-level control but can introduce undefined behaviour (UB). Existing works on reasoning about unsafe code either use \emph{verification} techniques to show \emph{correctness} (i.e. safety, useful only when the unsafe code is indeed correct), or use \emph{bug detection} techniques to show \emph{incorrectness} (i.e. unsafety) but fail to do so \emph{automatically} (to avoid developer burden), \emph{compositionally} (to support libraries without a main function), \emph{soundly} (without false positives) and \emph{generally} (rather than applying to specific patterns).

We close this gap by developing RUXt, a \emph{fully automatic}, \emph{compositional} bug detection technique for detecting UB in internally unsafe Rust libraries with a formal \emph{inadequacy} theorem (formalised and proven in Rocq) providing a \emph{no-false-positives guarantee}. RUXt leverages the Rust type system to under-approximate the set of safe values for user-defined types and detect safety violations without requiring manual annotations by the user. By encoding well-typed values in Rust as separation logic assertions, RUXt enables compositional reasoning about types to refute unsound type signatures and detect UB. The inadequacy theorem of RUXt ensures that each UB detected by RUXt in an internally unsafe library is a true safety violation that can be triggered by a \emph{safe} program, i.e. one that solely interacts with the safe API of the library. To this end, when RUXt identifies a UB, it additionally produces a \emph{safe program} witnessing the UB. In addition, we develop a prototype implementation in OCaml that can analyse programs written in a small model of Rust, and apply it to several case studies, showcasing its ability to detect true safety violations.