We are organizing a retreat for people involved in the Verus project. Bryan Parno (@parno) and the Secure Foundations Lab will be hosting the retreat at CMU on the Week of June 26th.

We are planning 3.5 days of "official" semi-structured time (Monday 26th till Thursday 29th at lunchtime), followed by 1.5 days of "optional" informal meet-ups, discussion, and hacking.

Sessions will begin at 9:30 AM. We will be meeting in the Collaborative Innovation Center (CIC), room 2101.

This is a tentative program.

Overview of new/upcoming features (2-3 hours in the morning)

• Traits (Chris)
• Prophecy variables (Andrea, Travis)
• State machines (Travis)
• Simple crash consistency framework (Jay L)

User experience improvements (2 hours in the afternoon)

• Proof actions (Chanhee)
• Setting up CI that includes other Verus projects (a-la crater) (Andrea)

Issue/feature request triage (1-2 hours in the afternoon)

6:00 PM -- Collaboration Dinner at Union Grill

• Documentation write-a-thon (2-3 hours in the morning)

(11am) Experience reports building systems in Verus (2 hours in the morning / afternoon)

• What's working well
• What isn't working

• Reto (NR)
• Matthias (Page Table)
• Jialin / Tenzin (Verusplinter)
• Jay L. / Jon (IronSHT)
• Jay B. (Serialization)
• Hayley (Crash-consistent log)

Afternoon sessions

• Proof stability (Yi + Jessica)
• Docs writing

• Issue triage (1 hour)

• 10:30AM: Brainstorming next big steps for Verus (1-2 hours in the morning)

• 1:00PM: Verus internals + Q&A (Chris + Andrea)

• Math library / Verus standard library (Liz and Alex)

• Axiom import sets (Andrea / Pranav)

• Recommends (Chris, ...)

(Escape Room -- Arrive by 6:45 pm at 145 E 8th Ave. Homestead, PA 15120)

• C to idiomatic Rust with LLMs and Verus (João)
• Writing specifications for Rust's standard library (intro) (Travis)
• Benchmarking suite for Verus (1 hours in the morning) (Chris)
• Discuss moving to an open chat channel (Zulip?) (Andrea)
• Syntax (Chris, ...)

Afternoon: Informal meetings and hacking

• Paper writing (Bryan)
• Bug fix hack-a-thon
• Writing specifications for Rust's standard library (hackathon)

• IronFleet hackathon (Jay L)
• Ghost features for Rust (Andrea)
• Writing specifications for Rust's standard library (hackathon)

Informal meetings and hacking