If you forgive some self-advertisement, I think that a participation of the Rust community to the ML and HOPE workshops at ICFP (see my previous announce thread on internals) could help further the goals of the Rust Verification WG.
To verify Rust programs, you need to have a semantics of everyday Rust code, while foundational verification efforts such as RustBelt naturally study a suitably aestheticized subset of the langague (sufficient to express everyday programs, but without syntactic sugar or features designed for convenience, such as lifetime inference or the pattern-matching ergonomics). In a community which decentralizes the surface language design through the RFC process and numerous working groups, the best way to ensure that clean, formalizable translations exist between the evolving surface language and those core/simplified languages is to (1) disseminate precise descriptions of ongoing/new language features and (2) teach the wider “internals” community to use and produce these precise descriptions.
Participating to academic workshops on language design is an engaging, low-cost way to get started on that front – and there are enough knowledgeable people in the Rust community to serve as mentors to produce nice submissions. Not everyone can build Iris, but anyone that has gone through the demanding process of language design by RFCs can submit and participate to ICFP-colocated workshops on language design. Consider submitting to the ML workshop! (And encouraging/helping your fellow rustaceans to do it.)