diff --git a/dependencies/syn/src/lib.rs b/dependencies/syn/src/lib.rs
index b40004bfe6..14653425eb 100644
--- a/dependencies/syn/src/lib.rs
+++ b/dependencies/syn/src/lib.rs
@@ -556,10 +556,11 @@ pub use crate::verus::{
     BroadcastUse, Closed, DataMode, Decreases, Ensures, ExprGetField, ExprHas, ExprIs, ExprMatches,
     FnMode, Global, GlobalInner, GlobalLayout, GlobalSizeOf, Invariant, InvariantEnsures,
     InvariantExceptBreak, InvariantNameSet, InvariantNameSetAny, InvariantNameSetList,
-    InvariantNameSetNone, ItemBroadcastGroup, MatchesOpExpr, MatchesOpToken, Mode, ModeExec,
-    ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, Prover,
-    Publish, Recommends, Requires, Returns, RevealHide, SignatureDecreases, SignatureInvariants,
-    SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, TypeFnSpec, View,
+    InvariantNameSetNone, ItemBroadcastGroup, LoopSpec, MatchesOpExpr, MatchesOpToken, Mode,
+    ModeExec, ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted,
+    Prover, Publish, Recommends, Requires, Returns, RevealHide, SignatureDecreases,
+    SignatureInvariants, SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification,
+    TypeFnSpec, View,
 };
 
 #[rustfmt::skip] // https://github.com/rust-lang/rustfmt/issues/6176
diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs
index c31ec239c9..7d1910b1b7 100644
--- a/dependencies/syn/src/verus.rs
+++ b/dependencies/syn/src/verus.rs
@@ -2048,3 +2048,37 @@ pub(crate) fn parse_fn_spec(input: ParseStream) -> Result<TypeFnSpec> {
 
     Ok(fn_spec)
 }
+
+ast_struct! {
+    pub struct LoopSpec {
+        pub iter_name: Option<(Ident, Token![=>])>,
+        pub invariants: Option<Invariant>,
+        pub invariant_except_breaks: Option<InvariantExceptBreak>,
+        pub ensures: Option<Ensures>,
+        pub decreases: Option<Decreases>,
+    }
+}
+
+impl parse::Parse for LoopSpec {
+    fn parse(input: ParseStream) -> Result<Self> {
+        let iter_name = if input.peek2(Token![=>]) {
+            let pat = input.parse()?;
+            let token = input.parse()?;
+            Some((pat, token))
+        } else {
+            None
+        };
+
+        let invariants: Option<Invariant> = input.parse()?;
+        let invariant_except_breaks: Option<InvariantExceptBreak> = input.parse()?;
+        let ensures: Option<Ensures> = input.parse()?;
+        let decreases: Option<Decreases> = input.parse()?;
+        Ok(LoopSpec {
+            iter_name,
+            invariants,
+            invariant_except_breaks,
+            ensures,
+            decreases,
+        })
+    }
+}
diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs
index 086b8b0bb6..d0d7de362e 100644
--- a/source/builtin/src/lib.rs
+++ b/source/builtin/src/lib.rs
@@ -370,6 +370,12 @@ pub struct Tracked<A> {
     phantom: PhantomData<A>,
 }
 
