verus

Tech stack & purpose

Verus is a project for verified Rust, a formal methods tool designed for proving properties of low-level systems code. The project incorporates a modified version of prettyplease, a minimal pretty-printer for Rust's `syn` syntax trees that converts AST structures into well-formatted source code strings. Prettyplease is built in Rust and designed as an alternative to rustfmt for formatting generated code, prioritizing reliability over perfection by ensuring entire inputs are always formattable rather than bailing out on complex constructs. The implementation is based on Derek C. Oppen's 1979 pretty-printing algorithm and uses the `syn` crate to work with Rust syntax trees.

Community & reference links

• verus-lang.zulipchat.com
• 💬 Zulip

Languages

Contributors (top 30 of 118)

• Andrea Lattuada1,091 commits
• Travis Hance1,081 commits
• Chris Hawblitzel699 commits
• Bryan Parno340 commits
• Chris Hawblitzel (Microsoft)154 commits
• tjhance116 commits
• Jay Lorch104 commits
• Chanhee Cho93 commits
• Jon Howell69 commits
• Baltasar Dinis62 commits
• ziqiaozhou53 commits
• 
  Jay Bosamiya51 commits · 881 followers
• Version Bumper Bot47 commits
• Máté Kovács45 commits
• Michael McLoughlin44 commits
• yizhou744 commits
• 
  Nickolai Zeldovich24 commits · 321 followers
• Alex Bai23 commits
• Ziqiao Zhou21 commits
• Daniel Schoepe20 commits
• Zhengyao Lin18 commits
• Isitha Subasinghe15 commits
• elanortang15 commits
• Xinyi Wan14 commits
• 
  Matthias14 commits · 4 followers
• Reto Achermann14 commits
• ahuoguo13 commits
• 
  Tej Chajed12 commits · 360 followers
• nobody12 commits
• hayley-leblanc12 commits