SMT-based automated verification is a promising approach for ensuring software correctness, but it often suffers from unpredictability and proof instability due to the undecidability of the underlying logic. While tools like Liquid Haskell or F* provide automation, they either restrict logical expressivity to ensure decidability or sacrifice decidability and predictability for richer logic. In this paper, we present Ravencheck, a verification tool for Rust programs. Ravencheck occupies a unique design space: it supports specifications within an expressive fragment of Higher-Order Logic (HOL) while guaranteeing decidable verification outcomes. To achieve this, Ravencheck automatically encodes high-level Rust programs into the Extended Effectively Propositional (EEPR) fragment of first-order logic with relational abstraction. Ravencheck builds on prior EEPR-based modeling languages (e.g., Ivy) by integrating with the standard Rust toolchain. This integration supports a one-language workflow in which verification conditions are expressed using the same purely functional Rust syntax as the verified executable code, rather than introducing a separate modeling language.