+impl<A> core::fmt::Debug for Tracked<A> {
+    fn fmt(&self, _: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
+        Ok(())
+    }
+}
+
 impl<A> Ghost<A> {
     #[cfg(verus_keep_ghost)]
     #[rustc_diagnostic_item = "verus::builtin::Ghost::view"]
diff --git a/source/builtin_macros/src/attr_rewrite.rs b/source/builtin_macros/src/attr_rewrite.rs
index 7b37407c0f..151cdf4d1e 100644
--- a/source/builtin_macros/src/attr_rewrite.rs
+++ b/source/builtin_macros/src/attr_rewrite.rs
@@ -30,10 +30,9 @@
 ///
 /// Example:
 /// - Refer to `example/syntax_attr.rs`.
-use core::convert::TryFrom;
 use proc_macro2::TokenStream;
 use quote::{quote, quote_spanned, ToTokens};
-use syn::{parse2, spanned::Spanned, Ident, Item};
+use syn::{parse2, spanned::Spanned, Item};
 
 use crate::{
     attr_block_trait::{AnyAttrBlock, AnyFnOrLoop},
@@ -42,122 +41,6 @@ use crate::{
     EraseGhost,
 };
 
-#[derive(Debug)]
-pub enum SpecAttributeKind {
-    Requires,
-    Ensures,
-    Decreases,
-    Invariant,
-    InvariantExceptBreak,
-}
-
-struct SpecAttributeApply {
-    pub on_function: bool,
-    pub on_loop: bool,
-}
-
-type SpecAttrWithArgs = (SpecAttributeKind, TokenStream);
-
-impl SpecAttributeKind {
-    fn applies_to(&self) -> SpecAttributeApply {
-        let (on_function, on_loop) = match self {
-            SpecAttributeKind::Requires => (true, false),
-            SpecAttributeKind::Ensures => (true, true),
-            SpecAttributeKind::Decreases => (true, true),
-            SpecAttributeKind::Invariant => (false, true),
-            SpecAttributeKind::InvariantExceptBreak => (false, true),
-        };
-        SpecAttributeApply { on_function, on_loop }
-    }
-
-    fn applies_to_function(&self) -> bool {
-        self.applies_to().on_function
-    }
-
-    fn applies_to_loop(&self) -> bool {
-        self.applies_to().on_loop
-    }
-}
-
-impl TryFrom<String> for SpecAttributeKind {
-    type Error = String;
-
-    fn try_from(name: String) -> Result<Self, Self::Error> {
-        match name.as_str() {
-            "requires" => Ok(SpecAttributeKind::Requires),
-            "ensures" => Ok(SpecAttributeKind::Ensures),
-            "decreases" => Ok(SpecAttributeKind::Decreases),
-            "invariant" => Ok(SpecAttributeKind::Invariant),
-            _ => Err(name),
-        }
-    }
-}
-
-// Add brackets for requires, invariant.
-// Add brackets for ensures if it could not be parsed as a syn_verus::Expr.
-fn insert_brackets(attr_type: &SpecAttributeKind, tokens: TokenStream) -> TokenStream {
-    // Parse the TokenStream into a Syn Expression
-    match attr_type {
-        SpecAttributeKind::Ensures => {
-            // if the tokens are not valid verus expr, it might need a bracket.
-            syn_verus::parse2::<syn_verus::Expr>(tokens.clone())
-                .map_or(quote! {[#tokens]}, |e| quote! {#e})
-        }
-        SpecAttributeKind::Decreases => tokens,
-        _ => {
-            quote! {[#tokens]}
-        }
-    }
-}
-
-fn expand_verus_attribute(
-    erase: EraseGhost,
-    verus_attrs: Vec<SpecAttrWithArgs>,
-    any_with_attr_block: &mut dyn AnyAttrBlock,
-    function_or_loop: bool,
-) {
-    if !erase.keep() {
-        return;
-    }
-    // rewrite based on different spec attributes
-    for (attr_kind, attr_tokens) in verus_attrs {
-        if function_or_loop {
-            assert!(attr_kind.applies_to_function());
-        }
-        if !function_or_loop {
-            assert!(attr_kind.applies_to_loop());
-        }
-        match attr_kind {
-            SpecAttributeKind::Invariant => {
-                insert_spec_call(any_with_attr_block, "invariant", attr_tokens)
-            }
-            SpecAttributeKind::Decreases => {
-                insert_spec_call(any_with_attr_block, "decreases", attr_tokens)
-            }
-            SpecAttributeKind::Ensures => {
-                insert_spec_call(any_with_attr_block, "ensures", attr_tokens)
-            }
-            SpecAttributeKind::Requires => {
-                insert_spec_call(any_with_attr_block, "requires", attr_tokens)
-            }
-            SpecAttributeKind::InvariantExceptBreak => {
-                insert_spec_call(any_with_attr_block, "invariant_except_break", attr_tokens)
-            }
-        }
-    }
-}
-
-fn insert_spec_call(any_fn: &mut dyn AnyAttrBlock, call: &str, verus_expr: TokenStream) {
-    let fname = Ident::new(call, verus_expr.span());
-    let tokens: TokenStream =
-        syntax::rewrite_expr(EraseGhost::Keep, true, verus_expr.into()).into();
-    any_fn.block_mut().unwrap().stmts.insert(
-        0,
-        parse2(quote! { #[verus::internal(const_header_wrapper)]||{::builtin::#fname(#tokens);};})
-            .unwrap(),
-    );
-}
-
 pub fn rewrite_verus_attribute(
     erase: &EraseGhost,
     attr_args: Vec<syn::Ident>,
@@ -203,23 +86,27 @@ pub fn rewrite_verus_spec(
             // (In the normal case, this results in a redundant extra error message after
             // the normal Rust syntax error, but it's a reasonable looking error message.)
             return proc_macro::TokenStream::from(
-                quote_spanned!(err.span() => compile_error!("syntax error in function");),
+                quote_spanned!(err.span() => compile_error!("Misuse of #[verus_spec]");),
             );
         }
     };
-    let spec_attr =
-        syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::SignatureSpecAttr);
+
     match f {
         AnyFnOrLoop::Fn(mut fun) => {
+            let spec_attr =
+                syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::SignatureSpecAttr);
             // Note: trait default methods appear in this case,
             // since they look syntactically like non-trait functions
             let spec_stmts = syntax::sig_specs_attr(erase, spec_attr, &fun.sig);
             let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap());
             let _ = fun.block_mut().unwrap().stmts.splice(0..0, new_stmts);
             fun.attrs.push(mk_verus_attr_syn(fun.span(), quote! { verus_macro }));
+
             proc_macro::TokenStream::from(fun.to_token_stream())
         }
         AnyFnOrLoop::TraitMethod(mut method) => {
+            let spec_attr =
+                syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::SignatureSpecAttr);
             // Note: default trait methods appear in the AnyFnOrLoop::Fn case, not here
             let spec_stmts = syntax::sig_specs_attr(erase, spec_attr, &method.sig);
             let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap());
@@ -232,41 +119,28 @@ pub fn rewrite_verus_spec(
             method.to_tokens(&mut new_stream);
             proc_macro::TokenStream::from(new_stream)
         }
-        _ => {
-            let span = spec_attr.span();
-            proc_macro::TokenStream::from(
-                quote_spanned!(span => compile_error!("'verus_spec' is not allowed here");),
-            )
+        AnyFnOrLoop::ForLoop(forloop) => {
+            let spec_attr = syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::LoopSpec);
+            syntax::for_loop_spec_attr(erase, spec_attr, forloop).to_token_stream().into()
         }
-    }
-}
-
-pub fn rewrite(
-    erase: EraseGhost,
-    outer_attr: SpecAttributeKind,
-    outer_attr_tokens: TokenStream,
-    input: TokenStream,
-) -> Result<TokenStream, syn::Error> {
-    let span = outer_attr_tokens.span();
-    let outer_attr_tokens = insert_brackets(&outer_attr, outer_attr_tokens);
-    let verus_attrs = vec![(outer_attr, outer_attr_tokens)];
-    let f = parse2::<AnyFnOrLoop>(input)?;
-    match f {
         AnyFnOrLoop::Loop(mut l) => {
-            expand_verus_attribute(erase, verus_attrs, &mut l, false);
-            Ok(quote_spanned! {l.span()=>#l})
-        }
-        AnyFnOrLoop::ForLoop(mut l) => {
-            expand_verus_attribute(erase, verus_attrs, &mut l, false);
-            Ok(quote_spanned! {l.span()=>#l})
+            let spec_attr = syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::LoopSpec);
+            let spec_stmts = syntax::while_loop_spec_attr(erase, spec_attr);
+            let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap());
+            if erase.keep() {
+                l.body.stmts.splice(0..0, new_stmts);
+            }
+            l.to_token_stream().into()
         }
         AnyFnOrLoop::While(mut l) => {
-            expand_verus_attribute(erase, verus_attrs, &mut l, false);
-            Ok(quote_spanned! {l.span()=>#l})
+            let spec_attr = syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::LoopSpec);
+            let spec_stmts = syntax::while_loop_spec_attr(erase, spec_attr);
+            let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap());
+            if erase.keep() {
+                l.body.stmts.splice(0..0, new_stmts);
+            }
+            l.to_token_stream().into()
         }
-        AnyFnOrLoop::Fn(_) | AnyFnOrLoop::TraitMethod(_) => Ok(
-            quote_spanned!(span => compile_error!("'verus_spec' attribute expected on function");),
-        ),
     }
 }
 
diff --git a/source/builtin_macros/src/lib.rs b/source/builtin_macros/src/lib.rs
index 6abb95fc80..aa67d93815 100644
--- a/source/builtin_macros/src/lib.rs
+++ b/source/builtin_macros/src/lib.rs
@@ -7,7 +7,6 @@
     feature(proc_macro_diagnostic)
 )]
 
-use attr_rewrite::SpecAttributeKind;
 #[cfg(verus_keep_ghost)]
 use std::sync::OnceLock;
 use synstructure::{decl_attribute, decl_derive};
@@ -280,71 +279,6 @@ pub fn verus_spec(
     }
 }
 
-// The attribute should work together with verus_verify attribute.
-#[proc_macro_attribute]
-pub fn ensures(
-    attr: proc_macro::TokenStream,
-    input: proc_macro::TokenStream,
-) -> proc_macro::TokenStream {
-    let erase = cfg_erase();
-    if erase.keep() {
-        attr_rewrite::rewrite(erase, SpecAttributeKind::Ensures, attr.into(), input.into())
-            .expect("Misuse of #[ensures()].")
-            .into()
-    } else {
-        input
-    }
-}
-
-// The attribute should work together with verus_verify attribute.
-#[proc_macro_attribute]
-pub fn decreases(
-    attr: proc_macro::TokenStream,
-    input: proc_macro::TokenStream,
-) -> proc_macro::TokenStream {
-    let erase = cfg_erase();
-    if erase.keep() {
-        attr_rewrite::rewrite(erase, SpecAttributeKind::Decreases, attr.into(), input.into())
-            .expect("Misuse of #[decreases()].")
-            .into()
-    } else {
-        input
-    }
-}
-
-// The attribute should work together with verus_verify attribute.
-#[proc_macro_attribute]
-pub fn invariant(
-    attr: proc_macro::TokenStream,
-    input: proc_macro::TokenStream,
-) -> proc_macro::TokenStream {
-    let erase = cfg_erase();
-    if erase.keep() {
-        attr_rewrite::rewrite(erase, SpecAttributeKind::Invariant, attr.into(), input.into())
-            .expect("Misuse of #[invariant()]")
-            .into()
-    } else {
-        input
-    }
-}
-
-// The attribute should work together with verus_verify attribute.
-#[proc_macro_attribute]
-pub fn invariant_except_break(
-    attr: proc_macro::TokenStream,
-    input: proc_macro::TokenStream,
-) -> proc_macro::TokenStream {
-    let erase = cfg_erase();
-    if erase.keep() {
-        let kind = SpecAttributeKind::InvariantExceptBreak;
-        attr_rewrite::rewrite(erase, kind, attr.into(), input.into())
-            .expect("Misuse of #[invariant_except_break()]")
-            .into()
-    } else {
-        input
-    }
-}
-
 #[proc_macro]
 pub fn proof(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     attr_rewrite::proof_rewrite(cfg_erase(), input.into()).into()
diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs
index dbf96012ef..d6d671a4ce 100644
--- a/source/builtin_macros/src/syntax.rs
+++ b/source/builtin_macros/src/syntax.rs
@@ -20,6 +20,7 @@ use syn_verus::visit_mut::{
 };
 use syn_verus::BroadcastUse;
 use syn_verus::ExprBlock;
+use syn_verus::ExprForLoop;
 use syn_verus::{
     braced, bracketed, parenthesized, parse_macro_input, AssumeSpecification, Attribute, BareFnArg,
     BinOp, Block, DataMode, Decreases, Ensures, Expr, ExprBinary, ExprCall, ExprLit, ExprLoop,
@@ -239,6 +240,26 @@ impl Visitor {
         }
     }
 
+    fn visit_loop_spec(&mut self, spec: &mut syn_verus::LoopSpec) {
+        let mut visit_spec = |exprs: &mut syn_verus::Specification| {
+            for expr in exprs.exprs.iter_mut() {
+                self.visit_expr_mut(expr);
+            }
+        };
+        if let Some(exprs) = spec.invariants.as_mut() {
+            visit_spec(&mut exprs.exprs);
+        }
+        if let Some(exprs) = spec.invariant_except_breaks.as_mut() {
+            visit_spec(&mut exprs.exprs);
+        }
+        if let Some(exprs) = spec.ensures.as_mut() {
+            visit_spec(&mut exprs.exprs);
+        }
+        if let Some(exprs) = spec.decreases.as_mut() {
+            visit_spec(&mut exprs.exprs);
+        }
+    }
+
     fn take_sig_specs<TType: ToTokens>(
         &mut self,
         spec: &mut SignatureSpec,
@@ -1256,7 +1277,7 @@ impl Visitor {
                                     broadcast proof fn #lemma_ident()
                                         ensures
                                             #[trigger] #vstd::layout::size_of::<#type_>() == #size_lit,
-                                            ::vstd::layout::is_sized::<#type_>(),
+                                            #vstd::layout::is_sized::<#type_>(),
                                             #ensures_align
                                     {
                                     }
@@ -3981,6 +4002,78 @@ pub(crate) fn sig_specs_attr(
     visitor.take_sig_specs(&mut spec, ret_pat, sig.constness.is_some(), sig_span)
 }
 
+pub(crate) fn while_loop_spec_attr(
+    erase_ghost: EraseGhost,
+    spec_attr: syn_verus::LoopSpec,
+) -> Vec<Stmt> {
+    let mut visitor = Visitor {
+        erase_ghost,
+        use_spec_traits: true,
+        inside_ghost: 1,
+        inside_type: 0,
+        inside_external_code: 0,
+        inside_const: false,
+        inside_arith: InsideArith::None,
+        assign_to: false,
+        rustdoc: env_rustdoc(),
+    };
+    let mut spec_attr = spec_attr;
+    visitor.visit_loop_spec(&mut spec_attr);
+    let syn_verus::LoopSpec { invariants, invariant_except_breaks, ensures, decreases, .. } =
+        spec_attr;
+    let mut stmt = vec![];
+    visitor.add_loop_specs(
+        &mut stmt,
+        invariant_except_breaks,
+        invariants,
+        None,
+        ensures,
+        decreases,
+    );
+    stmt
+}
+
+pub(crate) fn for_loop_spec_attr(
+    erase_ghost: EraseGhost,
+    spec_attr: syn_verus::LoopSpec,
+    forloop: syn::ExprForLoop,
+) -> syn_verus::Expr {
+    let mut visitor = Visitor {
+        erase_ghost,
+        use_spec_traits: true,
+        inside_ghost: 1,
+        inside_type: 0,
+        inside_external_code: 0,
+        inside_const: false,
+        inside_arith: InsideArith::None,
+        assign_to: false,
+        rustdoc: env_rustdoc(),
+    };
+    let mut spec_attr = spec_attr;
+    visitor.visit_loop_spec(&mut spec_attr);
+    let syn_verus::LoopSpec { iter_name, invariants: invariant, decreases, .. } = spec_attr;
+    let syn::ExprForLoop { attrs, label, for_token, pat, in_token, expr, body, .. } = forloop;
+    let verus_forloop = ExprForLoop {
+        attrs: attrs.into_iter().map(|a| parse_quote_spanned! {a.span() => #a}).collect(),
+        label: label.map(|l| syn_verus::Label {
+            name: syn_verus::Lifetime::new(l.name.ident.to_string().as_str(), l.name.span()),
+            colon_token: Token![:](l.colon_token.span),
+        }),
+        for_token: Token![for](for_token.span),
+        pat: Box::new(Pat::Verbatim(quote_spanned! {pat.span() => #pat})),
+        in_token: Token![in](in_token.span),
+        expr_name: iter_name.map(|(name, token)| Box::new((name, Token![:](token.span())))),
+        expr: Box::new(Expr::Verbatim(quote_spanned! {expr.span() => #expr})),
+        invariant,
+        decreases,
+        body: Block {
+            brace_token: Brace(body.brace_token.span),
+            stmts: vec![Stmt::Expr(Expr::Verbatim(quote_spanned! {body.span() => #body}), None)],
+        },
+    };
+    visitor.desugar_for_loop(verus_forloop)
+}
+
 // Unfortunately, the macro_rules tt tokenizer breaks tokens like &&& and ==> into smaller tokens.
 // Try to put the original tokens back together here.
 #[cfg(verus_keep_ghost)]
diff --git a/source/rust_verify/example/guide/bst_map_generic.rs b/source/rust_verify/example/guide/bst_map_generic.rs
index d7a6e83858..143c0c541a 100644
--- a/source/rust_verify/example/guide/bst_map_generic.rs
+++ b/source/rust_verify/example/guide/bst_map_generic.rs
@@ -392,13 +392,9 @@ impl<K: Copy + TotalOrdered, V: Clone> Clone for Node<K, V> {
             forall |key| #[trigger] res.as_map().dom().contains(key) ==>
                 cloned::<V>(self.as_map()[key], res.as_map()[key])
     {
-        // TODO(fixme): Assigning V::clone to a variable is a hack needed to work around
-        // this issue: https://github.com/verus-lang/verus/issues/1348
-        let v_clone = V::clone;
-
         let res = Node {
             key: self.key,
-            value: v_clone(&self.value),
+            value: self.value.clone(),
             // Ordinarily, we would use Option<Node>::clone rather than inlining
             // the case statement here; we write it this way to work around
             // this issue: https://github.com/verus-lang/verus/issues/1346
diff --git a/source/rust_verify/example/guide/invariants.rs b/source/rust_verify/example/guide/invariants.rs
index abecd1955a..66ce6eead0 100644
--- a/source/rust_verify/example/guide/invariants.rs
+++ b/source/rust_verify/example/guide/invariants.rs
@@ -3,6 +3,7 @@ use builtin::*;
 #[allow(unused_imports)]
 use builtin_macros::*;
 use vstd::prelude::*;
+use vstd::arithmetic::overflow::*;
 
 verus! {
 
@@ -129,6 +130,64 @@ fn fib_impl(n: u64) -> (result: u64)
 }
 // ANCHOR_END: fib_final
 
+// ANCHOR: fib_checked
+fn fib_checked(n: u64) -> (result: u64)
+    requires
+        fib(n as nat) <= u64::MAX
+    ensures
+        result == fib(n as nat),
+{
+    if n == 0 {
+        return 0;
+    }
+    let mut prev: CheckedU64 = CheckedU64::new(0);
+    let mut cur: CheckedU64 = CheckedU64::new(1);
+    let mut i: u64 = 1;
+    while i < n
+        invariant
+            0 < i <= n,
+            fib(n as nat) <= u64::MAX,
+            cur@ == fib(i as nat),
+            prev@ == fib((i - 1) as nat),
+    {
+        i = i + 1;
+        let new_cur = cur.add_checked(&prev);
+        prev = cur;
+        cur = new_cur;
+    }
+    cur.unwrap()
+}
+// ANCHOR_END: fib_checked
+
+// ANCHOR: fib_checked_no_precondition
+fn fib_checked_no_precondition(n: u64) -> (result: Option<u64>)
+    ensures
+        match result {
+            Some(x) => x == fib(n as nat),
+            None => fib(n as nat) > u64::MAX,
+        },
+{
+    if n == 0 {
+        return Some(0);
+    }
+    let mut prev: CheckedU64 = CheckedU64::new(0);
+    let mut cur: CheckedU64 = CheckedU64::new(1);
+    let mut i: u64 = 1;
+    while i < n
+        invariant
+            0 < i <= n,
+            cur@ == fib(i as nat),
+            prev@ == fib((i - 1) as nat),
+    {
+        i = i + 1;
+        let new_cur = cur.add_checked(&prev);
+        prev = cur;
+        cur = new_cur;
+    }
+    cur.to_option()
+}
+// ANCHOR_END: fib_checked_no_precondition
+
 
 // ANCHOR: bank_spec
 spec fn always_non_negative(s: Seq<i64>) -> bool
diff --git a/source/rust_verify/example/overflow.rs b/source/rust_verify/example/overflow.rs
new file mode 100644
index 0000000000..b8cda3f0e0
--- /dev/null
+++ b/source/rust_verify/example/overflow.rs
@@ -0,0 +1,69 @@
+// examples of using `CheckedU32` and `CheckedU64`
+use vstd::prelude::*;
+use vstd::arithmetic::overflow::*;
+
+verus! {
+
+fn checked_u64_constants()
+{
+    let w = CheckedU64::new(0xFFFFFFFFFFFFFFFF);
+    let x = w.add_value(1);
+    assert(x.is_overflowed());
+    assert(x.view() == 0x10000000000000000);
+
+    let y = CheckedU64::new(0x8000000000000000);
+    let z = y.mul_value(2);
+    assert(z.is_overflowed());
+    assert(z.view() == 0x10000000000000000);
+}
+
+fn checked_u64_calculations(a: u64, b: u64, c: u64, d: u64) -> (result: Option<u64>)
+    ensures
+        match result {
+            Some(v) => v == a * b + c * d,
+            None => a * b + c * d > u64::MAX,
+        }
+{
+    let a_times_b = CheckedU64::new(a).mul_value(b);
+    let c_times_d = CheckedU64::new(c).mul_value(d);
+    let sum_of_products = a_times_b.add_checked(&c_times_d);
+    if sum_of_products.is_overflowed() {
+        assert(a * b + c * d > u64::MAX);
+        None
+    }
+    else {
+        let i: u64 = sum_of_products.unwrap();
+        assert(i == a * b + c * d);
+        Some(i)
+    }
+}
+
+fn checked_u32_constants()
+{
+    let w = CheckedU32::new(0xFFFFFFFF);
+    let x = w.add_value(9);
+    assert(x.is_overflowed());
+    assert(x.view() == 0x100000008);
+
+    let y = CheckedU32::new(0x40000000);
+    let z = y.mul_value(8);
+    assert(z.is_overflowed());
+    assert(z.view() == 0x200000000);
+}
+
+fn checked_u32_calculations(a: u32, b: u32, c: u32, d: u32, e: u32) -> (result: Option<u32>)
+    ensures
+        match result {
+            Some(v) => v == a * b + c * d + e,
+            None => a * b + c * d + e > u32::MAX,
+        }
+{
+    let a_times_b = CheckedU32::new(a).mul_value(b);
+    let c_times_d = CheckedU32::new(c).mul_value(d);
+    let sum_of_products = a_times_b.add_checked(&c_times_d);
+    let f = sum_of_products.add_value(e);
+    f.to_option()
+}
+
+} // verus!
+fn main() {}
diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs
index a79cbb4b61..2b969cf446 100644
--- a/source/rust_verify/src/attributes.rs
+++ b/source/rust_verify/src/attributes.rs
@@ -978,6 +978,21 @@ pub(crate) fn get_external_attrs(
 pub(crate) fn get_verifier_attrs(
     attrs: &[Attribute],
     diagnostics: Option<&mut Vec<VirErrAs>>,
+) -> Result<VerifierAttrs, VirErr> {
+    get_verifier_attrs_maybe_check(attrs, diagnostics, true)
+}
+
+pub(crate) fn get_verifier_attrs_no_check(
+    attrs: &[Attribute],
+    diagnostics: Option<&mut Vec<VirErrAs>>,
+) -> Result<VerifierAttrs, VirErr> {
+    get_verifier_attrs_maybe_check(attrs, diagnostics, false)
+}
+
+pub(crate) fn get_verifier_attrs_maybe_check(
+    attrs: &[Attribute],
+    diagnostics: Option<&mut Vec<VirErrAs>>,
+    do_check: bool,
 ) -> Result<VerifierAttrs, VirErr> {
     let mut vs = VerifierAttrs {
         verus_macro: false,
@@ -1096,8 +1111,10 @@ pub(crate) fn get_verifier_attrs(
             _ => {}
         }
     }
-    if let Some((rustc_attr, span)) = unsupported_rustc_attr {
-        return err_span(span, format!("The attribute `{rustc_attr:}` is not supported"));
+    if do_check {
+        if let Some((rustc_attr, span)) = unsupported_rustc_attr {
+            return err_span(span, format!("The attribute `{rustc_attr:}` is not supported"));
+        }
     }
     Ok(vs)
 }
diff --git a/source/rust_verify/src/context.rs b/source/rust_verify/src/context.rs
index 19d18322eb..e8f0ffcaf0 100644
--- a/source/rust_verify/src/context.rs
+++ b/source/rust_verify/src/context.rs
@@ -58,6 +58,16 @@ impl<'tcx> ContextX<'tcx> {
         crate::attributes::get_verifier_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut()))
     }
 
+    pub(crate) fn get_verifier_attrs_no_check(
+        &self,
+        attrs: &[Attribute],
+    ) -> Result<crate::attributes::VerifierAttrs, vir::ast::VirErr> {
+        crate::attributes::get_verifier_attrs_no_check(
+            attrs,
+            Some(&mut *self.diagnostics.borrow_mut()),
+        )
+    }
+
     pub(crate) fn get_external_attrs(
         &self,
         attrs: &[Attribute],
diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs
index 48dd33c571..55705628a3 100644
--- a/source/rust_verify/src/external.rs
+++ b/source/rust_verify/src/external.rs
@@ -135,7 +135,7 @@ pub(crate) fn get_crate_items<'tcx>(ctxt: &Context<'tcx>) -> Result<CrateItems,
         state: default_state,
         module_path: root_module_path,
         errors: vec![],
-        is_impl_trait: false,
+        in_impl: None,
     };
     let owner = ctxt.tcx.hir_owner_node(rustc_hir::CRATE_OWNER_ID);
     visitor.visit_mod(root_module, owner.span(), rustc_hir::CRATE_HIR_ID);
@@ -171,6 +171,13 @@ enum VerifState {
     External,
 }
 
+// Information about the impl, used when visitings its ImplItems.
+#[derive(Copy, Clone)]
+struct InsideImpl {
+    is_trait: bool,
+    has_any_verus_aware_item: bool,
+}
+
 struct VisitMod<'a, 'tcx> {
     items: Vec<CrateItem>,
     ctxt: &'a Context<'tcx>,
@@ -178,7 +185,7 @@ struct VisitMod<'a, 'tcx> {
 
     state: VerifState,
     module_path: Path,
-    is_impl_trait: bool,
+    in_impl: Option<InsideImpl>,
 }
 
 impl<'a, 'tcx> rustc_hir::intravisit::Visitor<'tcx> for VisitMod<'a, 'tcx> {
@@ -250,7 +257,6 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
                 if eattrs.external {
                     VerifState::External
                 } else if opts_in_to_verus(&eattrs) {
-                    //|| opts_in_by_automatic_derive(&self.ctxt, &general_item, &attrs) {
                     VerifState::Verify
                 } else {
                     VerifState::Default
@@ -266,10 +272,18 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
             VerifState::External => VerifState::External,
         };
 
+        if matches!(general_item, GeneralItem::ImplItem(_)) && self.in_impl.is_none() {
+            self.errors.push(crate::util::err_span_bare(
+                span,
+                "Verus internal error: expected ImplItem to be child of Impl",
+            ));
+            return;
+        }
+
         // Error if any item of a trait or trait impl is ignored.
 
         if matches!(general_item, GeneralItem::ImplItem(_))
-            && self.is_impl_trait
+            && self.in_impl.as_ref().unwrap().is_trait
             && self.state == VerifState::Verify
             && state_for_this_item == VerifState::External
         {
@@ -290,6 +304,12 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
             return;
         }
 
+        if matches!(general_item, GeneralItem::ImplItem(_))
+            && state_for_this_item == VerifState::Verify
+        {
+            self.in_impl.as_mut().unwrap().has_any_verus_aware_item = true;
+        }
+
         // Append this item to the items
 
         let verif = if state_for_this_item == VerifState::Verify {
@@ -309,6 +329,7 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
         };
 
         self.items.push(CrateItem { id: general_item.id(), verif });
+        let this_item_idx = self.items.len() - 1;
 
         // Compute the context for any _nested_ items
 
@@ -330,9 +351,10 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
 
         let saved_state = self.state;
         let saved_mod = self.module_path.clone();
-        let saved_is_impl_trait = self.is_impl_trait;
+        let saved_in_impl = self.in_impl;
 
         self.state = state_inside;
+        self.in_impl = None;
 
         match general_item {
             GeneralItem::Item(item) => match item.kind {
@@ -341,7 +363,10 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
                         def_id_to_vir_path(self.ctxt.tcx, &self.ctxt.verus_items, def_id);
                 }
                 ItemKind::Impl(impll) => {
-                    self.is_impl_trait = impll.of_trait.is_some();
+                    self.in_impl = Some(InsideImpl {
+                        is_trait: impll.of_trait.is_some(),
+                        has_any_verus_aware_item: false,
+                    });
                 }
                 _ => {}
             },
@@ -355,9 +380,37 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
             GeneralItem::TraitItem(i) => rustc_hir::intravisit::walk_trait_item(self, i),
         }
 
+        if let Some(in_impl) = self.in_impl {
+            if in_impl.has_any_verus_aware_item && state_for_this_item != VerifState::Verify {
+                // Suppose the user writes something like:
+                //
+                // impl X {
+                //     verus!{
+                //          fn foo() { ... }
+                //     }
+                // }
+                //
+                // We need to make sure 'foo' isn't skipped just because the impl block
+                // as a whole isn't marked verify.
+                //
+                // For _normal impls_, we just go ahead and mark the impl as verification-aware.
+                // For _trait impls_, this situation would be too complicated, so we error.
+
+                if in_impl.is_trait {
+                    self.errors.push(crate::util::err_span_bare(
+                        span,
+                        "In order to verify any items of this trait impl, the entire impl must be verified. Try wrapping the entire impl in the `verus!` macro.",
+                    ));
+                } else {
+                    self.items[this_item_idx].verif =
+                        VerifOrExternal::VerusAware { module_path: self.module_path.clone() }
+                }
+            }
+        }
+
         self.state = saved_state;
         self.module_path = saved_mod;
-        self.is_impl_trait = saved_is_impl_trait;
+        self.in_impl = saved_in_impl;
     }
 }
 
@@ -500,54 +553,3 @@ impl<'a> GeneralItem<'a> {
         }
     }
 }
-
-/*
-fn opts_in_by_automatic_derive<'tcx>(
-    ctxt: &Context<'tcx>,
-    general_item: &GeneralItem<'tcx>,
-    attrs: &[rustc_ast::Attribute],
-) -> bool {
-    if is_automatically_derived(attrs) {
-        match general_item {
-            GeneralItem::Item(item) => match &item.kind {
-                ItemKind::Impl(impll) => {
-                    let def_id = match impll.self_ty.kind {
-                        rustc_hir::TyKind::Path(rustc_hir::QPath::Resolved(None, path)) => path.res.def_id(),
-                        _ => { return false; }
-                    };
-                    if let Some(local_def_id) = def_id.as_local() {
-                        let hir_id = ctxt.tcx.local_def_id_to_hir_id(local_def_id);
-                        let attrs = ctxt.tcx.hir().attrs(hir_id);
-                        let eattrs = match ctxt.get_external_attrs(attrs) {
-                            Ok(eattrs) => eattrs,
-                            Err(_) => { return false; }
-                        };
-                        opts_in_to_verus(&eattrs)
-                    } else {
-                        false
-                    }
-                }
-                _ => false,
-            }
-            _ => false,
-        }
-    } else {
-        false
-    }
-}
-
-fn is_automatically_derived(attrs: &[rustc_ast::Attribute]) -> bool {
-    for attr in attrs.iter() {
-        match &attr.kind {
-            rustc_ast::AttrKind::Normal(item) => match &item.item.path.segments[..] {
-                [segment] => if segment.ident.as_str() == "automatically_derived" {
-                    return true;
-                }
-                _ => { }
-            }
-            _ => { }
-        }
-    }
-    false
-}
-*/
diff --git a/source/rust_verify/src/rust_to_vir_global.rs b/source/rust_verify/src/rust_to_vir_global.rs
index 2a7e532aee..af5b9bb926 100644
--- a/source/rust_verify/src/rust_to_vir_global.rs
+++ b/source/rust_verify/src/rust_to_vir_global.rs
@@ -22,7 +22,7 @@ pub(crate) fn process_const_early<'tcx>(
     item: &Item<'tcx>,
 ) -> Result<(), VirErr> {
     let attrs = ctxt.tcx.hir().attrs(item.hir_id());
-    let vattrs = ctxt.get_verifier_attrs(attrs)?;
+    let vattrs = ctxt.get_verifier_attrs_no_check(attrs)?;
     if vattrs.size_of_global {
         let err = crate::util::err_span(item.span, "invalid global size_of");
         let ItemKind::Const(_ty, generics, body_id) = item.kind else {
diff --git a/source/rust_verify_test/tests/fndef_types.rs b/source/rust_verify_test/tests/fndef_types.rs
index bae791f907..e7509d5161 100644
--- a/source/rust_verify_test/tests/fndef_types.rs
+++ b/source/rust_verify_test/tests/fndef_types.rs
@@ -1725,3 +1725,179 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] generic_conditions_for_normal_call verus_code! {
+        spec fn foo_req(x: u64) -> bool;
+        spec fn foo_ens(x: u64, a: u64) -> bool;
+
+        fn foo(x: u64) -> (a: u64)
+            requires foo_req(x),
+            ensures foo_ens(x, a),
+        {
+            assume(false);
+            20
+        }
+
+        fn test(x: u64) {
+            assume(call_requires(foo, (x,)));
+            let r = foo(x);
+            assert(call_ensures(foo, (x,), r));
+        }
+
+        fn test_fails(x: u64) {
+            assume(call_requires(foo, (x,)));
+            let r = foo(x);
+            assert(call_ensures(foo, (x,), r));
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 1)
+}
+
+test_verify_one_file! {
+    #[test] generic_conditions_for_normal_call_returns_unit verus_code! {
+        spec fn foo_req(x: u64) -> bool;
+        spec fn foo_ens(x: u64, a: u64) -> bool;
+
+        fn foo(x: u64)
+            requires foo_req(x),
+            ensures foo_ens(x, 0),
+        {
+            assume(false);
+        }
+
+        fn test(x: u64) {
+            assume(call_requires(foo, (x,)));
+            foo(x);
+            assert(call_ensures(foo, (x,), ()));
+        }
+
+        fn test_fails(x: u64) {
+            assume(call_requires(foo, (x,)));
+            foo(x);
+            assert(call_ensures(foo, (x,), ()));
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 1)
+}
+
+test_verify_one_file! {
+    #[test] generic_conditions_for_normal_call_no_spec verus_code! {
+        fn foo(x: u64) -> (a: u64) {
+            assume(false);
+            20
+        }
+
+        fn test(x: u64) {
+            assume(call_requires(foo, (x,)));
+            let r = foo(x);
+            assert(call_ensures(foo, (x,), r));
+        }
+
+        fn test_fails(x: u64) {
+            assume(call_requires(foo, (x,)));
+            let r = foo(x);
+            assert(call_ensures(foo, (x,), r));
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 1)
+}
+
+test_verify_one_file! {
+    #[test] generic_conditions_for_normal_call_return_unit_no_spec verus_code! {
+        fn foo(x: u64) {
+            assume(false);
+        }
+
+        fn test(x: u64) {
+            assume(call_requires(foo, (x,)));
+            foo(x);
+            assert(call_ensures(foo, (x,), ()));
+        }
+
+        fn test_fails(x: u64) {
+            assume(call_requires(foo, (x,)));
+            foo(x);
+            assert(call_ensures(foo, (x,), ()));
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 1)
+}
+
+test_verify_one_file! {
+    #[test] generic_conditions_for_normal_call_traits verus_code! {
+        trait Tr : Sized {
+            spec fn foo_req(&self) -> bool;
+            spec fn foo_ens(&self, a: Self) -> bool;
+
+            fn foo(&self) -> (a: Self)
+                requires self.foo_req(),
+                ensures self.foo_ens(a);
+        }
+
+        struct X { u: u64 }
+
+        struct Y { u: u64 }
+
+        impl Tr for X {
+            spec fn foo_req(&self) -> bool;
+            spec fn foo_ens(&self, a: Self) -> bool;
+
+            fn foo(&self) -> Self {
+                assume(false);
+                X { u: 0 }
+            }
+        }
+
+        impl Tr for Y {
+            spec fn foo_req(&self) -> bool;
+            spec fn foo_ens(&self, a: Self) -> bool;
+
+            fn foo(&self) -> (res: Self)
+                ensures res.u == 0
+            {
+                assume(false);
+                Y { u: 0 }
+            }
+        }
+
+        fn test_generic<T: Tr>(x: &T) {
+            assume(call_requires(T::foo, (x,)));
+            let r = x.foo();
+            assert(call_ensures(T::foo, (x,), r));
+        }
+
+        fn test_x(x: &X) {
+            assume(call_requires(X::foo, (x,)));
+            let r = x.foo();
+            assert(call_ensures(X::foo, (x,), r));
+        }
+
+        fn test_y(y: &Y) {
+            assume(call_requires(Y::foo, (y,)));
+            let r = y.foo();
+            assert(call_ensures(Y::foo, (y,), r));
+        }
+
+        fn test_generic_fail<T: Tr>(x: &T) {
+            assume(call_requires(T::foo, (x,)));
+            let r = x.foo();
+            assert(call_ensures(T::foo, (x,), r));
+            assert(false); // FAILS
+        }
+
+        fn test_x_fail(x: &X) {
+            assume(call_requires(X::foo, (x,)));
+            let r = x.foo();
+            assert(call_ensures(X::foo, (x,), r));
+            assert(false); // FAILS
+        }
+
+        fn test_y_fail(y: &Y) {
+            assume(call_requires(Y::foo, (y,)));
+            let r = y.foo();
+            assert(call_ensures(Y::foo, (y,), r));
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 3)
+}
diff --git a/source/rust_verify_test/tests/match.rs b/source/rust_verify_test/tests/match.rs
index 13aa30f0ba..5596986eae 100644
--- a/source/rust_verify_test/tests/match.rs
+++ b/source/rust_verify_test/tests/match.rs
@@ -1218,3 +1218,67 @@ test_verify_one_file! {
     //} => Err(err) => assert_one_fails(err)
     } => Err(err) => assert_vir_error_msg(err, "Not supported: pattern containing both an or-pattern (|) and an if-guard")
 }
+
+test_verify_one_file! {
+    #[test] pattern_with_no_initializer verus_code! {
+        struct X { u: u32 }
+
+        struct B { b: bool, x: u32 }
+        struct B2 { b: B }
+
+        fn test1() {
+            let _: X;
+
+            let (_, _): (X, X);
+            let (mut a, mut b): (X, X);
+
+            a = X { u: 20 };
+            b = X { u: 23 };
+
+            let X { u: mut ur }: X;
+            ur = 20;
+            assert(ur == 20);
+        }
+
+        fn test2() {
+            let _: X;
+
+            let X { u: mut ur }: X;
+            ur = 20;
+            assert(false); // FAILS
+        }
+
+        fn test3() {
+            let _: X;
+
+            let (_, _): (X, X);
+            let (a, b): (X, X);
+
+            assert(false); // FAILS
+        }
+
+        fn test4() {
+            let B { b: true | false, x: mut y }: B;
+
+            y = 5;
+            assert(y == 5);
+
+            let B2 { b: B { b: true, x: mut x } | B { b: false, x: mut x } }: B2;
+            x = 5;
+            assert(x == 5);
+        }
+
+        fn test5() {
+            let B { b: true | false, x: mut y }: B;
+
+            y = 5;
+            assert(y == 5);
+
+            let B2 { b: B { b: true, x: mut x } | B { b: false, x: mut x } }: B2;
+            x = 5;
+            assert(x == 5);
+
+            assert(false); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 3)
+}
diff --git a/source/rust_verify_test/tests/never_type.rs b/source/rust_verify_test/tests/never_type.rs
index 6fe181c7da..c77c35050f 100644
--- a/source/rust_verify_test/tests/never_type.rs
+++ b/source/rust_verify_test/tests/never_type.rs
@@ -69,3 +69,36 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_spec_never_caught1 verus_code! {
+        spec fn make_never() -> !;
+        proof fn test() {
+            let x: ! = make_never();
+            let y: ! = make_never();
+            assert(x == y);
+            let tracked z = x; // FAILS
+            assert(false); // FAILS
+        }
+    } => Err(e) => assert_vir_error_msg(e, "never-to-any coercion is not allowed in spec mode")
+}
+
+test_verify_one_file! {
+    #[test] test_spec_never_caught2 verus_code! {
+        spec fn make_never() -> !;
+        proof fn test() {
+            let x: ! = make_never();
+            let y: ! = make_never();
+            let tracked t: ! = true; // FAILS
+        }
+    } => Err(e) => assert_rust_error_msg(e, "mismatched types")
+}
+
+test_verify_one_file! {
+    #[test] test_spec_never_caught3 verus_code! {
+        spec fn make_never() -> !;
+        fn test_exec() -> ! {
+            let ghost x = make_never();
+        }
+    } => Err(e) => assert_vir_error_msg(e, "never-to-any coercion is not allowed in spec mode")
+}
diff --git a/source/rust_verify_test/tests/regression.rs b/source/rust_verify_test/tests/regression.rs
index dbf79580ba..6f470f1ff0 100644
--- a/source/rust_verify_test/tests/regression.rs
+++ b/source/rust_verify_test/tests/regression.rs
@@ -1348,3 +1348,45 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file_with_options! {
+    #[test] verus_macro_in_impl_block_issue1461 ["--external-by-default"] => code! {
+        use vstd::prelude::*;
+
+        verus! {
+        pub struct MyStruct {}
+        }
+
+        impl MyStruct {
+            verus! {
+                proof fn unsound()
+                {
+                    assert(false); // FAILS
+                }
+            }
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_one_file_with_options! {
+    #[test] verus_macro_in_impl_block_issue1461_traits ["--external-by-default"] => code! {
+        use vstd::prelude::*;
+
+        verus! {
+            pub struct MyStruct {}
+
+            trait Tr {
+                fn unsound();
+            }
+        }
+
+        impl Tr for MyStruct {
+            verus! {
+                fn unsound()
+                {
+                    assert(false);
+                }
+            }
+        }
+    } => Err(err) => assert_vir_error_msg(err, "In order to verify any items of this trait impl, the entire impl must be verified. Try wrapping the entire impl in the `verus!` macro.")
+}
diff --git a/source/rust_verify_test/tests/sets.rs b/source/rust_verify_test/tests/sets.rs
index 03d19b67ab..255e8a7539 100644
--- a/source/rust_verify_test/tests/sets.rs
+++ b/source/rust_verify_test/tests/sets.rs
@@ -111,7 +111,7 @@ test_verify_one_file! {
 
         proof fn test() {
             let s: Set<nat> = set![9];
-            reveal_with_fuel(Set::fold, 10);
+            broadcast use fold::lemma_fold_insert, fold::lemma_fold_empty;
             assert(s.finite());
             assert(s.len() > 0);
             assert(s.fold(0, |p: nat, a: nat| p + a) == 9);
diff --git a/source/rust_verify_test/tests/std.rs b/source/rust_verify_test/tests/std.rs
index 5e1a4b215a..434d8e24ff 100644
--- a/source/rust_verify_test/tests/std.rs
+++ b/source/rust_verify_test/tests/std.rs
@@ -509,10 +509,9 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] derive_copy verus_code! {
-        // When an auto-derived impl is produce, it doesn't get the verus_macro attribute.
+        // When an auto-derived impl is produced, it doesn't get the verus_macro attribute.
         // However, this test case does not use --external-by-default, so verus will
-        // process the derived impls anyway. This currently causes verus to fail,
-        // but should probably be fixed.
+        // process the derived impls anyway.
 
         #[derive(Clone, Copy)]
         struct X {
@@ -523,12 +522,12 @@ test_verify_one_file! {
             let a = x;
             let b = x;
         }
-    } => Err(err) => assert_vir_error_msg(err, "let-pattern declaration must have an initializer")
+    } => Ok(())
 }
 
 test_verify_one_file_with_options! {
     #[test] derive_copy_external_by_default ["--external-by-default"] => verus_code! {
-        // When an auto-derived impl is produce, it doesn't get the verus_macro attribute.
+        // When an auto-derived impl is produced, it doesn't get the verus_macro attribute.
         // Since this test case uses --external-by-default, these derived impls do not
         // get processed.
 
diff --git a/source/rust_verify_test/tests/syntax_attr.rs b/source/rust_verify_test/tests/syntax_attr.rs
index e5e508e691..56b60959fa 100644
--- a/source/rust_verify_test/tests/syntax_attr.rs
+++ b/source/rust_verify_test/tests/syntax_attr.rs
@@ -4,11 +4,14 @@ mod common;
 use common::*;
 
 test_verify_one_file! {
-    #[test] verus_verify_basic_while code! {
-        #[verus_verify]
+    #[test] verus_verify_basic_while  code! {
+        #[verus_spec]
         fn test1() {
             let mut i = 0;
-            #[invariant(i <= 10)]
+            #[verus_spec(
+                invariant
+                    i <= 10
+            )]
             while i < 10
             {
                 i = i + 1;
@@ -20,27 +23,79 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] verus_verify_basic_loop code! {
-        #[verus_verify]
+        #[verus_spec]
         fn test1() {
             let mut i = 0;
-            #[invariant(i <= 10)]
-            #[invariant_except_break(i <= 9)]
-            #[ensures(i == 10)]
+            let mut ret = 0;
+            #[verus_spec(
+                invariant i <= 10,
+                invariant_except_break i <= 9,
+                ensures i == 10, ret == 10
+            )]
             loop
             {
                 i = i + 1;
                 if (i == 10) {
+                    ret = i;
                     break;
                 }
             }
-            proof!{assert(i == 10);}
+            proof!{assert(ret == 10);}
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] verus_verify_basic_for_loop_verus_spec  code! {
+        use vstd::prelude::*;
+        #[verus_spec(v =>
+            ensures
+                v.len() == n,
+                forall|i: int| 0 <= i < n ==> v[i] == i
+        )]
+        fn test_for_loop(n: u32) -> Vec<u32>
+        {
+            let mut v: Vec<u32> = Vec::new();
+            #[verus_spec(
+                invariant
+                    v@ =~= Seq::new(i as nat, |k| k as u32),
+            )]
+            for i in 0..n
+            {
+                v.push(i);
+            }
+            v
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] verus_verify_for_loop_verus_spec_naming_iter  code! {
+        use vstd::prelude::*;
+        #[verus_spec(v =>
+            ensures
+                v.len() == n,
+                forall|i: int| 0 <= i < n ==> v[i] == 0
+        )]
+        fn test(n: u32) -> Vec<u32>
+        {
+            let mut v: Vec<u32> = Vec::new();
+            #[verus_spec(iter =>
+                invariant
+                    v@ =~= Seq::new(iter.cur as nat, |k| 0u32),
+            )]
+            for _ in 0..n
+            {
+                v.push(0);
+            }
+            v
         }
     } => Ok(())
 }
 
 test_verify_one_file! {
     #[test] verus_verify_basic_while_fail1 code! {
-        #[verus_verify]
+        #[verus_spec]
         fn test1() {
             let mut i = 0;
             while i < 10 {
@@ -56,7 +111,10 @@ test_verify_one_file! {
         #[verus_verify]
         fn test1() {
             let mut i = 0;
-            #[invariant(i <= 10, false)]
+            #[verus_spec(
+                invariant
+                    i <= 10, false
+            )]
             while i < 10 {
                 i = i + 1;
             }
@@ -65,11 +123,12 @@ test_verify_one_file! {
 }
 
 test_verify_one_file! {
-    #[test] verus_verify_bad_loop_spec code! {
-        #[verus_verify]
-        #[invariant(true)]
+    #[test] verus_verify_invariant_on_func code! {
+        #[verus_spec(
+            invariant true
+        )]
         fn test1() {}
-    } => Err(err) => assert_any_vir_error_msg(err, "'verus_spec' attribute expected")
+    } => Err(err) => assert_any_vir_error_msg(err, "unexpected token")
 }
 
 test_verify_one_file! {
@@ -100,10 +159,13 @@ test_verify_one_file! {
 test_verify_one_file! {
     #[test] test_bad_macro_attributes_in_trait code!{
         trait SomeTrait {
-            #[ensures(true)]
+            #[verus_spec(
+                ensures
+                    true
+            )]
             type T;
         }
-    } => Err(err) => assert_custom_attr_error_msg(err, "Misuse of #[ensures()]")
+    } => Err(err) => assert_any_vir_error_msg(err, "Misuse of #[verus_spec]")
 }
 
 test_verify_one_file! {
diff --git a/source/rust_verify_test/tests/triggers.rs b/source/rust_verify_test/tests/triggers.rs
index e2bd080da9..075fb86b25 100644
--- a/source/rust_verify_test/tests/triggers.rs
+++ b/source/rust_verify_test/tests/triggers.rs
@@ -249,6 +249,19 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] test_arith_variables_with_same_names verus_code! {
+        // https://github.com/verus-lang/verus/issues/1447
+        spec fn a(x: int) -> bool;
+
+        proof fn p_() {
+            let ranking_pred = |n: int| a(n);
+            assert forall|n: int| #![trigger a(n)] a(n) by { } // FAILS
+            assert forall|n: int| #![trigger a(-n)] a(-n) by { }
+        }
+    } => Err(e) => assert_one_fails(e)
+}
+
 const TRIGGER_ON_LAMBDA_COMMON: &str = verus_code_str! {
     struct S { a: int, }
 
diff --git a/source/tools/line_count/src/main.rs b/source/tools/line_count/src/main.rs
index acce0df3ed..a5a608e0bd 100644
--- a/source/tools/line_count/src/main.rs
+++ b/source/tools/line_count/src/main.rs
@@ -536,10 +536,6 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_item_macro(self, i);
     }
 
-    fn visit_item_macro2(&mut self, i: &'ast syn_verus::ItemMacro2) {
-        syn_verus::visit::visit_item_macro2(self, i);
-    }
-
     fn visit_item_mod(&mut self, i: &'ast syn_verus::ItemMod) {
         let exit = self.item_attr_enter(&i.attrs);
         if i.content.is_none() {
@@ -621,10 +617,6 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_lifetime(self, i);
     }
 
-    fn visit_lifetime_def(&mut self, i: &'ast syn_verus::LifetimeDef) {
-        syn_verus::visit::visit_lifetime_def(self, i);
-    }
-
     fn visit_lit(&mut self, i: &'ast syn_verus::Lit) {
         syn_verus::visit::visit_lit(self, i);
     }
@@ -865,10 +857,6 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_meta_name_value(self, i);
     }
 
-    fn visit_method_turbofish(&mut self, i: &'ast syn_verus::MethodTurbofish) {
-        syn_verus::visit::visit_method_turbofish(self, i);
-    }
-
     fn visit_mode(&mut self, i: &'ast syn_verus::Mode) {
         syn_verus::visit::visit_mode(self, i);
     }
@@ -897,10 +885,6 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_mode_tracked(self, i);
     }
 
-    fn visit_nested_meta(&mut self, i: &'ast syn_verus::NestedMeta) {
-        syn_verus::visit::visit_nested_meta(self, i);
-    }
-
     fn visit_open(&mut self, i: &'ast syn_verus::Open) {
         syn_verus::visit::visit_open(self, i);
     }
@@ -920,42 +904,14 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_pat(self, i);
     }
 
