I'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?