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

Andrada-Livia Antoneac, Dorel Lucanu, Dragoş Teodor Gavriluţ

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…