-    fn visit_pat_box(&mut self, i: &'ast syn_verus::PatBox) {
-        syn_verus::visit::visit_pat_box(self, i);
-    }
-
     fn visit_pat_ident(&mut self, i: &'ast syn_verus::PatIdent) {
         syn_verus::visit::visit_pat_ident(self, i);
     }
 
-    fn visit_pat_lit(&mut self, i: &'ast syn_verus::PatLit) {
-        syn_verus::visit::visit_pat_lit(self, i);
-    }
-
-    fn visit_pat_macro(&mut self, i: &'ast syn_verus::PatMacro) {
-        syn_verus::visit::visit_pat_macro(self, i);
-    }
-
     fn visit_pat_or(&mut self, i: &'ast syn_verus::PatOr) {
         syn_verus::visit::visit_pat_or(self, i);
     }
 
-    fn visit_pat_path(&mut self, i: &'ast syn_verus::PatPath) {
-        syn_verus::visit::visit_pat_path(self, i);
-    }
-
-    fn visit_pat_range(&mut self, i: &'ast syn_verus::PatRange) {
-        syn_verus::visit::visit_pat_range(self, i);
-    }
-
-    fn visit_pat_reference(&mut self, i: &'ast syn_verus::PatReference) {
-        syn_verus::visit::visit_pat_reference(self, i);
-    }
-
-    fn visit_pat_rest(&mut self, i: &'ast syn_verus::PatRest) {
-        syn_verus::visit::visit_pat_rest(self, i);
-    }
-
     fn visit_pat_slice(&mut self, i: &'ast syn_verus::PatSlice) {
         syn_verus::visit::visit_pat_slice(self, i);
     }
