Discussions

• 1 You must be logged in to vote

  🗨️

  favour an attribute style procedural macros

  gilescope started May 5, 2024 in Language design · Closed

  

  

  1
• 4 You must be logged in to vote

  🗨️

  Import sets for ambient lemmas/axioms

  utaal started Jan 20, 2022 in Language design

  

  

  

  

  14
• 1 You must be logged in to vote

  💬

  Improve --verify-function and --verify-module

  utaal started Feb 21, 2023 in General

  

  

  4
• 1 You must be logged in to vote

  💬

  Consider using stable MIR at the top level of lowering HIR to VIR

  utaal started Apr 9, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  💬

  Support multiple trait implementations for the same outer type

  jaybosamiya started Apr 9, 2023 in General · Closed

  

  

  

  

  7
• 3 You must be logged in to vote

  💬

  Support associated types with bounds

  marshtompsxd started Jun 26, 2023 in General · Closed

  

  

  2
• 1 You must be logged in to vote

  🗨️

  Proposal: rework the rules for old(self) in preconditions and postconditions

  tchajed started Apr 18, 2023 in Language design

  

  

  

  

  11
• 1 You must be logged in to vote

  💬

  What's the best practice to combine verified code and original rust code?

  HaoYang670 started Aug 4, 2023 in General · Closed

  

  

  

  

  6
• 2 You must be logged in to vote

  🗨️

  Using Verus from unverified client code

  tjhance started Mar 24, 2022 in Language design

  

  

  

  

  19
• 1 You must be logged in to vote

  🗨️

  Ghostly DSTs

  jaybosamiya started Feb 15, 2023 in Language design

  

  

  1
• 1 You must be logged in to vote

  💬

  Replace fully axiomatic Seq with a model

  tchajed started Feb 15, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  🗨️

  Type invariants

  tjhance started Jan 17, 2024 in Language design

  

  

  4
• 1 You must be logged in to vote

  💬

  Documentation improvements

  utaal started Nov 24, 2023 in General

  

  

  1
• 1 You must be logged in to vote

  💬

  Certificate error on play.verus-lang.org

  eminence started Nov 1, 2023 in General · Closed

  

  

  1
• 1 You must be logged in to vote

  💬

  Constants and arithmetic in bitvector assertions

  matthias-brun started Oct 25, 2023 in General

  

  

  

  

  4
• 1 You must be logged in to vote

  🗨️

  Consider supporting assert (expression) by (spinoff)

  utaal started Oct 30, 2023 in Language design

  

  

  0
• 5 You must be logged in to vote

  💬

  Proof stability

  utaal started May 13, 2022 in General

  

  

  

  

  29
• 1 You must be logged in to vote

  🗨️

  Partial functions / changes to recommends checking

  utaal started Jul 14, 2023 in Language design · Closed

  

  

  4
• 2 You must be logged in to vote

  🗨️

  No analog of assert forall by for forall_arith; deprecate forall_arith?

  jaylorch started Jun 12, 2023 in Language design · Closed

  

  

  

  

  3
• 1 You must be logged in to vote

  🗨️

  Allow top-level reveal in exec mode (without a proof block)

  jaylorch started Apr 14, 2023 in Language design · Closed

  

  

  5
• 1 You must be logged in to vote

  🗨️

  Warn when declaring variables, parameters, and return values with a type with an incompatible mode

  utaal started Jun 9, 2022 in Language design · Closed

  

  

  2
• 1 You must be logged in to vote

  💬

  Support for associated types in trait

  marshtompsxd started Feb 8, 2023 in General · Closed

  

  

  

  

  3
• 2 You must be logged in to vote

  💬

  Too Many Assertions

  jonhnet started Mar 7, 2023 in General · Closed

  

  

  2
• 1 You must be logged in to vote

  💬

  Default trait method implementation blocked by no_method_body()

  marshtompsxd started Sep 28, 2022 in General · Closed

  

  

  2
• 1 You must be logged in to vote

  💬

  Use Seq drop_last in recursive definitions

  Chris-Hawblitzel started Sep 18, 2023 in General

  

  

  3