Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification.

arXiv:2609.34886v1 Announce Type: new Abstract: LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for veri