@@ -992,10 +948,6 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_path_segment(self, i);
     }
 
-    fn visit_predicate_eq(&mut self, i: &'ast syn_verus::PredicateEq) {
-        syn_verus::visit::visit_predicate_eq(self, i);
-    }
-
     fn visit_predicate_lifetime(&mut self, i: &'ast syn_verus::PredicateLifetime) {
         syn_verus::visit::visit_predicate_lifetime(self, i);
     }
@@ -1081,8 +1033,13 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
                     }
                     return;
                 }
+                // let a = Ghost(...)
                 if let Some(right) = init {
-                    match &*right.1 {
+                    if right.diverge.is_some() {
+                        // the else branch of let
+                        warn("else branch in let currently not supported");
+                    }
+                    match &*right.expr {
                         syn_verus::Expr::Call(call_expr) => {
                             let syn_verus::ExprCall { attrs: _, func, paren_token: _, args: _ } =
                                 &*call_expr;
@@ -1139,7 +1096,7 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         syn_verus::visit::visit_trait_item_macro(self, i);
     }
 
-    fn visit_trait_item_method(&mut self, i: &'ast syn_verus::TraitItemFn) {
+    fn visit_trait_item_fn(&mut self, i: &'ast syn_verus::TraitItemFn) {
         let exit = self.item_attr_enter(&i.attrs);
         let content_code_kind = i.sig.mode.to_code_kind();
         let code_kind = self.mode_or_trusted(content_code_kind);
@@ -1151,7 +1108,7 @@ impl<'ast, 'f> syn_verus::visit::Visit<'ast> for Visitor<'f> {
         if let Some(default) = &i.default {
             self.visit_block(default);
         }
-        syn_verus::visit::visit_trait_item_method(self, i);
+        syn_verus::visit::visit_trait_item_fn(self, i);
         self.in_body = None;
         exit.exit(self);
     }
@@ -1215,7 +1172,7 @@ impl ItemAttrExit {
 impl<'f> Visitor<'f> {
     fn item_attr_enter(&mut self, attrs: &Vec<Attribute>) -> ItemAttrExit {
         for attr in attrs.iter() {
-            if let Ok(Meta::Path(path)) = attr.parse_meta() {
+            if let Meta::Path(path) = &attr.meta {
                 let mut path_iter = path.segments.iter();
                 match (path_iter.next(), path_iter.next(), path_iter.next()) {
                     (Some(first), Some(second), None)
@@ -1286,7 +1243,7 @@ impl<'f> Visitor<'f> {
                 }
             }
 
-            if attr.path.segments.first().map(|x| x.ident == "doc").unwrap_or(false) {
+            if attr.path().segments.first().map(|x| x.ident == "doc").unwrap_or(false) {
             } else {
                 self.mark(
                     &attr,
@@ -1494,8 +1451,8 @@ fn process_file(config: Rc<Config>, input_path: &std::path::Path) -> Result<File
         config: config.clone(),
     };
     for attr in file.attrs.iter() {
-        match attr.parse_meta() {
-            Ok(Meta::Path(path)) => {
+        match &attr.meta {
+            Meta::Path(path) => {
                 let mut path_iter = path.segments.iter();
                 match (path_iter.next(), path_iter.next()) {
                     (Some(first), Some(second))
@@ -1506,22 +1463,25 @@ fn process_file(config: Rc<Config>, input_path: &std::path::Path) -> Result<File
                     _ => {}
                 }
             }
-            Ok(Meta::List(MetaList { path, paren_token: _, nested })) => {
+            Meta::List(MetaList { path, delimiter: _, tokens: _ }) => {
                 let mut path_iter = path.segments.iter();
                 match (path_iter.next(), path_iter.next()) {
                     (Some(first), None) if first.ident == "cfg_attr" => {
+                        let nested = attr.parse_args_with(syn_verus::punctuated::Punctuated::<Meta, syn_verus::Token![,]>::parse_terminated)
+                            .map_err(|e| {
+                                dbg!(&e.span().start(), &e.span().end());
+                                format!("failed to parse attribute: {} {:?}", e, e.span())
+                            })?;
                         let mut nested_iter = nested.iter();
                         match (nested_iter.next(), nested_iter.next()) {
-                            (
-                                Some(syn_verus::NestedMeta::Meta(Meta::Path(first))),
-                                Some(syn_verus::NestedMeta::Meta(Meta::Path(second))),
-                            ) if first
-                                .segments
-                                .iter()
-                                .next()
-                                .as_ref()
-                                .map(|x| x.ident == "verus_keep_ghost")
-                                .unwrap_or(false) =>
+                            (Some(Meta::Path(first)), Some(Meta::Path(second)))
+                                if first
+                                    .segments
+                                    .iter()
+                                    .next()
+                                    .as_ref()
+                                    .map(|x| x.ident == "verus_keep_ghost")
+                                    .unwrap_or(false) =>
                             {
                                 let mut path_iter = second.segments.iter();
                                 match (path_iter.next(), path_iter.next()) {
@@ -1675,6 +1635,10 @@ fn process_file(config: Rc<Config>, input_path: &std::path::Path) -> Result<File
     Ok(file_stats)
 }
 
+fn warn(msg: &str) {
+    eprintln!("warning: {}", msg);
+}
+
 fn run(config: Config, deps_path: &std::path::Path) -> Result<(), String> {
     let config = Rc::new(config);
     let (root_path, files) = get_dependencies(deps_path)?;
diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs
index 4e3c6115d3..dc09fccabc 100644
--- a/source/vir/src/ast.rs
+++ b/source/vir/src/ast.rs
@@ -10,7 +10,6 @@ use crate::messages::{Message, Span};
 pub use air::ast::{Binder, Binders};
 use num_bigint::BigInt;
 use serde::{Deserialize, Serialize};
-use std::fmt::Display;
 use std::sync::Arc;
 use vir_macros::{to_node_impl, ToDebugSNode};
 
@@ -585,12 +584,6 @@ pub struct SpannedTyped<X> {
     pub x: X,
 }
 
-impl<X: Display> Display for SpannedTyped<X> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{}", self.x)
-    }
-}
-
 /// Patterns for match expressions
 pub type Pattern = Arc<SpannedTyped<PatternX>>;
 pub type Patterns = Arc<Vec<Pattern>>;
@@ -1280,21 +1273,6 @@ pub enum ArchWordBits {
     Exactly(u32),
 }
 
-impl ArchWordBits {
-    pub fn min_bits(&self) -> u32 {
-        match self {
-            ArchWordBits::Either32Or64 => 32,
-            ArchWordBits::Exactly(v) => *v,
-        }
-    }
-    pub fn num_bits(&self) -> Option<u32> {
-        match self {
-            ArchWordBits::Either32Or64 => None,
-            ArchWordBits::Exactly(v) => Some(*v),
-        }
-    }
-}
-
 #[derive(Clone, Debug, Serialize, Deserialize)]
 pub struct Arch {
     pub word_bits: ArchWordBits,
@@ -1327,16 +1305,3 @@ pub struct KrateX {
     /// Arch info
     pub arch: Arch,
 }
-
-impl FunctionKind {
-    pub(crate) fn inline_okay(&self) -> bool {
-        match self {
-            FunctionKind::Static | FunctionKind::TraitMethodImpl { .. } => true,
-            // We don't want to do inlining for MethodDecls. If a MethodDecl has a body,
-            // it's a *default* body, so we can't know for sure it hasn't been overridden.
-            FunctionKind::TraitMethodDecl { .. } | FunctionKind::ForeignTraitMethodImpl { .. } => {
-                false
-            }
-        }
-    }
-}
diff --git a/source/vir/src/ast_simplify.rs b/source/vir/src/ast_simplify.rs
index 525a2e1d40..d828b98103 100644
--- a/source/vir/src/ast_simplify.rs
+++ b/source/vir/src/ast_simplify.rs
@@ -234,6 +234,42 @@ fn pattern_to_exprs_rec(
     }
 }
 
+fn pattern_to_decls_with_no_initializer(pattern: &Pattern, stmts: &mut Vec<Stmt>) {
+    match &pattern.x {
+        PatternX::Wildcard(_) => {}
+        PatternX::Var { name, mutable } | PatternX::Binding { name, mutable, sub_pat: _ } => {
+            let v_patternx = PatternX::Var { name: name.clone(), mutable: *mutable };
+            let v_pattern = SpannedTyped::new(&pattern.span, &pattern.typ, v_patternx);
+            stmts.push(Spanned::new(
+                pattern.span.clone(),
+                StmtX::Decl {
+                    pattern: v_pattern,
+                    mode: Some(Mode::Exec), // mode doesn't matter anymore
+                    init: None,
+                    els: None,
+                },
+            ));
+
+            match &pattern.x {
+                PatternX::Binding { sub_pat, .. } => {
+                    pattern_to_decls_with_no_initializer(sub_pat, stmts);
+                }
+                _ => {}
+            }
+        }
+        PatternX::Constructor(_path, _variant, patterns) => {
+            for binder in patterns.iter() {
+                pattern_to_decls_with_no_initializer(&binder.a, stmts);
+            }
+        }
+        PatternX::Or(pat1, _pat2) => {
+            pattern_to_decls_with_no_initializer(&pat1, stmts);
+        }
+        PatternX::Expr(_) => {}
+        PatternX::Range(_, _) => {}
+    }
+}
+
 fn pattern_has_or(pattern: &Pattern) -> bool {
     match &pattern.x {
         PatternX::Wildcard(_) => false,
@@ -596,7 +632,11 @@ fn simplify_one_stmt(ctx: &GlobalCtx, state: &mut State, stmt: &Stmt) -> Result<
     match &stmt.x {
         StmtX::Decl { pattern, mode: _, init: None, els: None } => match &pattern.x {
             PatternX::Var { .. } => Ok(vec![stmt.clone()]),
-            _ => Err(error(&stmt.span, "let-pattern declaration must have an initializer")),
+            _ => {
+                let mut stmts: Vec<Stmt> = Vec::new();
+                pattern_to_decls_with_no_initializer(pattern, &mut stmts);
+                Ok(stmts)
+            }
         },
         StmtX::Decl { pattern, mode: _, init: Some(init), els }
             if !matches!(pattern.x, PatternX::Var { .. }) =>
diff --git a/source/vir/src/ast_util.rs b/source/vir/src/ast_util.rs
index ec249f303a..0bd132607c 100644
--- a/source/vir/src/ast_util.rs
+++ b/source/vir/src/ast_util.rs
@@ -75,6 +75,12 @@ impl fmt::Display for Mode {
     }
 }
 
+impl<X: fmt::Display> fmt::Display for SpannedTyped<X> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.x)
+    }
+}
+
 pub fn type_is_bool(typ: &Typ) -> bool {
     matches!(&**typ, TypX::Bool)
 }
@@ -908,6 +914,34 @@ impl<A: Clone> VarBinderX<A> {
     }
 }
 
+impl FunctionKind {
+    pub(crate) fn inline_okay(&self) -> bool {
+        match self {
+            FunctionKind::Static | FunctionKind::TraitMethodImpl { .. } => true,
+            // We don't want to do inlining for MethodDecls. If a MethodDecl has a body,
+            // it's a *default* body, so we can't know for sure it hasn't been overridden.
+            FunctionKind::TraitMethodDecl { .. } | FunctionKind::ForeignTraitMethodImpl { .. } => {
+                false
+            }
+        }
+    }
+}
+
+impl ArchWordBits {
+    pub fn min_bits(&self) -> u32 {
+        match self {
+            ArchWordBits::Either32Or64 => 32,
+            ArchWordBits::Exactly(v) => *v,
+        }
+    }
+    pub fn num_bits(&self) -> Option<u32> {
+        match self {
+            ArchWordBits::Either32Or64 => None,
+            ArchWordBits::Exactly(v) => Some(*v),
+        }
+    }
+}
+
 pub fn str_unique_var(s: &str, dis: crate::ast::VarIdentDisambiguate) -> VarIdent {
     VarIdent(Arc::new(s.to_string()), dis)
 }
diff --git a/source/vir/src/sst_elaborate.rs b/source/vir/src/sst_elaborate.rs
index 469e2bdfc3..46ddb1bfea 100644
--- a/source/vir/src/sst_elaborate.rs
+++ b/source/vir/src/sst_elaborate.rs
@@ -5,9 +5,10 @@ use crate::ast_to_sst_func::SstMap;
 use crate::context::Ctx;
 use crate::def::{unique_local, Spanned};
 use crate::messages::{error_with_label, warning, ToAny};
-use crate::sst::{BndX, CallFun, Exp, ExpX, FunctionSst, Stm, StmX, UniqueIdent};
+use crate::sst::{BndX, CallFun, Exp, ExpX, FuncCheckSst, FunctionSst, Stm, StmX, UniqueIdent};
 use crate::sst_visitor::{NoScoper, Rewrite, Visitor};
 use crate::triggers::build_triggers;
+use crate::visitor::Returner;
 use air::messages::Diagnostics;
 use std::collections::HashMap;
 use std::sync::Arc;
@@ -16,7 +17,7 @@ fn elaborate_one_exp<D: Diagnostics + ?Sized>(
     ctx: &Ctx,
     diagnostics: &D,
     fun_ssts: &HashMap<Fun, FunctionSst>,
-    is_native: &mut HashMap<VarIdent, bool>,
+    is_native: &mut Option<HashMap<VarIdent, bool>>,
     exp: &Exp,
 ) -> Result<Exp, VirErr> {
     match &exp.x {
@@ -69,8 +70,10 @@ fn elaborate_one_exp<D: Diagnostics + ?Sized>(
                     assert!(assert_by_vars.len() == bs.len());
                     for (x, b) in assert_by_vars.iter().zip(bs.iter()) {
                         let native = natives.contains(&b.name);
-                        if let Some(n) = is_native.insert(x.clone(), native) {
-                            assert!(n == native);
+                        if let Some(is_native) = is_native {
+                            if let Some(n) = is_native.insert(x.clone(), native) {
+                                assert!(n == native);
+                            }
                         }
                     }
                 }
@@ -146,7 +149,7 @@ struct ElaborateVisitor1<'a, 'b, 'c, D: Diagnostics> {
     ctx: &'a Ctx,
     diagnostics: &'b D,
     fun_ssts: &'c HashMap<Fun, FunctionSst>,
-    is_native: HashMap<VarIdent, bool>,
+    is_native: Option<HashMap<VarIdent, bool>>,
 }
 
 impl<'a, 'b, 'c, D: Diagnostics> Visitor<Rewrite, VirErr, NoScoper>
@@ -160,16 +163,40 @@ impl<'a, 'b, 'c, D: Diagnostics> Visitor<Rewrite, VirErr, NoScoper>
     fn visit_stm(&mut self, stm: &Stm) -> Result<Stm, VirErr> {
         self.visit_stm_rec(stm)
     }
+
+    fn visit_func_check(&mut self, def: &FuncCheckSst) -> Result<FuncCheckSst, VirErr> {
+        self.is_native = Some(HashMap::new());
+        let reqs = self.visit_exps(&def.reqs)?;
+        let post_condition = self.visit_postcondition(&def.post_condition)?;
+        let body = self.visit_stm(&def.body)?;
+        let local_decls =
+            Rewrite::map_vec(&def.local_decls, &mut |decl| self.visit_local_decl(decl))?;
+        let mask_set = self.visit_mask_set(&def.mask_set)?;
+        let unwind = self.visit_unwind(&def.unwind)?;
+        let is_native = self.is_native.take().expect("is_native");
+
+        let mut def = FuncCheckSst {
+            reqs: Arc::new(reqs),
+            post_condition: Arc::new(post_condition),
+            mask_set: Arc::new(mask_set),
+            unwind,
+            body,
+            local_decls: Arc::new(local_decls),
+            statics: def.statics.clone(),
+        };
+
+        rewrite_locals(&is_native, &mut def);
+
+        Ok(def)
+    }
 }
 
-impl<'a, 'b, 'c, D: Diagnostics> ElaborateVisitor1<'a, 'b, 'c, D> {
-    fn rewrite_locals(&self, function: &mut crate::sst::FuncCheckSst) {
-        for local in Arc::make_mut(&mut function.local_decls) {
-            use crate::sst::LocalDeclKind;
-            if matches!(local.kind, LocalDeclKind::AssertByVar { .. }) {
-                let native = self.is_native[&local.ident];
-                Arc::make_mut(local).kind = LocalDeclKind::AssertByVar { native };
-            }
+fn rewrite_locals(is_native: &HashMap<VarIdent, bool>, function: &mut crate::sst::FuncCheckSst) {
+    for local in Arc::make_mut(&mut function.local_decls) {
+        use crate::sst::LocalDeclKind;
+        if matches!(local.kind, LocalDeclKind::AssertByVar { .. }) {
+            let native = is_native[&local.ident];
+            Arc::make_mut(local).kind = LocalDeclKind::AssertByVar { native };
         }
     }
 }
@@ -194,20 +221,8 @@ pub(crate) fn elaborate_function1<'a, 'b, 'c, D: Diagnostics>(
     fun_ssts: &'c HashMap<Fun, FunctionSst>,
     function: &mut FunctionSst,
 ) -> Result<(), VirErr> {
-    let mut visitor = ElaborateVisitor1 { ctx, diagnostics, fun_ssts, is_native: HashMap::new() };
+    let mut visitor = ElaborateVisitor1 { ctx, diagnostics, fun_ssts, is_native: None };
     *function = visitor.visit_function(function)?;
-    let function_mut = Arc::make_mut(function);
-    if let Some(check) = &mut function_mut.x.exec_proof_check {
-        visitor.rewrite_locals(Arc::make_mut(check));
-    }
-    if let Some(check) = &mut function_mut.x.recommends_check {
-        visitor.rewrite_locals(Arc::make_mut(check));
-    }
-    if let Some(axioms) = &mut Arc::make_mut(&mut function_mut.x.axioms).spec_axioms {
-        if let Some(check) = &mut axioms.termination_check {
-            visitor.rewrite_locals(check);
-        }
-    }
 
     if function.x.axioms.proof_exec_axioms.is_some() {
         let typ_params = function.x.typ_params.clone();
diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs
index 18d59a99a7..fcf933cbf2 100644
--- a/source/vir/src/sst_to_air.rs
+++ b/source/vir/src/sst_to_air.rs
@@ -1547,6 +1547,14 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
     let expr_ctxt = &ExprCtxt::new();
     let result = match &stm.x {
         StmX::Call { fun, resolved_method, mode, typ_args: typs, args, split, dest, assert_id } => {
+            // When we emit the VCs for a call to `f`, we might also want these to include
+            // the generic conditions
+            // `call_requires(f, (args...))` and `call_ensures(f, (args...), ret)`
+            // We don't want to do this all the time though --- only when the generic
+            // FnDef types exist post-pruning.
+            let emit_generic_conditions = ctx.fndef_types.contains(fun);
+            let resolved_fun = resolved_method.clone().map(|r| r.0);
+
             assert!(split.is_none());
             let mut stmts: Vec<Stmt> = Vec::new();
             let func = &ctx.func_map[fun];
@@ -1564,13 +1572,29 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
             {
                 let f_req = prefix_requires(&fun_to_air_ident(&func.x.name));
 
-                let e_req = Arc::new(ExprX::Apply(f_req, req_args.clone()));
+                let mut e_req = Arc::new(ExprX::Apply(f_req, req_args.clone()));
+
+                if emit_generic_conditions {
+                    let generic_req_exp = crate::sst_util::sst_call_requires(
+                        ctx,
+                        &stm.span,
+                        fun,
+                        typs,
+                        func,
+                        &resolved_fun,
+                        args,
+                    );
+                    let generic_req_expr = exp_to_expr(ctx, &generic_req_exp, expr_ctxt)?;
+                    e_req = mk_implies(&mk_not(&generic_req_expr), &e_req);
+                }
+
                 let description =
                     match (ctx.checking_spec_preconditions(), &func.x.attrs.custom_req_err) {
                         (true, None) => "recommendation not met".to_string(),
                         (_, None) => crate::def::PRECONDITION_FAILURE.to_string(),
                         (_, Some(s)) => s.clone(),
                     };
+
                 let error = error(&stm.span, description);
                 let filter = Some(fun_to_air_ident(&func.x.name));
                 stmts.push(Arc::new(StmtX::Assert(assert_id.clone(), error, filter, e_req)));
@@ -1758,6 +1782,8 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
                         let snapshot = Arc::new(StmtX::Snapshot(sid.clone()));
                         stmts.push(snapshot);
                     }
+                } else {
+                    crate::messages::internal_error(&stm.span, "ens_has_return but no Dest");
                 }
             }
             if has_ens {
@@ -1765,6 +1791,22 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
                 let e_ens = Arc::new(ExprX::Apply(f_ens, Arc::new(ens_args)));
                 stmts.push(Arc::new(StmtX::Assume(e_ens)));
             }
+            if emit_generic_conditions {
+                let dest_exp =
+                    if func.x.ens_has_return { Some(dest.clone().unwrap().dest) } else { None };
+                let generic_ens_exp = crate::sst_util::sst_call_ensures(
+                    ctx,
+                    &stm.span,
+                    fun,
+                    typs,
+                    func,
+                    &resolved_fun,
+                    args,
+                    dest_exp,
+                );
+                let generic_ens_expr = exp_to_expr(ctx, &generic_ens_exp, expr_ctxt)?;
+                stmts.push(Arc::new(StmtX::Assume(generic_ens_expr)));
+            }
             vec![Arc::new(StmtX::Block(Arc::new(stmts)))] // wrap in block for readability
         }
         StmX::Assert(assert_id, error, expr) => {
diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs
index 7a59093cc8..2276b9de0a 100644
--- a/source/vir/src/sst_util.rs
+++ b/source/vir/src/sst_util.rs
@@ -1,14 +1,16 @@
 use crate::ast::{
-    ArithOp, BinaryOp, BinaryOpr, BitwiseOp, Constant, CtorPrintStyle, Dt, Ident, InequalityOp,
-    IntRange, IntegerTypeBitwidth, IntegerTypeBoundKind, Mode, Quant, SpannedTyped, Typ, TypX,
-    Typs, UnaryOp, UnaryOpr, VarBinder, VarBinderX, VarBinders,
+    ArithOp, BinaryOp, BinaryOpr, BitwiseOp, Constant, CtorPrintStyle, Dt, Fun, Ident,
+    InequalityOp, IntRange, IntegerTypeBitwidth, IntegerTypeBoundKind, Mode, Quant, SpannedTyped,
+    Typ, TypX, Typs, UnaryOp, UnaryOpr, VarBinder, VarBinderX, VarBinders,
 };
 use crate::ast_util::{get_variant, unit_typ};
 use crate::context::GlobalCtx;
 use crate::def::{unique_bound, user_local_name, Spanned};
 use crate::interpreter::InterpExp;
 use crate::messages::Span;
-use crate::sst::{BndX, CallFun, Exp, ExpX, LocalDeclKind, Stm, Trig, Trigs, UniqueIdent};
+use crate::sst::{
+    BndX, CallFun, Exp, ExpX, Exps, InternalFun, LocalDeclKind, Stm, Trig, Trigs, UniqueIdent,
+};
 use air::scope_map::ScopeMap;
 use std::collections::HashMap;
 use std::sync::Arc;
@@ -812,3 +814,103 @@ pub fn sst_unpack_tuple_style_ctor(expx: &ExpX) -> Option<Vec<Exp>> {
         _ => None,
     }
 }
+
+pub fn sst_tuple(span: &Span, exps: &Exps) -> Exp {
+    let typs = crate::util::vec_map(exps, |e| e.typ.clone());
+    let tup_typ = crate::ast_util::mk_tuple_typ(&Arc::new(typs));
+    SpannedTyped::new(span, &tup_typ, sst_tuple_x(exps))
+}
+
+pub fn sst_tuple_x(exps: &Exps) -> ExpX {
+    let arity = exps.len();
+
+    let mut binders: Vec<crate::ast::Binder<Exp>> = Vec::new();
+    for (i, arg) in exps.iter().enumerate() {
+        let field = crate::def::positional_field_ident(i);
+        binders.push(crate::ast_util::ident_binder(&field, &arg));
+    }
+    let binders = Arc::new(binders);
+
+    ExpX::Ctor(Dt::Tuple(arity), crate::def::prefix_tuple_variant(arity), binders)
+}
+
+pub(crate) fn sst_call_requires(
+    ctx: &crate::context::Ctx,
+    span: &Span,
+    fun: &Fun,
+    typ_args: &Typs,
+    func: &crate::ast::Function,
+    resolved_fun: &Option<Fun>,
+    req_args: &Exps,
+) -> Exp {
+    let mut typ_substs: HashMap<Ident, Typ> = HashMap::new();
+    assert!(func.x.typ_params.len() == typ_args.len());
+    for (typ_param, arg) in func.x.typ_params.iter().zip(typ_args.iter()) {
+        typ_substs.insert(typ_param.clone(), arg.clone());
+    }
+    let param_typs: Vec<Typ> =
+        func.x.params.iter().map(|p| subst_typ(&typ_substs, &p.x.typ)).collect();
+
+    let tuple_typ = crate::ast_util::mk_tuple_typ(&Arc::new(param_typs));
+    let fndef_typ = Arc::new(TypX::FnDef(fun.clone(), typ_args.clone(), resolved_fun.clone()));
+
+    let fndef_value = SpannedTyped::new(span, &fndef_typ, ExpX::ExecFnByName(fun.clone()));
+    let fndef_value = crate::poly::coerce_exp_to_poly(ctx, &fndef_value);
+
+    let req_args: Vec<Exp> =
+        req_args.iter().map(|r| crate::poly::coerce_exp_to_poly(ctx, r)).collect();
+    let args_tuple = sst_tuple(span, &Arc::new(req_args));
+    let args_tuple = crate::poly::coerce_exp_to_poly(ctx, &args_tuple);
+
+    let expx = ExpX::Call(
+        CallFun::InternalFun(InternalFun::ClosureReq),
+        Arc::new(vec![fndef_typ, tuple_typ]),
+        Arc::new(vec![fndef_value, args_tuple]),
+    );
+    SpannedTyped::new(span, &Arc::new(TypX::Bool), expx)
+}
+
+pub(crate) fn sst_call_ensures(
+    ctx: &crate::context::Ctx,
+    span: &Span,
+    fun: &Fun,
+    typ_args: &Typs,
+    func: &crate::ast::Function,
+    resolved_fun: &Option<Fun>,
+    req_args: &Exps,
+    return_value: Option<Exp>,
+) -> Exp {
+    let mut typ_substs: HashMap<Ident, Typ> = HashMap::new();
+    assert!(func.x.typ_params.len() == typ_args.len());
+    for (typ_param, arg) in func.x.typ_params.iter().zip(typ_args.iter()) {
+        typ_substs.insert(typ_param.clone(), arg.clone());
+    }
+    let param_typs: Vec<Typ> =
+        func.x.params.iter().map(|p| subst_typ(&typ_substs, &p.x.typ)).collect();
+
+    let tuple_typ = crate::ast_util::mk_tuple_typ(&Arc::new(param_typs));
+    let fndef_typ = Arc::new(TypX::FnDef(fun.clone(), typ_args.clone(), resolved_fun.clone()));
+
+    let fndef_value = SpannedTyped::new(span, &fndef_typ, ExpX::ExecFnByName(fun.clone()));
+    let fndef_value = crate::poly::coerce_exp_to_poly(ctx, &fndef_value);
+
+    let req_args: Vec<Exp> =
+        req_args.iter().map(|r| crate::poly::coerce_exp_to_poly(ctx, r)).collect();
+    let args_tuple = sst_tuple(span, &Arc::new(req_args));
+    let args_tuple = crate::poly::coerce_exp_to_poly(ctx, &args_tuple);
+
+    let return_value = match &return_value {
+        Some(r) => crate::poly::coerce_exp_to_poly(ctx, r),
+        None => {
+            let unit = sst_tuple(span, &Arc::new(vec![]));
+            crate::poly::coerce_exp_to_poly(ctx, &unit)
+        }
+    };
+
+    let expx = ExpX::Call(
+        CallFun::InternalFun(InternalFun::ClosureEns),
+        Arc::new(vec![fndef_typ, tuple_typ]),
+        Arc::new(vec![fndef_value, args_tuple, return_value]),
+    );
+    SpannedTyped::new(span, &Arc::new(TypX::Bool), expx)
+}
diff --git a/source/vstd/arithmetic/mod.rs b/source/vstd/arithmetic/mod.rs
index 61a1b65a38..32d166606f 100644
--- a/source/vstd/arithmetic/mod.rs
+++ b/source/vstd/arithmetic/mod.rs
@@ -3,5 +3,6 @@ mod internals;
 pub mod div_mod;
 pub mod logarithm;
 pub mod mul;
+pub mod overflow;
 pub mod power;
 pub mod power2;
diff --git a/source/vstd/arithmetic/overflow.rs b/source/vstd/arithmetic/overflow.rs
new file mode 100644
index 0000000000..e7499e3856
--- /dev/null
+++ b/source/vstd/arithmetic/overflow.rs
@@ -0,0 +1,307 @@
+/// This file defines structs `CheckedU8`, `CheckedU16`, etc. and
+/// their associated methods to handle `u8`, `u16`, etc. values that
+/// can overflow. Each struct includes a ghost value representing the
+/// true value (not subject to overflow), so that the `view` function
+/// can provide the true value.
+///
+/// It's a fully verified library, i.e., it contains no trusted code.
+///
+/// Here are some examples using `CheckedU64`. (See
+/// `rust_verify/example/overflow.rs` for more examples, including
+/// ones for the analogous `CheckedU32`.)
+///
+/// ```
+/// fn test1()
+/// {
+///     let w = CheckedU64::new(0xFFFFFFFFFFFFFFFF);
+///     let x = w.add_value(1);
+///     assert(x.is_overflowed());
+///     assert(x.view() == 0x10000000000000000);
+///
+///     let y = CheckedU64::new(0x8000000000000000);
+///     let z = y.mul_value(2);
+///     assert(z.is_overflowed());
+///     assert(z.view() == 0x10000000000000000);
+/// }
+///
+/// fn test2(a: u64, b: u64, c: u64, d: u64) -> (e: Option<u64>)
+///     ensures
+///         match e {
+///             Some(v) => v == a * b + c * d,
+///             None => a * b + c * d > u64::MAX,
+///         }
+/// {
+///     let a_times_b = CheckedU64::new(a).mul_value(b);
+///     let c_times_d = CheckedU64::new(c).mul_value(d);
+///     let sum_of_products = a_times_b.add_checked(&c_times_d);
+///     if sum_of_products.is_overflowed() {
+///         assert(a * b + c * d > u64::MAX);
+///         None
+///     }
+///     else {
+///         let i: u64 = sum_of_products.unwrap();
+///         assert(i == a * b + c * d);
+///         Some(i)
+///     }
+/// }
+/// ```
+#[allow(unused_imports)]
+use super::super::prelude::*;
+#[allow(unused_imports)]
+use super::super::view::View;
+#[allow(unused_imports)]
+#[cfg(verus_keep_ghost)]
+use super::mul::{lemma_mul_by_zero_is_zero, lemma_mul_inequality, lemma_mul_is_commutative};
+#[allow(unused_imports)]
+use super::*;
+macro_rules! checked_uint_gen {
+    // This macro should be instantiated with the following parameters:
+    //
+    // $uty - The name of the `std` unsigned integer, e.g., `u64`
+    // $cty - The name of the checked struct to create, e.g., `CheckedU64`
+    ($uty: ty, $cty: ty) => {
+        verus! {
+
+            /// This struct represents a `$uty` value that can overflow. The `i` field
+            /// is a ghost value that represents the true value, while the `v` field
+            /// is `None` when the value has overflowed and `Some(x)` when the value
+            /// `x` fits in a `$uty`.
+            pub struct $cty {
+                i: Ghost<nat>,
+                v: Option<$uty>,
+            }
+
+            /// The view of an `$cty` instance is the true value of the instance.
+            impl View for $cty
+            {
+                type V = nat;
+
+                closed spec fn view(&self) -> nat
+                {
+                    self.i@
+                }
+            }
+
+            impl Clone for $cty {
+                /// Clones the `$cty` instance.
+                /// Ensures the cloned instance has the same value as the original.
+                exec fn clone(&self) -> (result: Self)
+                    ensures
+                        result@ == self@
+                {
+                    proof { use_type_invariant(self); }
+                    Self{ i: self.i, v: self.v }
+                }
+            }
+
+            impl $cty {
+                /// This is the internal type invariant for an `$cty`.
+                /// It ensures the key invariant that relates `i` and `v`.
+                #[verifier::type_invariant]
+                spec fn well_formed(self) -> bool
+                {
+                    match self.v {
+                        Some(v) => self.i@ == v,
+                        None => self.i@ > $uty::MAX,
+                    }
+                }
+
+                /// Creates a new `$cty` instance from a `$uty` value.
+                /// Ensures the internal representation matches the provided value.
+                pub closed spec fn spec_new(v: $uty) -> $cty
+                {
+                    $cty{ i: Ghost(v as nat), v: Some(v) }
+                }
+
+                /// Creates a new `$cty` instance from a `$uty` value.
+                /// Ensures the internal representation matches the provided value.
+                #[verifier::when_used_as_spec(spec_new)]
+                pub exec fn new(v: $uty) -> (result: Self)
+                    ensures
+                        result@ == v,
+                {
+                    Self{ i: Ghost(v as nat), v: Some(v) }
+                }
+
+                /// Creates a new `$cty` instance with an overflowed value.
+                /// Requires the provided value to be greater than `$uty::MAX`.
+                /// Ensures the internal representation matches the provided value.
+                pub exec fn new_overflowed(Ghost(i): Ghost<int>) -> (result: Self)
+                    requires
+                        i > $uty::MAX,
+                    ensures
+                        result@ == i,
+                {
+                    Self{ i: Ghost(i as nat), v: None }
+                }
+
+                /// Checks if the `$cty` instance is overflowed.
+                /// Returns true if the value is greater than `$uty::MAX`.
+                pub open spec fn spec_is_overflowed(&self) -> bool
+                {
+                    self@ > $uty::MAX
+                }
+
+                /// Checks if the `$cty` instance is overflowed.
+                /// Returns true if the value is greater than `$uty::MAX`.
+                #[verifier::when_used_as_spec(spec_is_overflowed)]
+                pub exec fn is_overflowed(&self) -> (result: bool)
+                    ensures
+                        result == self.spec_is_overflowed()
+                {
+                    proof { use_type_invariant(self) }
+                    self.v.is_none()
+                }
+
+                /// Unwraps the `$cty` instance to get the `$uty` value.
+                /// Requires the instance to not be overflowed.
+                /// Ensures the returned value matches the internal representation.
+                pub exec fn unwrap(&self) -> (result: $uty)
+                    requires
+                        !self.is_overflowed(),
+                    ensures
+                        result == self@,
+                {
+                    proof { use_type_invariant(self) }
+                    self.v.unwrap()
+                }
+
+                /// Converts the `$cty` instance to an `Option<$uty>`.
+                /// Ensures the returned option matches the internal representation.
+                pub exec fn to_option(&self) -> (result: Option<$uty>)
+                    ensures
+                        match result {
+                            Some(v) => self@ == v && v <= $uty::MAX,
+                            None => self@ > $uty::MAX,
+                        }
+                {
+                    proof { use_type_invariant(self); }
+                    self.v
+                }
+
+                /// Adds a `$uty` value to the `$cty` instance.
+                /// Ensures the resulting value matches the sum of
+                /// the internal representation and the provided
+                /// value.
+                #[inline]
+                pub exec fn add_value(&self, v2: $uty) -> (result: Self)
+                    ensures
+                        result@ == self@ + v2,
+                {
+                    proof {
+                        use_type_invariant(&self);
+                    }
+                    let i: Ghost<nat> = Ghost((&self@ + v2) as nat);
+                    match self.v {
+                        Some(v1) => Self{ i, v: v1.checked_add(v2) },
+                        None => Self{ i, v: None },
+                    }
+                }
+
+                /// Adds another `$cty` instance to the current
+                /// instance. Ensures the resulting value matches
+                /// the sum of the internal representations of
+                /// both instances.
+                #[inline]
+                pub exec fn add_checked(&self, v2: &$cty) -> (result: Self)
+                    ensures
+                        result@ == self@ + v2@,
+                {
+                    proof {
+                        use_type_invariant(self);
+                        use_type_invariant(v2);
+                    }
+                    match v2.v {
+                        Some(n) => self.add_value(n),
+                        None => {
+                            let i: Ghost<nat> = Ghost((self@ + v2@) as nat);
+                            Self{ i, v: None }
+                        }
+                    }
+                }
+
+                /// Multiplies the `$cty` instance by a `$uty`
+                /// value. Ensures the resulting value matches the
+                /// product of the internal representation and the
+                /// provided value.
+                #[inline]
+                pub exec fn mul_value(&self, v2: $uty) -> (result: Self)
+                    ensures
+                        result@ == self@ as int * v2 as int,
+                {
+                    proof {
+                        use_type_invariant(self);
+                    }
+                    let i: Ghost<nat> = Ghost((self@ * v2) as nat);
+                    match self.v {
+                        Some(n1) => Self{ i, v: n1.checked_mul(v2) },
+                        None => {
+                            if v2 == 0 {
+                                assert(i@ == 0) by {
+                                    lemma_mul_by_zero_is_zero(self@ as int);
+                                }
+                                Self{ i, v: Some(0) }
+                            }
+                            else {
+                                assert(self@ * v2 >= self@ * 1 == self@) by {
+                                    lemma_mul_inequality(1, v2 as int, self@ as int);
+                                    lemma_mul_is_commutative(self@ as int, v2 as int);
+                                }
+                                Self{ i, v: None }
+                            }
+                        },
+                    }
+                }
+
+                /// Multiplies the `$cty` instance by another `$cty` instance.
+                /// Ensures the resulting value matches the product of the internal
+                /// representations of both instances.
+                #[inline]
+                pub exec fn mul_checked(&self, v2: &Self) -> (result: Self)
+                    ensures
+                        result@ == self@ as int * v2@ as int,
+                {
+                    proof {
+                        use_type_invariant(self);
+                        use_type_invariant(v2);
+                    }
+                    let i: Ghost<nat> = Ghost((self@ * v2@) as nat);
+                    match v2.v {
+                        Some(n) => self.mul_value(n),
+                        None => {
+                            match self.v {
+                                Some(n1) => {
+                                    if n1 == 0 {
+                                        assert(i@ == 0) by {
+                                            lemma_mul_by_zero_is_zero(v2@ as int);
+                                        }
+                                        Self{ i, v: Some(0) }
+                                    }
+                                    else {
+                                        assert(self@ * v2@ >= 1 * v2@ == v2@) by {
+                                            lemma_mul_inequality(1, self@ as int, v2@ as int);
+                                        }
+                                        Self{ i, v: None }
+                                    }
+                                },
+                                None => {
+                                    assert(self@ * v2@ > $uty::MAX) by {
+                                        lemma_mul_inequality(1, self@ as int, v2@ as int);
+                                    }
+                                    Self{ i, v: None }
+                                },
+                            }
+                        }
+                    }
+                }
+            }
+        }
+    };
+}
+
+checked_uint_gen!(u8, CheckedU8);
+checked_uint_gen!(u16, CheckedU16);
+checked_uint_gen!(u32, CheckedU32);
+checked_uint_gen!(u64, CheckedU64);
+checked_uint_gen!(u128, CheckedU128);
+checked_uint_gen!(usize, CheckedUsize);
diff --git a/source/vstd/map.rs b/source/vstd/map.rs
index 1ce1f0c8fd..8dbae74605 100644
--- a/source/vstd/map.rs
+++ b/source/vstd/map.rs
@@ -41,13 +41,13 @@ impl<K, V> Map<K, V> {
 
     /// Gives a `Map<K, V>` whose domain contains every key, and maps each key
     /// to the value given by `fv`.
-    pub open spec fn total(fv: impl Fn(K) -> V) -> Map<K, V> {
+    pub open spec fn total(fv: spec_fn(K) -> V) -> Map<K, V> {
         Set::full().mk_map(fv)
     }
 
     /// Gives a `Map<K, V>` whose domain is given by the boolean predicate on keys `fk`,
     /// and maps each key to the value given by `fv`.
-    pub open spec fn new(fk: impl Fn(K) -> bool, fv: impl Fn(K) -> V) -> Map<K, V> {
+    pub open spec fn new(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V) -> Map<K, V> {
         Set::new(fk).mk_map(fv)
     }
 
diff --git a/source/vstd/multiset.rs b/source/vstd/multiset.rs
index 9560d24f0b..00268a01c6 100644
--- a/source/vstd/multiset.rs
+++ b/source/vstd/multiset.rs
@@ -653,7 +653,7 @@ pub proof fn lemma_multiset_properties<V>()
 
 }
 
-broadcast group group_multiset_properties {
+pub broadcast group group_multiset_properties {
     lemma_update_same,
     lemma_update_different,
     lemma_insert_containment,
diff --git a/source/vstd/set.rs b/source/vstd/set.rs
index 2dec920ede..e03fe2d6c8 100644
--- a/source/vstd/set.rs
+++ b/source/vstd/set.rs
@@ -1,5 +1,3 @@
-use core::marker;
-
 #[allow(unused_imports)]
 use super::map::*;
 #[allow(unused_imports)]
@@ -28,19 +26,29 @@ verus! {
 ///
 /// To prove that two sequences are equal, it is usually easiest to use the extensionality
 /// operator `=~=`.
-#[verifier::external_body]
 #[verifier::ext_equal]
 #[verifier::reject_recursive_types(A)]
 pub struct Set<A> {
-    dummy: marker::PhantomData<A>,
+    set: spec_fn(A) -> bool,
 }
 
 impl<A> Set<A> {
     /// The "empty" set.
-    pub spec fn empty() -> Set<A>;
+    pub closed spec fn empty() -> Set<A> {
+        Set { set: |a| false }
+    }
 
     /// Set whose membership is determined by the given boolean predicate.
-    pub spec fn new<F: Fn(A) -> bool>(f: F) -> Set<A>;
+    pub closed spec fn new(f: spec_fn(A) -> bool) -> Set<A> {
+        Set {
+            set: |a|
+                if f(a) {
+                    true
+                } else {
+                    false
+                },
+        }
+    }
 
     /// The "full" set, i.e., set containing every element of type `A`.
     pub open spec fn full() -> Set<A> {
@@ -48,7 +56,9 @@ impl<A> Set<A> {
     }
 
     /// Predicate indicating if the set contains the given element.
-    pub spec fn contains(self, a: A) -> bool;
+    pub closed spec fn contains(self, a: A) -> bool {
+        (self.set)(a)
+    }
 
     /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
     #[verifier::inline]
@@ -68,14 +78,34 @@ impl<A> Set<A> {
 
     /// Returns a new set with the given element inserted.
     /// If that element is already in the set, then an identical set is returned.
-    pub spec fn insert(self, a: A) -> Set<A>;
+    pub closed spec fn insert(self, a: A) -> Set<A> {
+        Set {
+            set: |a2|
+                if a2 == a {
+                    true
+                } else {
+                    (self.set)(a2)
+                },
+        }
+    }
 
     /// Returns a new set with the given element removed.
     /// If that element is already absent from the set, then an identical set is returned.
-    pub spec fn remove(self, a: A) -> Set<A>;
+    pub closed spec fn remove(self, a: A) -> Set<A> {
+        Set {
+            set: |a2|
+                if a2 == a {
+                    false
+                } else {
+                    (self.set)(a2)
+                },
+        }
+    }
 
     /// Union of two sets.
-    pub spec fn union(self, s2: Set<A>) -> Set<A>;
+    pub closed spec fn union(self, s2: Set<A>) -> Set<A> {
+        Set { set: |a| (self.set)(a) || (s2.set)(a) }
+    }
 
     /// `+` operator, synonymous with `union`
     #[verifier::inline]
@@ -84,7 +114,9 @@ impl<A> Set<A> {
     }
 
     /// Intersection of two sets.
-    pub spec fn intersect(self, s2: Set<A>) -> Set<A>;
+    pub closed spec fn intersect(self, s2: Set<A>) -> Set<A> {
+        Set { set: |a| (self.set)(a) && (s2.set)(a) }
+    }
 
     /// `*` operator, synonymous with `intersect`
     #[verifier::inline]
@@ -93,7 +125,9 @@ impl<A> Set<A> {
     }
 
     /// Set difference, i.e., the set of all elements in the first one but not in the second.
-    pub spec fn difference(self, s2: Set<A>) -> Set<A>;
+    pub closed spec fn difference(self, s2: Set<A>) -> Set<A> {
+        Set { set: |a| (self.set)(a) && !(s2.set)(a) }
+    }
 
     /// Set complement (within the space of all possible elements in `A`).
     /// `-` operator, synonymous with `difference`
@@ -102,18 +136,29 @@ impl<A> Set<A> {
         self.difference(s2)
     }
 
-    pub spec fn complement(self) -> Set<A>;
+    pub closed spec fn complement(self) -> Set<A> {
+        Set { set: |a| !(self.set)(a) }
+    }
 
     /// Set of all elements in the given set which satisfy the predicate `f`.
-    pub open spec fn filter<F: Fn(A) -> bool>(self, f: F) -> Set<A> {
+    pub open spec fn filter(self, f: spec_fn(A) -> bool) -> Set<A> {
         self.intersect(Self::new(f))
     }
 
     /// Returns `true` if the set is finite.
-    pub spec fn finite(self) -> bool;
+    pub closed spec fn finite(self) -> bool {
+        exists|f: spec_fn(A) -> nat, ub: nat|
+            {
+                &&& #[trigger] trigger_finite(f, ub)
+                &&& surj_on(f, self)
+                &&& forall|a| self.contains(a) ==> f(a) < ub
+            }
+    }
 
     /// Cardinality of the set. (Only meaningful if a set is finite.)
-    pub spec fn len(self) -> nat;
+    pub closed spec fn len(self) -> nat {
+        self.fold(0, |acc: nat, a| acc + 1)
+    }
 
     /// Chooses an arbitrary element of the set.
     ///
@@ -127,7 +172,7 @@ impl<A> Set<A> {
 
     /// Creates a [`Map`] whose domain is the given set.
     /// The values of the map are given by `f`, a function of the keys.
-    pub spec fn mk_map<V, F: Fn(A) -> V>(self, f: F) -> Map<A, V>;
+    pub closed spec fn mk_map<V>(self, f: spec_fn(A) -> V) -> Map<A, V>;
 
     /// Returns `true` if the sets are disjoint, i.e., if their interesection is
     /// the empty set.
@@ -136,13 +181,431 @@ impl<A> Set<A> {
     }
 }
 
-// Trusted axioms
+// Closures make triggering finicky but using this to trigger explicitly works well.
+spec fn trigger_finite<A>(f: spec_fn(A) -> nat, ub: nat) -> bool {
+    true
+}
+
+spec fn surj_on<A, B>(f: spec_fn(A) -> B, s: Set<A>) -> bool {
+    forall|a1, a2| #![all_triggers] s.contains(a1) && s.contains(a2) && a1 != a2 ==> f(a1) != f(a2)
+}
+
+pub mod fold {
+    //! This module defines a fold function for finite sets and proves a number of associated
+    //! lemmas.
+    //!
+    //! The module was ported (with some modifications) from Isabelle/HOL's finite set theory in:
+    //! `HOL/Finite_Set.thy`
+    //! That file contains the following author list:
+    //!
+    //!
+    //! (*  Title:      HOL/Finite_Set.thy
+    //!     Author:     Tobias Nipkow
+    //!     Author:     Lawrence C Paulson
+    //!     Author:     Markus Wenzel
+    //!     Author:     Jeremy Avigad
+    //!     Author:     Andrei Popescu
+    //! *)
+    //!
+    //!
+    //! The file is distributed under a 3-clause BSD license as indicated in the file `COPYRIGHT`
+    //! in Isabelle's root directory, which also carries the following copyright notice:
+    //!
+    //! Copyright (c) 1986-2024,
+    //! University of Cambridge,
+    //! Technische Universitaet Muenchen,
+    //! and contributors.
+    use super::*;
+
+    broadcast group group_set_axioms_early {
+        axiom_set_empty,
+        axiom_set_new,
+        axiom_set_insert_same,
+        axiom_set_insert_different,
+        axiom_set_remove_same,
+        axiom_set_remove_insert,
+        axiom_set_remove_different,
+        axiom_set_union,
+        axiom_set_intersect,
+        axiom_set_difference,
+        axiom_set_complement,
+        axiom_set_ext_equal,
+        axiom_set_ext_equal_deep,
+        axiom_set_empty_finite,
+        axiom_set_insert_finite,
+        axiom_set_remove_finite,
+    }
+
+    pub open spec fn is_fun_commutative<A, B>(f: spec_fn(B, A) -> B) -> bool {
+        forall|a1, a2, b| #[trigger] f(f(b, a2), a1) == f(f(b, a1), a2)
+    }
+
+    // This predicate is intended to be used like an inductive predicate, with the corresponding
+    // introduction, elimination and induction rules proved below.
+    #[verifier(opaque)]
+    spec fn fold_graph<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>, y: B, d: nat) -> bool
+        decreases d,
+    {
+        if s === Set::empty() {
+            &&& z == y
+            &&& d == 0
+        } else {
+            exists|yr, a|
+                {
+                    &&& #[trigger] trigger_fold_graph(yr, a)
+                    &&& d > 0
+                    &&& s.remove(a).finite()
+                    &&& s.contains(a)
+                    &&& fold_graph(z, f, s.remove(a), yr, sub(d, 1))
+                    &&& y == f(yr, a)
+                }
+        }
+    }
+
+    spec fn trigger_fold_graph<A, B>(yr: B, a: A) -> bool {
+        true
+    }
+
+    // Introduction rules
+    proof fn lemma_fold_graph_empty_intro<A, B>(z: B, f: spec_fn(B, A) -> B)
+        ensures
+            fold_graph(z, f, Set::empty(), z, 0),
+    {
+        reveal(fold_graph);
+    }
+
+    proof fn lemma_fold_graph_insert_intro<A, B>(
+        z: B,
+        f: spec_fn(B, A) -> B,
+        s: Set<A>,
+        y: B,
+        d: nat,
+        a: A,
+    )
+        requires
+            fold_graph(z, f, s, y, d),
+            !s.contains(a),
+        ensures
+            fold_graph(z, f, s.insert(a), f(y, a), d + 1),
+    {
+        broadcast use group_set_axioms_early;
+
+        reveal(fold_graph);
+        let _ = trigger_fold_graph(y, a);
+        assert(s == s.insert(a).remove(a));
+    }
+
+    // Elimination rules
+    proof fn lemma_fold_graph_empty_elim<A, B>(z: B, f: spec_fn(B, A) -> B, y: B, d: nat)
+        requires
+            fold_graph(z, f, Set::empty(), y, d),
+        ensures
+            z == y,
+            d == 0,
+    {
+        reveal(fold_graph);
+    }
+
+    proof fn lemma_fold_graph_insert_elim<A, B>(
+        z: B,
+        f: spec_fn(B, A) -> B,
+        s: Set<A>,
+        y: B,
+        d: nat,
+        a: A,
+    )
+        requires
+            is_fun_commutative(f),
+            fold_graph(z, f, s.insert(a), y, d),
+            !s.contains(a),
+        ensures
+            d > 0,
+            exists|yp| y == f(yp, a) && #[trigger] fold_graph(z, f, s, yp, sub(d, 1)),
+    {
+        reveal(fold_graph);
+        lemma_fold_graph_insert_elim_aux(z, f, s.insert(a), y, d, a);
+        assert(s.insert(a).remove(a) =~= s);
+        let yp = choose|yp| y == f(yp, a) && #[trigger] fold_graph(z, f, s, yp, sub(d, 1));
+    }
+
+    proof fn lemma_fold_graph_insert_elim_aux<A, B>(
+        z: B,
+        f: spec_fn(B, A) -> B,
+        s: Set<A>,
+        y: B,
+        d: nat,
+        a: A,
+    )
+        requires
+            is_fun_commutative(f),
+            fold_graph(z, f, s, y, d),
+            s.contains(a),
+        ensures
+            exists|yp| y == f(yp, a) && #[trigger] fold_graph(z, f, s.remove(a), yp, sub(d, 1)),
+        decreases d,
+    {
+        broadcast use group_set_axioms_early;
+
+        reveal(fold_graph);
+        let (yr, aa): (B, A) = choose|yr, aa|
+            #![all_triggers]
+            {
+                &&& trigger_fold_graph(yr, a)
+                &&& d > 0
+                &&& s.remove(aa).finite()
+                &&& s.contains(aa)
+                &&& fold_graph(z, f, s.remove(aa), yr, sub(d, 1))
+                &&& y == f(yr, aa)
+            };
+        assert(trigger_fold_graph(yr, a));
+        if s.remove(aa) === Set::empty() {
+        } else {
+            if a == aa {
+            } else {
+                lemma_fold_graph_insert_elim_aux(z, f, s.remove(aa), yr, sub(d, 1), a);
+                let yrp = choose|yrp|
+                    yr == f(yrp, a) && #[trigger] fold_graph(
+                        z,
+                        f,
+                        s.remove(aa).remove(a),
+                        yrp,
+                        sub(d, 2),
+                    );
+                assert(fold_graph(z, f, s.remove(aa).insert(aa).remove(a), f(yrp, aa), sub(d, 1)))
+                    by {
+                    assert(s.remove(aa).remove(a) == s.remove(aa).insert(aa).remove(a).remove(aa));
+                    assert(trigger_fold_graph(yrp, aa));
+                };
+            }
+        }
+    }
+
+    // Induction rule
+    proof fn lemma_fold_graph_induct<A, B>(
+        z: B,
+        f: spec_fn(B, A) -> B,
+        s: Set<A>,
+        y: B,
+        d: nat,
+        pred: spec_fn(Set<A>, B, nat) -> bool,
+    )
+        requires
+            is_fun_commutative(f),
+            fold_graph(z, f, s, y, d),
+            pred(Set::empty(), z, 0),
+            forall|a, s, y, d|
+                pred(s, y, d) && !s.contains(a) && #[trigger] fold_graph(z, f, s, y, d) ==> pred(
+                    #[trigger] s.insert(a),
+                    f(y, a),
+                    d + 1,
+                ),
+        ensures
+            pred(s, y, d),
+        decreases d,
+    {
+        broadcast use group_set_axioms_early;
+
+        reveal(fold_graph);
+        if s === Set::empty() {
+            lemma_fold_graph_empty_elim(z, f, y, d);
+        } else {
+            let a = s.choose();
+            lemma_fold_graph_insert_elim(z, f, s.remove(a), y, d, a);
+            let yp = choose|yp|
+                y == f(yp, a) && #[trigger] fold_graph(z, f, s.remove(a), yp, sub(d, 1));
+            lemma_fold_graph_induct(z, f, s.remove(a), yp, sub(d, 1), pred);
+        }
+    }
+
+    impl<A> Set<A> {
+        /// Folds the set, applying `f` to perform the fold. The next element for the fold is chosen by
+        /// the choose operator.
+        ///
+        /// Given a set `s = {x0, x1, x2, ..., xn}`, applying this function `s.fold(init, f)`
+        /// returns `f(...f(f(init, x0), x1), ..., xn)`.
+        pub closed spec fn fold<B>(self, z: B, f: spec_fn(B, A) -> B) -> B
+            recommends
+                self.finite(),
+                is_fun_commutative(f),
+        {
+            let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, self, y, d);
+            y
+        }
+    }
+
+    proof fn lemma_fold_graph_finite<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>, y: B, d: nat)
+        requires
+            is_fun_commutative(f),
+            fold_graph(z, f, s, y, d),
+        ensures
+            s.finite(),
+    {
+        broadcast use group_set_axioms_early;
+
+        let pred = |s: Set<A>, y, d| s.finite();
+        lemma_fold_graph_induct(z, f, s, y, d, pred);
+    }
+
+    proof fn lemma_fold_graph_deterministic<A, B>(
+        z: B,
+        f: spec_fn(B, A) -> B,
+        s: Set<A>,
+        y1: B,
+        y2: B,
+        d1: nat,
+        d2: nat,
+    )
+        requires
+            is_fun_commutative(f),
+            fold_graph(z, f, s, y1, d1),
+            fold_graph(z, f, s, y2, d2),
+        ensures
+            y1 == y2,
+            d1 == d2,
+    {
+        let pred = |s: Set<A>, y1: B, d1: nat|
+            forall|y2, d2| fold_graph(z, f, s, y2, d2) ==> y1 == y2 && d2 == d1;
+        // Base case
+        assert(pred(Set::empty(), z, 0)) by {
+            assert forall|y2, d2| fold_graph(z, f, Set::empty(), y2, d2) implies z == y2 && d2
+                == 0 by {
+                lemma_fold_graph_empty_elim(z, f, y2, d2);
+            };
+        };
+        // Step case
+        assert forall|a, s, y1, d1|
+            pred(s, y1, d1) && !s.contains(a) && #[trigger] fold_graph(
+                z,
+                f,
+                s,
+                y1,
+                d1,
+            ) implies pred(#[trigger] s.insert(a), f(y1, a), d1 + 1) by {
+            assert forall|y2, d2| fold_graph(z, f, s.insert(a), y2, d2) implies f(y1, a) == y2 && d2
+                == d1 + 1 by {
+                lemma_fold_graph_insert_elim(z, f, s, y2, d2, a);
+            };
+        };
+        lemma_fold_graph_induct(z, f, s, y2, d2, pred);
+    }
+
+    proof fn lemma_fold_is_fold_graph<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>, y: B, d: nat)
+        requires
+            is_fun_commutative(f),
+            fold_graph(z, f, s, y, d),
+        ensures
+            s.fold(z, f) == y,
+    {
+        lemma_fold_graph_finite(z, f, s, y, d);
+        if s.fold(z, f) != y {
+            let (y2, d2) = choose|y2, d2| fold_graph(z, f, s, y2, d2) && y2 != y;
+            lemma_fold_graph_deterministic(z, f, s, y2, y, d2, d);
+            assert(false);
+        }
+    }
+
+    // At this point set cardinality is not yet defined, so we can't easily give a decreasing
+    // measure to prove the subsequent lemma `lemma_fold_graph_exists`. Instead, we first prove
+    // this lemma, for which we use the upper bound of a finiteness witness as the decreasing
+    // measure.
+    pub proof fn lemma_finite_set_induct<A>(s: Set<A>, pred: spec_fn(Set<A>) -> bool)
+        requires
+            s.finite(),
+            pred(Set::empty()),
+            forall|s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)),
+        ensures
+            pred(s),
+    {
+        let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
+            trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub);
+        lemma_finite_set_induct_aux(s, f, ub, pred);
+    }
+
+    proof fn lemma_finite_set_induct_aux<A>(
+        s: Set<A>,
+        f: spec_fn(A) -> nat,
+        ub: nat,
+        pred: spec_fn(Set<A>) -> bool,
+    )
+        requires
+            surj_on(f, s),
+            s.finite(),
+            forall|a| s.contains(a) ==> f(a) < ub,
+            pred(Set::empty()),
+            forall|s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)),
+        ensures
+            pred(s),
+        decreases ub,
+    {
+        broadcast use group_set_axioms_early;
+
+        if s =~= Set::empty() {
+        } else {
+            let a = s.choose();
+            // If `f` maps something to `ub - 1`, remap it to `f(a)` so we can decrease ub
+            let fp = |aa|
+                if f(aa) == ub - 1 {
+                    f(a)
+                } else {
+                    f(aa)
+                };
+            lemma_finite_set_induct_aux(s.remove(a), fp, sub(ub, 1), pred);
+        }
+    }
+
+    proof fn lemma_fold_graph_exists<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>)
+        requires
+            s.finite(),
+            is_fun_commutative(f),
+        ensures
+            exists|y, d| fold_graph(z, f, s, y, d),
+    {
+        let pred = |s| exists|y, d| fold_graph(z, f, s, y, d);
+        // Base case
+        assert(fold_graph(z, f, Set::empty(), z, 0)) by {
+            lemma_fold_graph_empty_intro(z, f);
+        };
+        // Step case
+        assert forall|s, a| pred(s) && s.finite() && !s.contains(a) implies #[trigger] pred(
+            s.insert(a),
+        ) by {
+            let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, s, y, d);
+            lemma_fold_graph_insert_intro(z, f, s, y, d, a);
+        };
+        lemma_finite_set_induct(s, pred);
+    }
+
+    pub broadcast proof fn lemma_fold_insert<A, B>(s: Set<A>, z: B, f: spec_fn(B, A) -> B, a: A)
+        requires
+            s.finite(),
+            !s.contains(a),
+            is_fun_commutative(f),
+        ensures
+            #[trigger] s.insert(a).fold(z, f) == f(s.fold(z, f), a),
+    {
+        lemma_fold_graph_exists(z, f, s);
+        let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, s, y, d);
+        lemma_fold_graph_insert_intro(z, f, s, s.fold(z, f), d, a);
+        lemma_fold_is_fold_graph(z, f, s.insert(a), f(s.fold(z, f), a), d + 1);
+    }
+
+    pub broadcast proof fn lemma_fold_empty<A, B>(z: B, f: spec_fn(B, A) -> B)
+        ensures
+            #[trigger] Set::empty().fold(z, f) == z,
+    {
+        let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, Set::empty(), y, d);
+        lemma_fold_graph_empty_intro(z, f);
+        lemma_fold_graph_empty_elim(z, f, y, d);
+    }
+
+}
+
+// Axioms
 /// The empty set contains no elements
 pub broadcast proof fn axiom_set_empty<A>(a: A)
     ensures
         !(#[trigger] Set::empty().contains(a)),
 {
-    admit();
 }
 
 /// A call to `Set::new` with the predicate `f` contains `a` if and only if `f(a)` is true.
@@ -150,7 +613,6 @@ pub broadcast proof fn axiom_set_new<A>(f: spec_fn(A) -> bool, a: A)
     ensures
         #[trigger] Set::new(f).contains(a) == f(a),
 {
-    admit();
 }
 
 /// The result of inserting element `a` into set `s` must contains `a`.
@@ -158,7 +620,6 @@ pub broadcast proof fn axiom_set_insert_same<A>(s: Set<A>, a: A)
     ensures
         #[trigger] s.insert(a).contains(a),
 {
-    admit();
 }
 
 /// If `a1` does not equal `a2`, then the result of inserting element `a2` into set `s`
@@ -169,7 +630,6 @@ pub broadcast proof fn axiom_set_insert_different<A>(s: Set<A>, a1: A, a2: A)
     ensures
         #[trigger] s.insert(a2).contains(a1) == s.contains(a1),
 {
-    admit();
 }
 
 /// The result of removing element `a` from set `s` must not contain `a`.
@@ -177,7 +637,6 @@ pub broadcast proof fn axiom_set_remove_same<A>(s: Set<A>, a: A)
     ensures
         !(#[trigger] s.remove(a).contains(a)),
 {
-    admit();
 }
 
 /// Removing an element `a` from a set `s` and then inserting `a` back into the set`
@@ -218,7 +677,6 @@ pub broadcast proof fn axiom_set_remove_different<A>(s: Set<A>, a1: A, a2: A)
     ensures
         #[trigger] s.remove(a2).contains(a1) == s.contains(a1),
 {
-    admit();
 }
 
 /// The union of sets `s1` and `s2` contains element `a` if and only if
@@ -227,7 +685,6 @@ pub broadcast proof fn axiom_set_union<A>(s1: Set<A>, s2: Set<A>, a: A)
     ensures
         #[trigger] s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)),
 {
-    admit();
 }
 
 /// The intersection of sets `s1` and `s2` contains element `a` if and only if
@@ -236,7 +693,6 @@ pub broadcast proof fn axiom_set_intersect<A>(s1: Set<A>, s2: Set<A>, a: A)
     ensures
         #[trigger] s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)),
 {
-    admit();
 }
 
 /// The set difference between `s1` and `s2` contains element `a` if and only if
@@ -245,7 +701,6 @@ pub broadcast proof fn axiom_set_difference<A>(s1: Set<A>, s2: Set<A>, a: A)
     ensures
         #[trigger] s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)),
 {
-    admit();
 }
 
 /// The complement of set `s` contains element `a` if and only if `s` does not contain `a`.
@@ -253,7 +708,6 @@ pub broadcast proof fn axiom_set_complement<A>(s: Set<A>, a: A)
     ensures
         #[trigger] s.complement().contains(a) == !s.contains(a),
 {
-    admit();
 }
 
 /// Sets `s1` and `s2` are equal if and only if they contain all of the same elements.
@@ -261,14 +715,24 @@ pub broadcast proof fn axiom_set_ext_equal<A>(s1: Set<A>, s2: Set<A>)
     ensures
         #[trigger] (s1 =~= s2) <==> (forall|a: A| s1.contains(a) == s2.contains(a)),
 {
-    admit();
+    if s1 =~= s2 {
+        assert(forall|a: A| s1.contains(a) == s2.contains(a));
+    }
+    if forall|a: A| s1.contains(a) == s2.contains(a) {
+        if !(forall|a: A| #[trigger] (s1.set)(a) <==> (s2.set)(a)) {
+            assert(exists|a: A| #[trigger] (s1.set)(a) != (s2.set)(a));
+            let a = choose|a: A| #[trigger] (s1.set)(a) != (s2.set)(a);
+            assert(s1.contains(a));
+            assert(false);
+        }
+        assert(s1 =~= s2);
+    }
 }
 
 pub broadcast proof fn axiom_set_ext_equal_deep<A>(s1: Set<A>, s2: Set<A>)
     ensures
         #[trigger] (s1 =~~= s2) <==> s1 =~= s2,
 {
-    admit();
 }
 
 pub broadcast proof fn axiom_mk_map_domain<K, V>(s: Set<K>, f: spec_fn(K) -> V)
@@ -293,7 +757,9 @@ pub broadcast proof fn axiom_set_empty_finite<A>()
     ensures
         #[trigger] Set::<A>::empty().finite(),
 {
-    admit();
+    let f = |a: A| 0;
+    let ub = 0;
+    let _ = trigger_finite(f, ub);
 }
 
 /// The result of inserting an element `a` into a finite set `s` is also finite.
@@ -303,7 +769,34 @@ pub broadcast proof fn axiom_set_insert_finite<A>(s: Set<A>, a: A)
     ensures
         #[trigger] s.insert(a).finite(),
 {
-    admit();
+    let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
+        trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub);
+    let f2 = |a2: A|
+        if a2 == a {
+            ub
+        } else {
+            f(a2)
+        };
+    let ub2 = ub + 1;
+    let _ = trigger_finite(f2, ub2);
+    assert forall|a1, a2|
+        #![all_triggers]
+        s.insert(a).contains(a1) && s.insert(a).contains(a2) && a1 != a2 implies f2(a1) != f2(
+        a2,
+    ) by {
+        if a != a1 {
+            assert(s.contains(a1));
+        }
+        if a != a2 {
+            assert(s.contains(a2));
+        }
+    };
+    assert forall|a2| s.insert(a).contains(a2) implies #[trigger] f2(a2) < ub2 by {
+        if a == a2 {
+        } else {
+            assert(s.contains(a2));
+        }
+    };
 }
 
 /// The result of removing an element `a` from a finite set `s` is also finite.
@@ -313,7 +806,25 @@ pub broadcast proof fn axiom_set_remove_finite<A>(s: Set<A>, a: A)
     ensures
         #[trigger] s.remove(a).finite(),
 {
-    admit();
+    let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
+        trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub);
+    assert forall|a1, a2|
+        #![all_triggers]
+        s.remove(a).contains(a1) && s.remove(a).contains(a2) && a1 != a2 implies f(a1) != f(a2) by {
+        if a != a1 {
+            assert(s.contains(a1));
+        }
+        if a != a2 {
+            assert(s.contains(a2));
+        }
+    };
+    assert(surj_on(f, s.remove(a)));
+    assert forall|a2| s.remove(a).contains(a2) implies #[trigger] f(a2) < ub by {
+        if a == a2 {
+        } else {
+            assert(s.contains(a2));
+        }
+    };
 }
 
 /// The union of two finite sets is finite.
@@ -324,7 +835,21 @@ pub broadcast proof fn axiom_set_union_finite<A>(s1: Set<A>, s2: Set<A>)
     ensures
         #[trigger] s1.union(s2).finite(),
 {
-    admit();
+    let (f1, ub1) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
+        trigger_finite(f, ub) && surj_on(f, s1) && (forall|a| s1.contains(a) ==> f(a) < ub);
+    let (f2, ub2) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
+        trigger_finite(f, ub) && surj_on(f, s2) && (forall|a| s2.contains(a) ==> f(a) < ub);
+    let f3 = |a|
+        if s1.contains(a) {
+            f1(a)
+        } else {
+            ub1 + f2(a)
+        };
+    let ub3 = ub1 + ub2;
+    assert(trigger_finite(f3, ub3));
+    assert(forall|a|
+        #![all_triggers]
+        s1.union(s2).contains(a) ==> s1.contains(a) || s2.contains(a));
 }
 
 /// The intersection of two finite sets is finite.
@@ -334,7 +859,9 @@ pub broadcast proof fn axiom_set_intersect_finite<A>(s1: Set<A>, s2: Set<A>)
     ensures
         #[trigger] s1.intersect(s2).finite(),
 {
-    admit();
+    assert(forall|a|
+        #![all_triggers]
+        s1.intersect(s2).contains(a) ==> s1.contains(a) && s2.contains(a));
 }
 
 /// The set difference between two finite sets is finite.
@@ -344,7 +871,9 @@ pub broadcast proof fn axiom_set_difference_finite<A>(s1: Set<A>, s2: Set<A>)
     ensures
         #[trigger] s1.difference(s2).finite(),
 {
-    admit();
+    assert(forall|a|
+        #![all_triggers]
+        s1.difference(s2).contains(a) ==> s1.contains(a) && !s2.contains(a));
 }
 
 /// An infinite set `s` contains the element `s.choose()`.
@@ -354,7 +883,9 @@ pub broadcast proof fn axiom_set_choose_finite<A>(s: Set<A>)
     ensures
         #[trigger] s.contains(s.choose()),
 {
-    admit();
+    let f = |a: A| 0;
+    let ub = 0;
+    let _ = trigger_finite(f, ub);
 }
 
 // Trusted axioms about len
@@ -365,7 +896,7 @@ pub broadcast proof fn axiom_set_empty_len<A>()
     ensures
         #[trigger] Set::<A>::empty().len() == 0,
 {
-    admit();
+    fold::lemma_fold_empty(0, |b: nat, a: A| b + 1);
 }
 
 /// The result of inserting an element `a` into a finite set `s` has length
@@ -380,7 +911,11 @@ pub broadcast proof fn axiom_set_insert_len<A>(s: Set<A>, a: A)
             1
         }),
 {
-    admit();
+    if s.contains(a) {
+        assert(s =~= s.insert(a));
+    } else {
+        fold::lemma_fold_insert(s, 0, |b: nat, a: A| b + 1, a);
+    }
 }
 
 /// The result of removing an element `a` from a finite set `s` has length
@@ -395,7 +930,13 @@ pub broadcast proof fn axiom_set_remove_len<A>(s: Set<A>, a: A)
             0
         }),
 {
-    admit();
+    axiom_set_remove_finite(s, a);
+    axiom_set_insert_len(s.remove(a), a);
+    if s.contains(a) {
+        assert(s =~= s.remove(a).insert(a));
+    } else {
+        assert(s =~= s.remove(a));
+    }
 }
 
 /// If a finite set `s` contains any element, it has length greater than 0.
@@ -406,7 +947,11 @@ pub broadcast proof fn axiom_set_contains_len<A>(s: Set<A>, a: A)
     ensures
         #[trigger] s.len() != 0,
 {
-    admit();
+    let a = s.choose();
+    assert(s.remove(a).insert(a) =~= s);
+    axiom_set_remove_finite(s, a);
+    axiom_set_insert_finite(s.remove(a), a);
+    axiom_set_insert_len(s.remove(a), a);
 }
 
 /// A finite set `s` contains the element `s.choose()` if it has length greater than 0.
@@ -417,7 +962,14 @@ pub broadcast proof fn axiom_set_choose_len<A>(s: Set<A>)
     ensures
         #[trigger] s.contains(s.choose()),
 {
-    admit();
+    // Separate statements to work around https://github.com/verus-lang/verusfmt/issues/86
+    broadcast use axiom_set_contains_len;
+    broadcast use axiom_set_empty_len;
+    broadcast use axiom_set_ext_equal;
+    broadcast use axiom_set_insert_finite;
+
+    let pred = |s: Set<A>| s.finite() ==> s.len() == 0 <==> s =~= Set::empty();
+    fold::lemma_finite_set_induct(s, pred);
 }
 
 pub broadcast group group_set_axioms {
diff --git a/source/vstd/set_lib.rs b/source/vstd/set_lib.rs
index 4383da92db..bbf1421ab9 100644
--- a/source/vstd/set_lib.rs
+++ b/source/vstd/set_lib.rs
@@ -30,26 +30,6 @@ impl<A> Set<A> {
         Set::new(|a: B| exists|x: A| self.contains(x) && a == f(x))
     }
 
-    /// Folds the set, applying `f` to perform the fold. The next element for the fold is chosen by
-    /// the choose operator.
-    ///
-    /// Given a set `s = {x0, x1, x2, ..., xn}`, applying this function `s.fold(init, f)`
-    /// returns `f(...f(f(init, x0), x1), ..., xn)`.
-    pub open spec fn fold<E>(self, init: E, f: spec_fn(E, A) -> E) -> E
-        decreases self.len(),
-    {
-        if self.finite() {
-            if self.len() == 0 {
-                init
-            } else {
-                let a = self.choose();
-                self.remove(a).fold(f(init, a), f)
-            }
-        } else {
-            arbitrary()
-        }
-    }
-
     /// Converts a set into a sequence with an arbitrary ordering.
     pub open spec fn to_seq(self) -> Seq<A>
         recommends
diff --git a/source/vstd/tokens.rs b/source/vstd/tokens.rs
index 55ab4ad733..c7a3d74235 100644
--- a/source/vstd/tokens.rs
+++ b/source/vstd/tokens.rs
@@ -536,6 +536,7 @@ impl<Element, Token> MultisetToken<Element, Token>
             s.multiset() === Multiset::empty(),
     {
         let tracked s = Self { inst: instance_id, m: Map::tracked_empty(), _v: PhantomData, };
+        broadcast use super::set::fold::lemma_fold_empty;
         assert(Self::map_elems(Map::empty()) =~= Map::empty());
         return s;
     }
diff --git a/tools/veritas/run_configuration_all.toml b/tools/veritas/run_configuration_all.toml
index 3d84f63589..309a34368b 100644
--- a/tools/veritas/run_configuration_all.toml
+++ b/tools/veritas/run_configuration_all.toml
@@ -1,7 +1,7 @@
 verus_git_url = "https://github.com/verus-lang/verus.git"
 verus_revspec = "main"
 verus_features = ["singular"]
-verus_verify_vstd = false
+verus_verify_vstd = true
 
 [[project]]
 name = "memory-allocator"
@@ -27,7 +27,7 @@ name = "page-table"
 git_url = "https://github.com/utaal/verified-nrkernel.git"
 revspec = "main"
 crate_root = "page-table/src/lib.rs"
-extra_args = ["--crate-type=lib", "--rlimit", "60"]
+extra_args = ["--crate-type=lib", "--rlimit", "60", "--cfg", "feature=\"impl\""]
 
 [[project]]
 name = "verified-storage"