Skip to content

Pull requests: verus-lang/verus

New pull request New
24 Open 973 Closed
24 Open 973 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Implement lifetime-checking by forking rustc_mir_build
#1792 opened Jul 2, 2025 by tjhance • Draft
4 tasks
fix #1644, do not ignore buckets that contain a single functions when computing module-level smt times
#1789 opened Jun 30, 2025 by utaal Loading…
Add support for Opaque types defined by function returns
#1785 opened Jun 26, 2025 by FeizaiYiHao Loading…
Allow external_body/assume_specification inside vstd
#1779 opened Jun 25, 2025 by zhengyao-lin Loading…
1
Split set, map into Finite & Infinite versions by generic type parameter
#1766 opened Jun 20, 2025 by jonhnet Loading…
1
Vec::swap_remove
#1755 opened Jun 18, 2025 by lengyijun Loading…
3
WIP: use prophecy encoding for functions that take a mutable reference as a parameter
#1738 opened Jun 12, 2025 by utaal • Draft
Spec-to-exec compiler macro exec_spec!
#1678 opened May 26, 2025 by zhengyao-lin • Draft
2
Add View and DeepView for Iterator
#1651 opened May 16, 2025 by txiang61 • Draft
1
Add external_trait_extension feature to extend external traits with spec functions
#1629 opened May 9, 2025 by Chris-Hawblitzel Loading…
5
Unambiguous View
#1598 opened Apr 17, 2025 by jaybosamiya-ms • Draft
16
Add specifications and laws for PartialEq, Eq, PartialOrd, Ord
#1569 opened Apr 4, 2025 by Chris-Hawblitzel Loading…
1
strong_call_ensures attribute
#1568 opened Apr 4, 2025 by Chris-Hawblitzel Loading…
1
change the encoding for consts and const fns
#1563 opened Apr 3, 2025 by tjhance • Draft
4
Support broadcast groups in traits
#1442 opened Feb 10, 2025 by utaal • Draft
get_impl_paths more exhaustive checks
#1342 opened Nov 13, 2024 by tjhance Loading…
@tjhance
6
Faster interpreter
#1225 opened Jul 14, 2024 by tjhance • Draft
2
Monomorphization
#1218 opened Jul 10, 2024 by lenianiva • Draft
@limpa105 @lenianiva
1
Documentation for arithmetic and mixed triggers
#1192 opened Jun 26, 2024 by matthias-brun • Draft
@utaal @matthias-brun
1
Add documentation on type sizes probably-easy
#1188 opened Jun 26, 2024 by hayley-leblanc • Draft
2
Support a module mode that verifies the contained proofs are in EPR and if so, enables the mbqi quant. instantiation strategy
#1000 opened Feb 19, 2024 by GenericMonkey • Draft
@utaal
2
Change Seq to an enum and verify its axioms probably-easy
#988 opened Feb 15, 2024 by tchajed • Draft
1
9
vargo: Decouple from rustup
#877 opened Nov 2, 2023 by zhaofengli • Draft
7
Generate our own impl block names for consistency between ghost/erased runs of rustc
#709 opened Jul 25, 2023 by Chris-Hawblitzel • Draft
23
ProTip! Adding no:label will show everything without a label.