verus
forked from verus-lang/verus
Star 0
Fork 0
Watch

Version history of source/vstd/vstd.rs

October 2026

Bryan Parno
Make NonZero specifications available in default Cargo builds. (#3361)
committed

September 2026

Yuwei LIU
vstd: add BTreeMap specifications (#2831)
committed
Travis Hance
IterMut proof of concept (#2857)
committed
Chris Hawblitzel (Microsoft)
Add get and get_mut specs for SliceIndex, refactor slice::get spec (#2895)
committed
Chris Hawblitzel (Microsoft)
Support "panic!" and "assert!" macros (#2861)
committed

August 2026

Chris Hawblitzel (Microsoft)
Add specs for format macro to std_specs (#2787)
committed
Martin Mirchev
vstd: slice range index mut writeback (#2744)
committed

July 2026

Bryan Parno
Use the loop_isolation_boundary feature to simplify our specs for Rust iterators. (#2736)
committed
Baltasar Dinis
vstd: remove usage of group_seq_axioms and added axioms (#2678)
committed
Xinyi Wan
Add specifications for `NonZero` (#2471)
committed

June 2026

Jay Lorch
Make `Set` and `Map` finite, add `ISet` and `IMap`. (#2486)
committed
Daniel Schoepe
Upgrade verus to use Rust 1.96.0 (#2528)
committed

May 2026

Bryan Parno
New approach to specifying iterators via a prophetic sequence encoding (#2163)
committed
Travis Hance
update vstd to use the new_mut_ref style (#2408)
committed
Baltasar Dinis
resource: refactor existing PCM code (#2140)
committed

April 2026

Ruize Tang
Gate btree specs on alloc instead of alloc + std (#2365)
committed
Jay Lorch
Merge remote-tracking branch 'upstream/main' into fix-2290
committed
Xiangdong Chen
add support for async functions. TODO: async trait function (#1993)
committed
Chris Hawblitzel (Microsoft)
Translate general case of ExprKind::Index into calls to Index::index (#2300)
committed

March 2026

Natalie Neamtu
Support for unicode str, specs for std::str fns, specs for UTF-8 (#2238)
committed
Daniel Schoepe
Support Rust 1.94.0 (#2248)
committed
Chris Hawblitzel
Merge branch 'main' into ieee-float
committed
elanortang
Wrapping specs (#2204)
committed
Chris Hawblitzel
Merge branch 'main' into make_spec_type
committed

February 2026

Baltasar Dinis
vstd: add specs for BTreeMap and BTreeSet (#2189)
committed
Travis Hance
new-mut-ref: rename the deprecation attribute
committed
Chris Hawblitzel
Merge branch 'main' into assoc-const1
committed
Natalie Neamtu
Add EndianNat for reasoning about representations in different bases and endianness (#2125)
committed
Travis Hance
add migrate_postconditions_with_mut_refs to vstd (#2144)
committed
Travis Hance
vstd cell restructuring (#2032)
committed

January 2026

Travis Hance
remove broken attribute
committed
Travis Hance
new-mut-ref: add backwards-compatability attribute migrate_postconditions_with_mut_refs
committed
Travis Hance
new-mut-ref: more tests about unions
committed

November 2025

Daniel Schoepe
Upgrade verus to use rustc-1.91.0 (#1937)
committed

October 2025

Chris Hawblitzel
Merge branch 'main' into nonblocking_external_error
committed

September 2025

Zhengyao Lin
Move exec_spec to contrib directories
committed
Zhengyao Lin
Port exec_spec into Verus
committed
Chris Hawblitzel (Microsoft)
Add vstd/contrib and builtin_macros/src/contrib directories (#1813)
committed

August 2025

Chris Hawblitzel (Microsoft)
f32/f64 types and constants, with uninterpreted f32/f64 arithmetic (#1859)
committed

July 2025

ziqiaozhou
Add spec for range contains (#1806)
committed
Chris Hawblitzel (Microsoft)
Add specifications and laws for PartialEq, Eq, PartialOrd, Ord (#1569)
committed
Chris Hawblitzel
Allow cfg attribute on broadcast group items
committed

June 2025

Travis Hance
bugfix: more exhaustive well_formed checks (#1786)
committed
Natalie Neamtu
Merge branch 'main' into zero-to-nat/docs-retreat-2025
committed
Chris Hawblitzel
Merge branch 'main' into add-decreases
committed
Daniel Schoepe
Rustc 1.86 (#1735)
committed
Chris Hawblitzel
Merge branch 'main' into loop-infer-base
committed
Baltasar Dinis
vstd: add support for iterating over slices (#1709)
committed

May 2025

Andrea Lattuada
Upgrade to Rustc 1.85.1 (#1385)
committed
Jay Lorch
Broadcast VecDeque axioms (#1689)
committed