diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs
index 06cc7bda17b9..6985d4a60dee 100644
--- a/cprover_bindings/src/irep/serialize.rs
+++ b/cprover_bindings/src/irep/serialize.rs
@@ -57,7 +57,7 @@ impl Serialize for crate::goto_program::SymbolTable {
     }
 }
 struct StreamingSymbols<'a>(&'a crate::goto_program::SymbolTable);
-impl<'a> Serialize for StreamingSymbols<'a> {
+impl Serialize for StreamingSymbols<'_> {
     fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
     where
         S: Serializer,
@@ -92,7 +92,7 @@ impl<'de> serde::Deserialize<'de> for InternedString {
     }
 }
 
-impl<'de> serde::de::Visitor<'de> for InternedStringVisitor {
+impl serde::de::Visitor<'_> for InternedStringVisitor {
     type Value = InternedString;
 
     fn expecting(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 66d6e2eb1ab4..4fce3f7494b6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -107,7 +107,7 @@ impl PropertyClass {
     }
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Generates a CBMC assertion. Note: Does _NOT_ assume.
     pub fn codegen_assert(
         &self,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
index 1b28de887002..b5d537c9824a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
@@ -10,7 +10,7 @@ pub fn bb_label(bb: BasicBlockIdx) -> String {
     format!("bb{bb}")
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Generates Goto-C for a basic block.
     ///
     /// A MIR basic block consists of 0 or more statements followed by a terminator.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index 26caf29bea1d..254fc854e8b5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -12,7 +12,7 @@ use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::{Local, VarDebugInfoContents};
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
     /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
     /// for which it needs to be enforced.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
index 1a68533d3dce..169f2022a6e7 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
@@ -39,7 +39,7 @@ lazy_static! {
     };
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Generate the symbol and symbol table entry for foreign items.
     ///
     /// CBMC built-in functions that are supported by Kani are always added to the symbol table, and
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index eae547d58a4f..3b92dcdae876 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -15,7 +15,7 @@ use std::collections::BTreeMap;
 use tracing::{debug, debug_span};
 
 /// Codegen MIR functions into gotoc
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Declare variables according to their index.
     /// - Index 0 represents the return value.
     /// - Indices [1, N] represent the function parameters where N is the number of parameters.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 75fbfe4fc307..e8f566dafb15 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -28,7 +28,7 @@ enum VTableInfo {
     Align,
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     fn binop<F: FnOnce(Expr, Expr) -> Expr>(
         &mut self,
         place: &Place,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index fb1ddb76e3a2..ffe404c092c9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -224,7 +224,7 @@ impl TypeOrVariant {
     }
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Codegen field access for types that allow direct field projection.
     ///
     /// I.e.: Algebraic data types, closures, and coroutines.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index e5396468a1f3..779874f2ff77 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -29,7 +29,7 @@ use stable_mir::ty::{ClosureKind, IntTy, RigidTy, Size, Ty, TyConst, TyKind, Uin
 use std::collections::BTreeMap;
 use tracing::{debug, trace, warn};
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
         let left_op = self.codegen_operand_stable(e1);
         let right_op = self.codegen_operand_stable(e2);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index 41a3da11324b..00160a0db1a0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -31,7 +31,7 @@ lazy_static! {
          ("pointer-primitive", "disable:pointer-primitive-check")].iter().copied().collect();
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     pub fn codegen_span(&self, sp: &Span) -> Location {
         self.codegen_span_stable(rustc_internal::stable(sp))
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index e54f962336d0..ab02d54b2559 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -20,7 +20,7 @@ use stable_mir::mir::{
 use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Generate Goto-C for MIR [Statement]s.
     /// This does not cover all possible "statements" because MIR distinguishes between ordinary
     /// statements and [Terminator]s, which can exclusively appear at the end of a basic block.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
index a45c3a8d69a0..a89167741db1 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
@@ -9,7 +9,7 @@ use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, StaticDef};
 use tracing::debug;
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Ensures a static variable is initialized.
     ///
     /// Note that each static variable have their own location in memory. Per Rust documentation:
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index ae45a2456794..a2e52ac552c6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -91,7 +91,7 @@ impl TypeExt for Type {
 }
 
 /// Function signatures
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// This method prints the details of a GotoC type, for debugging purposes.
     #[allow(unused)]
     pub(crate) fn debug_print_type_recursively(&self, ty: &Type) -> String {
@@ -1615,7 +1615,7 @@ impl<'tcx> GotocCtx<'tcx> {
             pub ctx: &'a GotocCtx<'tcx>,
         }
 
-        impl<'tcx, 'a> Iterator for ReceiverIter<'tcx, 'a> {
+        impl<'tcx> Iterator for ReceiverIter<'tcx, '_> {
             type Item = (String, Ty<'tcx>);
 
             fn next(&mut self) -> Option<Self::Item> {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
index 246b6cd94b47..16877ff6c18d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -84,7 +84,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
 }
 
 /// Setters
-impl<'tcx> CurrentFnCtx<'tcx> {
+impl CurrentFnCtx<'_> {
     /// Returns the current block, replacing it with an empty vector.
     pub fn extract_block(&mut self) -> Vec<Stmt> {
         std::mem::take(&mut self.block)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 3a47f7b9c09c..176268022f34 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -119,7 +119,7 @@ impl<'tcx> GotocCtx<'tcx> {
 }
 
 /// Generate variables
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Declare a local variable.
     /// Handles the bookkeeping of:
     /// - creating the symbol
@@ -302,7 +302,7 @@ impl<'tcx> GotocCtx<'tcx> {
 }
 
 /// Mutators
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     pub fn set_current_fn(&mut self, instance: Instance, body: &Body) {
         self.current_fn = Some(CurrentFnCtx::new(instance, self, body));
     }
@@ -346,7 +346,7 @@ impl<'tcx> HasTyCtxt<'tcx> for GotocCtx<'tcx> {
     }
 }
 
-impl<'tcx> HasDataLayout for GotocCtx<'tcx> {
+impl HasDataLayout for GotocCtx<'_> {
     fn data_layout(&self) -> &TargetDataLayout {
         self.tcx.data_layout()
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
index 854ddf6baa57..39bc57fc7385 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
@@ -104,7 +104,7 @@ impl VtableCtx {
     }
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Create a label to the virtual call site
     pub fn virtual_call_with_restricted_fn_ptr(
         &mut self,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
index 01f5ca4b3dce..f30f79fed24d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -10,7 +10,7 @@ use rustc_middle::mir::mono::CodegenUnitNameBuilder;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::Local;
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// The full crate name including versioning info
     pub fn full_crate_name(&self) -> &str {
         &self.full_crate_name
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index faf1ed61dc2f..c9d4511d7453 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -19,7 +19,7 @@ pub fn dynamic_fat_ptr(typ: Type, data: Expr, vtable: Expr, symbol_table: &Symbo
     Expr::struct_expr(typ, btree_string_map![("data", data), ("vtable", vtable)], symbol_table)
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     pub fn unsupported_msg(item: &str, url: Option<&str>) -> String {
         let mut s = format!("{item} is not currently supported by Kani");
         if let Some(url) = url {
@@ -71,7 +71,7 @@ impl<'tcx> GotocCtx<'tcx> {
 /// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer).
 const RAW_PTR_FROM_BOX: [&str; 3] = ["0", "pointer", "pointer"];
 
-impl<'tcx> GotocCtx<'tcx> {
+impl GotocCtx<'_> {
     /// Dereference a boxed type `std::boxed::Box<T>` to get a `*T`.
     ///
     /// WARNING: This is based on a manual inspection of how boxed types are currently
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 630f818231c9..0085928a37d0 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -140,7 +140,7 @@ pub struct ContractAttributes {
     pub modifies_wrapper: Symbol,
 }
 
-impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> {
+impl std::fmt::Debug for KaniAttributes<'_> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         f.debug_struct("KaniAttributes")
             .field("item", &self.tcx.def_path_debug_str(self.item))
@@ -726,7 +726,7 @@ struct UnstableAttrParseError<'a> {
     attr: &'a Attribute,
 }
 
-impl<'a> UnstableAttrParseError<'a> {
+impl UnstableAttrParseError<'_> {
     /// Report the error in a friendly format.
     fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed {
         tcx.dcx()
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 224abef1b02b..ebef669e0f5d 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -189,7 +189,7 @@ impl<'tcx> CoerceUnsizedIterator<'tcx> {
 ///   dst_ty: Ty, // *const &dyn Debug
 /// }
 /// ```
-impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
+impl Iterator for CoerceUnsizedIterator<'_> {
     type Item = CoerceUnsizedInfo;
 
     fn next(&mut self) -> Option<Self::Item> {
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 5f7f4c28068f..5fead860320c 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -77,7 +77,7 @@ struct FindUnsafeCell<'tcx> {
     tcx: TyCtxt<'tcx>,
 }
 
-impl<'tcx> TyVisitor for FindUnsafeCell<'tcx> {
+impl TyVisitor for FindUnsafeCell<'_> {
     type Break = ();
     fn visit_ty(&mut self, ty: &Ty) -> ControlFlow<Self::Break> {
         match ty.kind() {
@@ -171,7 +171,7 @@ impl<'tcx> HasTyCtxt<'tcx> for CompilerHelpers<'tcx> {
     }
 }
 
-impl<'tcx> HasDataLayout for CompilerHelpers<'tcx> {
+impl HasDataLayout for CompilerHelpers<'_> {
     fn data_layout(&self) -> &TargetDataLayout {
         self.tcx.data_layout()
     }
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
index 040a925e140f..3ac2d02ae8fc 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
@@ -114,7 +114,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
     }
 }
 
-impl<'a, 'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'a, 'tcx> {
+impl<'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'_, 'tcx> {
     /// Dataflow state at each instruction.
     type Domain = PointsToGraph<'tcx>;
 
@@ -135,7 +135,7 @@ impl<'a, 'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'a, 'tcx> {
     }
 }
 
-impl<'a, 'tcx> Analysis<'tcx> for PointsToAnalysis<'a, 'tcx> {
+impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
     /// Update current dataflow state based on the information we can infer from the given
     /// statement.
     fn apply_statement_effect(
@@ -366,7 +366,7 @@ fn try_resolve_instance<'tcx>(
     }
 }
 
-impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
+impl<'tcx> PointsToAnalysis<'_, 'tcx> {
     /// Update the analysis state according to the operation, which is semantically equivalent to `*to = *from`.
     fn apply_copy_effect(
         &self,
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
index 4dd2fba62fb0..0b52a84eaa59 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
@@ -70,7 +70,7 @@ struct NodeData<'tcx> {
     ancestors: HashSet<MemLoc<'tcx>>,
 }
 
-impl<'tcx> NodeData<'tcx> {
+impl NodeData<'_> {
     /// Merge two instances of NodeData together, return true if the original one was updated and
     /// false otherwise.
     fn merge(&mut self, other: Self) -> bool {
@@ -232,7 +232,7 @@ impl<'tcx> PointsToGraph<'tcx> {
 /// join operation. In our case, this is a simple union of two graphs. This "lattice" is finite,
 /// because in the worst case all places will alias to all places, in which case the join will be a
 /// no-op.
-impl<'tcx> JoinSemiLattice for PointsToGraph<'tcx> {
+impl JoinSemiLattice for PointsToGraph<'_> {
     fn join(&mut self, other: &Self) -> bool {
         let mut updated = false;
         // Check every node in the other graph.
@@ -247,4 +247,4 @@ impl<'tcx> JoinSemiLattice for PointsToGraph<'tcx> {
 
 /// This is a requirement for the fixpoint solver, and there is no derive macro for this, so
 /// implement it manually.
-impl<'tcx, C> DebugWithContext<C> for PointsToGraph<'tcx> {}
+impl<C> DebugWithContext<C> for PointsToGraph<'_> {}
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 6f2e779320f3..b875694fd648 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -245,7 +245,7 @@ struct MonoItemsFnCollector<'a, 'tcx> {
     body: &'a Body,
 }
 
-impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
+impl MonoItemsFnCollector<'_, '_> {
     /// Collect the implementation of all trait methods and its supertrait methods for the given
     /// concrete type.
     fn collect_vtable_methods(&mut self, concrete_ty: Ty, trait_ty: Ty) {
@@ -350,7 +350,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
 /// 6. Static Initialization
 ///
 /// Remark: This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
-impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
+impl MirVisitor for MonoItemsFnCollector<'_, '_> {
     /// Collect the following:
     /// - Trait implementations when casting from concrete to dyn Trait.
     /// - Functions / Closures that have their address taken.
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 31cf55650559..bf2102208e6e 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -184,13 +184,13 @@ pub enum ResolveError<'tcx> {
     UnsupportedPath { kind: &'static str },
 }
 
-impl<'tcx> fmt::Debug for ResolveError<'tcx> {
+impl fmt::Debug for ResolveError<'_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         std::fmt::Display::fmt(self, f)
     }
 }
 
-impl<'tcx> fmt::Display for ResolveError<'tcx> {
+impl fmt::Display for ResolveError<'_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             ResolveError::ExtraSuper => {
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index 4a48c649983c..a348d285a28a 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -183,7 +183,7 @@ impl<'tcx> StubConstChecker<'tcx> {
     }
 }
 
-impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
+impl MirVisitor for StubConstChecker<'_> {
     /// Collect constants that are represented as static variables.
     fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
         let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.const_));
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
index 877ff41ea6d5..ea50654ddcec 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
@@ -35,7 +35,7 @@ pub struct InstrumentationVisitor<'a, 'tcx> {
     tcx: TyCtxt<'tcx>,
 }
 
-impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
+impl TargetFinder for InstrumentationVisitor<'_, '_> {
     fn find_all(mut self, body: &MutableBody) -> Vec<InitRelevantInstruction> {
         for (bb_idx, bb) in body.blocks().iter().enumerate() {
             self.current_target = InitRelevantInstruction {
@@ -75,7 +75,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
     }
 }
 
-impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> {
+impl MirVisitor for InstrumentationVisitor<'_, '_> {
     fn visit_statement(&mut self, stmt: &Statement, location: Location) {
         self.super_statement(stmt, location);
         // Switch to the next statement.
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index d0fd553ef5cf..80c20b5cb108 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -325,7 +325,7 @@ impl<'a, 'b> CheckValueVisitor<'a, 'b> {
     }
 }
 
-impl<'a, 'b> MirVisitor for CheckValueVisitor<'a, 'b> {
+impl MirVisitor for CheckValueVisitor<'_, '_> {
     fn visit_statement(&mut self, stmt: &Statement, location: Location) {
         if self.skip_next {
             self.skip_next = false;
diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs
index 09d6e1fe8520..ae9f77ba239d 100644
--- a/kani-compiler/src/kani_middle/transform/stubs.rs
+++ b/kani-compiler/src/kani_middle/transform/stubs.rs
@@ -139,7 +139,7 @@ struct FnStubValidator<'a, 'tcx> {
     is_valid: bool,
 }
 
-impl<'a, 'tcx> FnStubValidator<'a, 'tcx> {
+impl FnStubValidator<'_, '_> {
     fn validate(tcx: TyCtxt, stub: (FnDef, FnDef), new_instance: Instance) -> Option<Body> {
         if validate_stub_const(tcx, new_instance) {
             let body = new_instance.body().unwrap();
@@ -153,7 +153,7 @@ impl<'a, 'tcx> FnStubValidator<'a, 'tcx> {
     }
 }
 
-impl<'a, 'tcx> MirVisitor for FnStubValidator<'a, 'tcx> {
+impl MirVisitor for FnStubValidator<'_, '_> {
     fn visit_operand(&mut self, op: &Operand, loc: Location) {
         let op_ty = op.ty(self.locals).unwrap();
         if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = op_ty.kind() {
@@ -188,7 +188,7 @@ struct ExternFnStubVisitor<'a> {
     stubs: &'a Stubs,
 }
 
-impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
+impl MutMirVisitor for ExternFnStubVisitor<'_> {
     fn visit_terminator(&mut self, term: &mut Terminator) {
         // Replace direct calls
         if let TerminatorKind::Call { func, .. } = &mut term.kind {
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 8ef1ee153106..58a93df3a2f6 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -483,7 +483,7 @@ impl<'a, 'b> Parser<'a, 'b> {
 
 /// The iterator implementation for `Parser` reads the buffer line by line,
 /// and determines if it must return an item based on processing each line.
-impl<'a, 'b> Iterator for Parser<'a, 'b> {
+impl Iterator for Parser<'_, '_> {
     type Item = ParserItem;
     fn next(&mut self) -> Option<Self::Item> {
         loop {
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 5a77a6a125a3..32f184b3ce6a 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -29,7 +29,7 @@ pub(crate) struct HarnessResult<'pr> {
     pub result: VerificationResult,
 }
 
-impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
+impl<'pr> HarnessRunner<'_, 'pr> {
     /// Given a [`HarnessRunner`] (to abstract over how these harnesses were generated), this runs
     /// the proof-checking process for each harness in `harnesses`.
     pub(crate) fn check_all_harnesses(
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 7ef640dbfdc9..4618c3ffdca1 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-10-03"
+channel = "nightly-2024-10-04"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 1622dc104919..5439942b195e 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -68,7 +68,7 @@ struct TestCx<'test> {
     testpaths: &'test TestPaths,
 }
 
-impl<'test> TestCx<'test> {
+impl TestCx<'_> {
     /// Code executed
     fn run(&self) {
         match self.config.mode {
diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs
index e0f65929ffdd..744ca4aec9e5 100644
--- a/tools/scanner/src/analysis.rs
+++ b/tools/scanner/src/analysis.rs
@@ -313,7 +313,7 @@ struct TypeVisitor<'a> {
     visited: HashSet<Ty>,
 }
 
-impl<'a> TypeVisitor<'a> {
+impl TypeVisitor<'_> {
     pub fn visit_variants(&mut self, def: AdtDef, _args: &GenericArgs) -> ControlFlow<()> {
         for variant in def.variants_iter() {
             for field in variant.fields() {
@@ -324,7 +324,7 @@ impl<'a> TypeVisitor<'a> {
     }
 }
 
-impl<'a> Visitor for TypeVisitor<'a> {
+impl Visitor for TypeVisitor<'_> {
     type Break = ();
 
     fn visit_ty(&mut self, ty: &Ty) -> ControlFlow<Self::Break> {
@@ -413,7 +413,7 @@ struct BodyVisitor<'a> {
     body: &'a Body,
 }
 
-impl<'a> MirVisitor for BodyVisitor<'a> {
+impl MirVisitor for BodyVisitor<'_> {
     fn visit_terminator(&mut self, term: &Terminator, location: Location) {
         match &term.kind {
             TerminatorKind::Call { func, .. } => {
@@ -501,7 +501,7 @@ struct IteratorVisitor<'a> {
     current_bbidx: u32,
 }
 
-impl<'a> MirVisitor for IteratorVisitor<'a> {
+impl MirVisitor for IteratorVisitor<'_> {
     fn visit_body(&mut self, body: &Body) {
         // First visit the body to build the control flow graph
         self.super_body(body);
@@ -677,7 +677,7 @@ struct FnCallVisitor<'a> {
     fns: Vec<FnDef>,
 }
 
-impl<'a> MirVisitor for FnCallVisitor<'a> {
+impl MirVisitor for FnCallVisitor<'_> {
     fn visit_terminator(&mut self, term: &Terminator, location: Location) {
         if let TerminatorKind::Call { func, .. } = &term.kind {
             let kind = func.ty(self.body.locals()).unwrap().kind();