diff --git a/.cargo/config.toml b/.cargo/config.toml
index 9bb4e0808345..f0df939ef506 100644
--- a/.cargo/config.toml
+++ b/.cargo/config.toml
@@ -20,6 +20,8 @@ KANI_SYSROOT ={value = "target/kani", relative = true}
 KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
 # Build Kani library without `build-std`.
 KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
+# This is only required for stable but is a no-op for nightly channels
+RUSTC_BOOTSTRAP = "1"
 
 [target.'cfg(all())']
 rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 2a29985cb229..5805dc4f7280 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -285,10 +285,13 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
     // give the struct the name "overflow_result_<type>", e.g.
     // "overflow_result_Unsignedbv"
     let name: InternedString = format!("overflow_result_{operand_type:?}").into();
-    Type::struct_type(name, vec![
-        DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
-        DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
-    ])
+    Type::struct_type(
+        name,
+        vec![
+            DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
+            DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
+        ],
+    )
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
index b3e29d8b5c65..5a0ad76b81c6 100644
--- a/cprover_bindings/src/goto_program/typ.rs
+++ b/cprover_bindings/src/goto_program/typ.rs
@@ -1594,10 +1594,10 @@ mod type_tests {
     fn check_typedef_struct_properties() {
         // Create a struct with a random field.
         let struct_name: InternedString = "MyStruct".into();
-        let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
-            name: "field".into(),
-            typ: Double,
-        }]);
+        let struct_type = Type::struct_type(
+            struct_name,
+            vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
+        );
         // Insert a field to the sym table to represent the struct field.
         let mut sym_table = SymbolTable::new(machine_model_test_stub());
         sym_table.ensure(struct_type.type_name().unwrap(), |_, name| {
diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs
index 6985d4a60dee..51a2b06fd874 100644
--- a/cprover_bindings/src/irep/serialize.rs
+++ b/cprover_bindings/src/irep/serialize.rs
@@ -149,12 +149,10 @@ mod test {
     #[test]
     fn serialize_irep() {
         let irep = Irep::empty();
-        assert_ser_tokens(&irep, &[
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("empty"),
-            Token::MapEnd,
-        ]);
+        assert_ser_tokens(
+            &irep,
+            &[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd],
+        );
     }
 
     #[test]
@@ -189,77 +187,80 @@ mod test {
             is_weak: false,
         };
         sym_table.insert(symbol);
-        assert_ser_tokens(&sym_table, &[
-            Token::Map { len: None },
-            Token::String("symbolTable"),
-            Token::Map { len: Some(1) },
-            Token::String("my_name"),
-            // symbol start
-            Token::Map { len: None },
-            // type irep
-            Token::String("type"),
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("empty"),
-            Token::MapEnd,
-            // value irep
-            Token::String("value"),
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("empty"),
-            Token::MapEnd,
-            // value locaton
-            Token::String("location"),
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("empty"),
-            Token::MapEnd,
-            Token::String("name"),
-            Token::String("my_name"),
-            Token::String("module"),
-            Token::String(""),
-            Token::String("baseName"),
-            Token::String(""),
-            Token::String("prettyName"),
-            Token::String(""),
-            Token::String("mode"),
-            Token::String(""),
-            Token::String("isType"),
-            Token::Bool(false),
-            Token::String("isMacro"),
-            Token::Bool(false),
-            Token::String("isExported"),
-            Token::Bool(false),
-            Token::String("isInput"),
-            Token::Bool(false),
-            Token::String("isOutput"),
-            Token::Bool(false),
-            Token::String("isStateVar"),
-            Token::Bool(false),
-            Token::String("isProperty"),
-            Token::Bool(false),
-            Token::String("isStaticLifetime"),
-            Token::Bool(false),
-            Token::String("isThreadLocal"),
-            Token::Bool(false),
-            Token::String("isLvalue"),
-            Token::Bool(false),
-            Token::String("isFileLocal"),
-            Token::Bool(false),
-            Token::String("isExtern"),
-            Token::Bool(false),
-            Token::String("isVolatile"),
-            Token::Bool(false),
-            Token::String("isParameter"),
-            Token::Bool(false),
-            Token::String("isAuxiliary"),
-            Token::Bool(false),
-            Token::String("isWeak"),
-            Token::Bool(false),
-            Token::MapEnd,
-            Token::MapEnd,
-            Token::MapEnd,
-        ]);
+        assert_ser_tokens(
+            &sym_table,
+            &[
+                Token::Map { len: None },
+                Token::String("symbolTable"),
+                Token::Map { len: Some(1) },
+                Token::String("my_name"),
+                // symbol start
+                Token::Map { len: None },
+                // type irep
+                Token::String("type"),
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String("empty"),
+                Token::MapEnd,
+                // value irep
+                Token::String("value"),
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String("empty"),
+                Token::MapEnd,
+                // value locaton
+                Token::String("location"),
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String("empty"),
+                Token::MapEnd,
+                Token::String("name"),
+                Token::String("my_name"),
+                Token::String("module"),
+                Token::String(""),
+                Token::String("baseName"),
+                Token::String(""),
+                Token::String("prettyName"),
+                Token::String(""),
+                Token::String("mode"),
+                Token::String(""),
+                Token::String("isType"),
+                Token::Bool(false),
+                Token::String("isMacro"),
+                Token::Bool(false),
+                Token::String("isExported"),
+                Token::Bool(false),
+                Token::String("isInput"),
+                Token::Bool(false),
+                Token::String("isOutput"),
+                Token::Bool(false),
+                Token::String("isStateVar"),
+                Token::Bool(false),
+                Token::String("isProperty"),
+                Token::Bool(false),
+                Token::String("isStaticLifetime"),
+                Token::Bool(false),
+                Token::String("isThreadLocal"),
+                Token::Bool(false),
+                Token::String("isLvalue"),
+                Token::Bool(false),
+                Token::String("isFileLocal"),
+                Token::Bool(false),
+                Token::String("isExtern"),
+                Token::Bool(false),
+                Token::String("isVolatile"),
+                Token::Bool(false),
+                Token::String("isParameter"),
+                Token::Bool(false),
+                Token::String("isAuxiliary"),
+                Token::Bool(false),
+                Token::String("isWeak"),
+                Token::Bool(false),
+                Token::MapEnd,
+                Token::MapEnd,
+                Token::MapEnd,
+            ],
+        );
     }
 
     #[test]
@@ -268,38 +269,41 @@ mod test {
         let one_irep = Irep::one();
         let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]);
         let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]);
-        assert_ser_tokens(&top_irep, &[
-            // top_irep
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String(""),
-            Token::String("sub"),
-            Token::Seq { len: Some(2) },
-            // sub_irep
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String(""),
-            Token::String("sub"),
-            Token::Seq { len: Some(2) },
-            // empty_irep
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("empty"),
-            Token::MapEnd,
-            // one_irep
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("1"),
-            Token::MapEnd,
-            Token::SeqEnd,
-            Token::MapEnd,
-            // empty_irep
-            Token::Map { len: None },
-            Token::String("id"),
-            Token::String("empty"),
-            Token::MapEnd,
-            Token::SeqEnd,
-            Token::MapEnd,
-        ]);
+        assert_ser_tokens(
+            &top_irep,
+            &[
+                // top_irep
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String(""),
+                Token::String("sub"),
+                Token::Seq { len: Some(2) },
+                // sub_irep
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String(""),
+                Token::String("sub"),
+                Token::Seq { len: Some(2) },
+                // empty_irep
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String("empty"),
+                Token::MapEnd,
+                // one_irep
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String("1"),
+                Token::MapEnd,
+                Token::SeqEnd,
+                Token::MapEnd,
+                // empty_irep
+                Token::Map { len: None },
+                Token::String("id"),
+                Token::String("empty"),
+                Token::MapEnd,
+                Token::SeqEnd,
+                Token::MapEnd,
+            ],
+        );
     }
 }
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index e007652a04a9..7fd364e5d725 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -273,12 +273,10 @@ impl ToIrep for ExprValue {
                     )],
                 }
             }
-            ExprValue::FunctionCall { function, arguments } => {
-                side_effect_irep(IrepId::FunctionCall, vec![
-                    function.to_irep(mm),
-                    arguments_irep(arguments.iter(), mm),
-                ])
-            }
+            ExprValue::FunctionCall { function, arguments } => side_effect_irep(
+                IrepId::FunctionCall,
+                vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
+            ),
             ExprValue::If { c, t, e } => Irep {
                 id: IrepId::If,
                 sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)],
@@ -320,11 +318,10 @@ impl ToIrep for ExprValue {
                 named_sub: linear_map![],
             },
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
-            ExprValue::StatementExpression { statements: ops, location: loc } => {
-                side_effect_irep(IrepId::StatementExpression, vec![
-                    Stmt::block(ops.to_vec(), *loc).to_irep(mm),
-                ])
-            }
+            ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
+                IrepId::StatementExpression,
+                vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
+            ),
             ExprValue::StringConstant { s } => Irep {
                 id: IrepId::StringConstant,
                 sub: vec![],
@@ -491,10 +488,10 @@ impl ToIrep for StmtBody {
             StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
             StmtBody::Decl { lhs, value } => {
                 if value.is_some() {
-                    code_irep(IrepId::Decl, vec![
-                        lhs.to_irep(mm),
-                        value.as_ref().unwrap().to_irep(mm),
-                    ])
+                    code_irep(
+                        IrepId::Decl,
+                        vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)],
+                    )
                 } else {
                     code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
                 }
@@ -507,19 +504,18 @@ impl ToIrep for StmtBody {
                     .with_comment("deinit")
             }
             StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
-            StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![
-                init.to_irep(mm),
-                cond.to_irep(mm),
-                update.to_irep(mm),
-                body.to_irep(mm),
-            ]),
-            StmtBody::FunctionCall { lhs, function, arguments } => {
-                code_irep(IrepId::FunctionCall, vec![
+            StmtBody::For { init, cond, update, body } => code_irep(
+                IrepId::For,
+                vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)],
+            ),
+            StmtBody::FunctionCall { lhs, function, arguments } => code_irep(
+                IrepId::FunctionCall,
+                vec![
                     lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
                     function.to_irep(mm),
                     arguments_irep(arguments.iter(), mm),
-                ])
-            }
+                ],
+            ),
             StmtBody::Goto { dest, loop_invariants } => {
                 let stmt_goto = code_irep(IrepId::Goto, vec![])
                     .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()));
@@ -532,11 +528,14 @@ impl ToIrep for StmtBody {
                     stmt_goto
                 }
             }
-            StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![
-                i.to_irep(mm),
-                t.to_irep(mm),
-                e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
-            ]),
+            StmtBody::Ifthenelse { i, t, e } => code_irep(
+                IrepId::Ifthenelse,
+                vec![
+                    i.to_irep(mm),
+                    t.to_irep(mm),
+                    e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
+                ],
+            ),
             StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)])
                 .with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())),
             StmtBody::Return(e) => {
@@ -548,10 +547,10 @@ impl ToIrep for StmtBody {
                 if default.is_some() {
                     switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm));
                 }
-                code_irep(IrepId::Switch, vec![
-                    control.to_irep(mm),
-                    code_irep(IrepId::Block, switch_arms),
-                ])
+                code_irep(
+                    IrepId::Switch,
+                    vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)],
+                )
             }
             StmtBody::While { cond, body } => {
                 code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)])
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
index 4780b4023a02..546a3aa4f127 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -1416,10 +1416,13 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             }
             RigidTy::RawPtr(ty, mutability) => {
                 let c_ty = self.translate_ty(ty);
-                CharonTy::new(CharonTyKind::RawPtr(c_ty, match mutability {
-                    Mutability::Mut => CharonRefKind::Mut,
-                    Mutability::Not => CharonRefKind::Shared,
-                }))
+                CharonTy::new(CharonTyKind::RawPtr(
+                    c_ty,
+                    match mutability {
+                        Mutability::Mut => CharonRefKind::Mut,
+                        Mutability::Not => CharonRefKind::Shared,
+                    },
+                ))
             }
             RigidTy::FnPtr(polyfunsig) => {
                 let value = polyfunsig.value;
@@ -1539,9 +1542,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     args: args.iter().map(|arg| self.translate_operand(arg)).collect(),
                     dest: self.translate_place(destination),
                 };
-                (Some(CharonRawStatement::Call(call)), CharonRawTerminator::Goto {
-                    target: CharonBlockId::from_usize(target.unwrap()),
-                })
+                (
+                    Some(CharonRawStatement::Call(call)),
+                    CharonRawTerminator::Goto {
+                        target: CharonBlockId::from_usize(target.unwrap()),
+                    },
+                )
             }
             TerminatorKind::Assert { cond, expected, msg: _, target, .. } => (
                 Some(CharonRawStatement::Assert(CharonAssert {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index f4ca557afbdb..b78d980a2cf4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -942,10 +942,10 @@ impl GotocCtx<'_> {
     pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty) -> Expr {
         let layout = self.layout_of_stable(ty);
         assert!(
-            matches!(&layout.variants, Variants::Multiple {
-                tag_encoding: TagEncoding::Direct,
-                ..
-            }),
+            matches!(
+                &layout.variants,
+                Variants::Multiple { tag_encoding: TagEncoding::Direct, .. }
+            ),
             "discriminant field (`case`) only exists for multiple variants and direct encoding"
         );
         let expr = if ty.kind().is_coroutine() {
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index 67d32b0079c4..e3ebb20b71d9 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -58,11 +58,8 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
         let attributes = KaniAttributes::for_def_id(tcx, item.def_id());
 
         if attributes.has_contract() {
-            fn_to_data.insert(item.def_id(), ContractedFunction {
-                function,
-                file,
-                harnesses: vec![],
-            });
+            fn_to_data
+                .insert(item.def_id(), ContractedFunction { function, file, harnesses: vec![] });
         } else if let Some((target_name, internal_def_id, _)) =
             attributes.interpret_for_contract_attribute()
         {
@@ -72,11 +69,14 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
             if let Some(cf) = fn_to_data.get_mut(&target_def_id) {
                 cf.harnesses.push(function);
             } else {
-                fn_to_data.insert(target_def_id, ContractedFunction {
-                    function: target_name.to_string(),
-                    file,
-                    harnesses: vec![function],
-                });
+                fn_to_data.insert(
+                    target_def_id,
+                    ContractedFunction {
+                        function: target_name.to_string(),
+                        file,
+                        harnesses: vec![function],
+                    },
+                );
             }
         }
     }
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 3d80397530b3..c326172ba843 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
@@ -463,19 +463,22 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> {
             // Sanity check. The first argument is the closure itself and the second argument is the tupled arguments from the caller.
             assert!(args.len() == 2);
             // First, connect all upvars.
-            let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
-                local: 1usize.into(),
-                projection: List::empty(),
-            })]);
+            let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(
+                instance,
+                Place { local: 1usize.into(), projection: List::empty() },
+            )]);
             let rvalue_set = self.successors_for_operand(state, args[0].node.clone());
             initial_graph.extend(&lvalue_set, &rvalue_set);
             // Then, connect the argument tuple to each of the spread arguments.
             let spread_arg_operand = args[1].node.clone();
             for i in 0..new_body.arg_count {
-                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
-                    local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
-                    projection: List::empty(),
-                })]);
+                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(
+                    instance,
+                    Place {
+                        local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
+                        projection: List::empty(),
+                    },
+                )]);
                 // This conservatively assumes all arguments alias to all parameters.
                 let rvalue_set = self.successors_for_operand(state, spread_arg_operand.clone());
                 initial_graph.extend(&lvalue_set, &rvalue_set);
@@ -483,10 +486,13 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> {
         } else {
             // Otherwise, simply connect all arguments to parameters.
             for (i, arg) in args.iter().enumerate() {
-                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
-                    local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
-                    projection: List::empty(),
-                })]);
+                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(
+                    instance,
+                    Place {
+                        local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
+                        projection: List::empty(),
+                    },
+                )]);
                 let rvalue_set = self.successors_for_operand(state, arg.node.clone());
                 initial_graph.extend(&lvalue_set, &rvalue_set);
             }
@@ -500,10 +506,10 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> {
 
         // Connect the return value to the return destination.
         let lvalue_set = state.resolve_place(*destination, self.instance);
-        let rvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
-            local: 0usize.into(),
-            projection: List::empty(),
-        })]);
+        let rvalue_set = HashSet::from([MemLoc::new_stack_allocation(
+            instance,
+            Place { local: 0usize.into(), projection: List::empty() },
+        )]);
         state.extend(&lvalue_set, &state.successors(&rvalue_set));
     }
 
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index fea8a8a1bc3c..41a41d2e73f7 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -434,10 +434,10 @@ impl FunctionWithContractPass {
             &mut mode_call,
             InsertPosition::Before,
         );
-        new_body.replace_terminator(&mode_call, Terminator {
-            kind: TerminatorKind::Goto { target },
-            span,
-        });
+        new_body.replace_terminator(
+            &mode_call,
+            Terminator { kind: TerminatorKind::Goto { target }, span },
+        );
 
         new_body.into()
     }
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index 8001b1f1d359..32caea57750e 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -83,11 +83,14 @@ impl BodyTransformation {
         // would also make sense to check that the values are initialized before checking their
         // validity. In the future, it would be nice to have a mechanism to skip automatically
         // generated code for future instrumentation passes.
-        transformer.add_pass(queries, UninitPass {
-            // Since this uses demonic non-determinism under the hood, should not assume the assertion.
-            check_type: CheckType::new_assert(queries),
-            mem_init_fn_cache: queries.kani_functions().clone(),
-        });
+        transformer.add_pass(
+            queries,
+            UninitPass {
+                // Since this uses demonic non-determinism under the hood, should not assume the assertion.
+                check_type: CheckType::new_assert(queries),
+                mem_init_fn_cache: queries.kani_functions().clone(),
+            },
+        );
         transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries));
         transformer.add_pass(queries, LoopContractPass::new(tcx, queries, &unit));
         transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries));
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 65424f6d46bf..761d9eba7a45 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -16,6 +16,8 @@
 #![feature(f128)]
 #![feature(f16)]
 #![feature(non_exhaustive_omitted_patterns_lint)]
+#![feature(cfg_version)]
+#![cfg_attr(not(version("1.86")), feature(float_next_up_down))]
 #![feature(try_blocks)]
 extern crate rustc_abi;
 extern crate rustc_ast;
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 0bc716115989..b28d8b089d9f 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -207,6 +207,8 @@ crate-type = ["lib"]
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
                     // https://doc.rust-lang.org/cargo/reference/environment-variables.html
                     .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
+                    // This is only required for stable but is a no-op for nightly channels
+                    .env("RUSTC_BOOTSTRAP", "1")
                     .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
                 match self.run_build_target(cmd, verification_target.target()) {
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 9a09ce6163f8..f21f83345783 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -84,6 +84,8 @@ impl KaniSession {
         let mut cmd = Command::new(&self.kani_compiler);
         let kani_compiler_args = to_rustc_arg(kani_args);
         cmd.arg(kani_compiler_args).args(rustc_args);
+        // This is only required for stable but is a no-op for nightly channels
+        cmd.env("RUSTC_BOOTSTRAP", "1");
 
         if self.args.common_args.quiet {
             self.run_suppress(cmd)?;
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index cc48449e01b2..95a2175a2eac 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -22,96 +22,126 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
     map.insert("error_label", vec![]);
     map.insert("division-by-zero", vec![("division by zero", None)]);
     map.insert("enum-range-check", vec![("enum range check", None)]);
-    map.insert("undefined-shift", vec![
-        ("shift distance is negative", None),
-        ("shift distance too large", None),
-        ("shift operand is negative", None),
-        ("shift of non-integer type", None),
-    ]);
-    map.insert("overflow", vec![
-        ("result of signed mod is not representable", None),
-        ("arithmetic overflow on signed type conversion", None),
-        ("arithmetic overflow on signed division", None),
-        ("arithmetic overflow on signed unary minus", None),
-        ("arithmetic overflow on signed shl", None),
-        ("arithmetic overflow on unsigned unary minus", None),
-        ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")),
-        ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")),
-        ("arithmetic overflow on signed *", Some("arithmetic overflow on signed multiplication")),
-        ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")),
-        ("arithmetic overflow on unsigned -", Some("arithmetic overflow on unsigned subtraction")),
-        (
-            "arithmetic overflow on unsigned *",
-            Some("arithmetic overflow on unsigned multiplication"),
-        ),
-        ("arithmetic overflow on floating-point typecast", None),
-        ("arithmetic overflow on floating-point division", None),
-        ("arithmetic overflow on floating-point addition", None),
-        ("arithmetic overflow on floating-point subtraction", None),
-        ("arithmetic overflow on floating-point multiplication", None),
-        ("arithmetic overflow on unsigned to signed type conversion", None),
-        ("arithmetic overflow on float to signed integer type conversion", None),
-        ("arithmetic overflow on signed to unsigned type conversion", None),
-        ("arithmetic overflow on unsigned to unsigned type conversion", None),
-        ("arithmetic overflow on float to unsigned integer type conversion", None),
-    ]);
-    map.insert("NaN", vec![
-        ("NaN on +", Some("NaN on addition")),
-        ("NaN on -", Some("NaN on subtraction")),
-        ("NaN on /", Some("NaN on division")),
-        ("NaN on *", Some("NaN on multiplication")),
-    ]);
-    map.insert("pointer_arithmetic", vec![
-        ("pointer relation: deallocated dynamic object", None),
-        ("pointer relation: dead object", None),
-        ("pointer relation: pointer NULL", None),
-        ("pointer relation: pointer invalid", None),
-        ("pointer relation: pointer outside dynamic object bounds", None),
-        ("pointer relation: pointer outside object bounds", None),
-        ("pointer relation: invalid integer address", None),
-        ("pointer arithmetic: deallocated dynamic object", None),
-        ("pointer arithmetic: dead object", None),
-        ("pointer arithmetic: pointer NULL", None),
-        ("pointer arithmetic: pointer invalid", None),
-        ("pointer arithmetic: pointer outside dynamic object bounds", None),
-        ("pointer arithmetic: pointer outside object bounds", None),
-        ("pointer arithmetic: invalid integer address", None),
-    ]);
-    map.insert("pointer_dereference", vec![
-        (
-            "dereferenced function pointer must be",
-            Some("dereference failure: invalid function pointer"),
-        ),
-        ("dereference failure: pointer NULL", None),
-        ("dereference failure: pointer invalid", None),
-        ("dereference failure: deallocated dynamic object", None),
-        ("dereference failure: dead object", None),
-        ("dereference failure: pointer outside dynamic object bounds", None),
-        ("dereference failure: pointer outside object bounds", None),
-        ("dereference failure: invalid integer address", None),
-    ]);
+    map.insert(
+        "undefined-shift",
+        vec![
+            ("shift distance is negative", None),
+            ("shift distance too large", None),
+            ("shift operand is negative", None),
+            ("shift of non-integer type", None),
+        ],
+    );
+    map.insert(
+        "overflow",
+        vec![
+            ("result of signed mod is not representable", None),
+            ("arithmetic overflow on signed type conversion", None),
+            ("arithmetic overflow on signed division", None),
+            ("arithmetic overflow on signed unary minus", None),
+            ("arithmetic overflow on signed shl", None),
+            ("arithmetic overflow on unsigned unary minus", None),
+            ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")),
+            ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")),
+            (
+                "arithmetic overflow on signed *",
+                Some("arithmetic overflow on signed multiplication"),
+            ),
+            ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")),
+            (
+                "arithmetic overflow on unsigned -",
+                Some("arithmetic overflow on unsigned subtraction"),
+            ),
+            (
+                "arithmetic overflow on unsigned *",
+                Some("arithmetic overflow on unsigned multiplication"),
+            ),
+            ("arithmetic overflow on floating-point typecast", None),
+            ("arithmetic overflow on floating-point division", None),
+            ("arithmetic overflow on floating-point addition", None),
+            ("arithmetic overflow on floating-point subtraction", None),
+            ("arithmetic overflow on floating-point multiplication", None),
+            ("arithmetic overflow on unsigned to signed type conversion", None),
+            ("arithmetic overflow on float to signed integer type conversion", None),
+            ("arithmetic overflow on signed to unsigned type conversion", None),
+            ("arithmetic overflow on unsigned to unsigned type conversion", None),
+            ("arithmetic overflow on float to unsigned integer type conversion", None),
+        ],
+    );
+    map.insert(
+        "NaN",
+        vec![
+            ("NaN on +", Some("NaN on addition")),
+            ("NaN on -", Some("NaN on subtraction")),
+            ("NaN on /", Some("NaN on division")),
+            ("NaN on *", Some("NaN on multiplication")),
+        ],
+    );
+    map.insert(
+        "pointer_arithmetic",
+        vec![
+            ("pointer relation: deallocated dynamic object", None),
+            ("pointer relation: dead object", None),
+            ("pointer relation: pointer NULL", None),
+            ("pointer relation: pointer invalid", None),
+            ("pointer relation: pointer outside dynamic object bounds", None),
+            ("pointer relation: pointer outside object bounds", None),
+            ("pointer relation: invalid integer address", None),
+            ("pointer arithmetic: deallocated dynamic object", None),
+            ("pointer arithmetic: dead object", None),
+            ("pointer arithmetic: pointer NULL", None),
+            ("pointer arithmetic: pointer invalid", None),
+            ("pointer arithmetic: pointer outside dynamic object bounds", None),
+            ("pointer arithmetic: pointer outside object bounds", None),
+            ("pointer arithmetic: invalid integer address", None),
+        ],
+    );
+    map.insert(
+        "pointer_dereference",
+        vec![
+            (
+                "dereferenced function pointer must be",
+                Some("dereference failure: invalid function pointer"),
+            ),
+            ("dereference failure: pointer NULL", None),
+            ("dereference failure: pointer invalid", None),
+            ("dereference failure: deallocated dynamic object", None),
+            ("dereference failure: dead object", None),
+            ("dereference failure: pointer outside dynamic object bounds", None),
+            ("dereference failure: pointer outside object bounds", None),
+            ("dereference failure: invalid integer address", None),
+        ],
+    );
     // These are very hard to understand without more context.
-    map.insert("pointer_primitives", vec![
-        ("pointer invalid", None),
-        ("deallocated dynamic object", Some("pointer to deallocated dynamic object")),
-        ("dead object", Some("pointer to dead object")),
-        ("pointer outside dynamic object bounds", None),
-        ("pointer outside object bounds", None),
-        ("invalid integer address", None),
-    ]);
-    map.insert("array_bounds", vec![
-        ("lower bound", Some("index out of bounds")),
-        // This one is redundant:
-        // ("dynamic object upper bound", Some("access out of bounds")),
-        (
-            "upper bound",
-            Some("index out of bounds: the length is less than or equal to the given index"),
-        ),
-    ]);
-    map.insert("bit_count", vec![
-        ("count trailing zeros is undefined for value zero", None),
-        ("count leading zeros is undefined for value zero", None),
-    ]);
+    map.insert(
+        "pointer_primitives",
+        vec![
+            ("pointer invalid", None),
+            ("deallocated dynamic object", Some("pointer to deallocated dynamic object")),
+            ("dead object", Some("pointer to dead object")),
+            ("pointer outside dynamic object bounds", None),
+            ("pointer outside object bounds", None),
+            ("invalid integer address", None),
+        ],
+    );
+    map.insert(
+        "array_bounds",
+        vec![
+            ("lower bound", Some("index out of bounds")),
+            // This one is redundant:
+            // ("dynamic object upper bound", Some("access out of bounds")),
+            (
+                "upper bound",
+                Some("index out of bounds: the length is less than or equal to the given index"),
+            ),
+        ],
+    );
+    map.insert(
+        "bit_count",
+        vec![
+            ("count trailing zeros is undefined for value zero", None),
+            ("count leading zeros is undefined for value zero", None),
+        ],
+    );
     map.insert("memory-leak", vec![("dynamically allocated memory never freed", None)]);
     // These pre-conditions should not print temporary variables since they are embedded in the libc implementation.
     // They are added via `__CPROVER_precondition`.
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
index 5c4076f13591..282ae42a7c37 100644
--- a/kani-driver/src/concrete_playback/test_generator.rs
+++ b/kani-driver/src/concrete_playback/test_generator.rs
@@ -500,11 +500,10 @@ mod tests {
     /// Check that the generated unit tests have the right formatting and indentation
     #[test]
     fn format_two_concrete_vals() {
-        let concrete_vals =
-            [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, ConcreteVal {
-                byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0],
-                interp_val: "0l".to_string(),
-            }];
+        let concrete_vals = [
+            ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() },
+            ConcreteVal { byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], interp_val: "0l".to_string() },
+        ];
         let actual: Vec<_> = format_concrete_vals(&concrete_vals).collect();
         let expected = vec![
             format!("{:<8}// 0", " "),
@@ -598,11 +597,10 @@ mod tests {
 
     #[test]
     fn check_rustfmt_args_some_line_ranges() {
-        let file_line_ranges =
-            [FileLineRange { file: "file1".to_string(), line_range: None }, FileLineRange {
-                file: "path/to/file2".to_string(),
-                line_range: Some((1, 3)),
-            }];
+        let file_line_ranges = [
+            FileLineRange { file: "file1".to_string(), line_range: None },
+            FileLineRange { file: "path/to/file2".to_string(), line_range: Some((1, 3)) },
+        ];
         let args = rustfmt_args(&file_line_ranges);
         let expected: Vec<OsString> = [
             "--unstable-features",
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 9ae762092eb2..345c2254017b 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-01-24"
+channel = "1.85.1"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/rustfmt.toml b/rustfmt.toml
index 44cbfe4a3dc9..7d435590213a 100644
--- a/rustfmt.toml
+++ b/rustfmt.toml
@@ -7,12 +7,3 @@ style_edition = "2024"
 use_small_heuristics = "Max"
 merge_derives = false
 
-ignore = [
-    "**/build/",
-    "**/target/",
-
-    # Do not format submodules
-    # For some reason, this is not working without the directory wildcard.
-    "**/firecracker",
-    "**/tests/perf/s2n-quic/",
-]
diff --git a/scripts/kani-fmt.sh b/scripts/kani-fmt.sh
index 5eca1582cc40..f5b90f75a145 100755
--- a/scripts/kani-fmt.sh
+++ b/scripts/kani-fmt.sh
@@ -27,11 +27,11 @@ for suite in "${TESTS[@]}"; do
     # Find uses breakline to split between files. This ensures that we can
     # handle files with space in their path.
     set -f; IFS=$'\n'
-    files=($(find "${suite}" -name "*.rs"))
+    files=($(find "${suite}" -name "*.rs" -not -path "*/perf/s2n-quic/*"))
     set +f; unset IFS
     # Note: We set the configuration file here because some submodules have
     # their own configuration file.
-    rustfmt --unstable-features "$@" --config-path rustfmt.toml "${files[@]}" || error=1
+    rustfmt "$@" --config-path rustfmt.toml "${files[@]}" || error=1
 done
 
 exit $error
diff --git a/tests/cargo-ui/verbose-cmds/expected b/tests/cargo-ui/verbose-cmds/expected
index f883ef972cb3..b47b60d51ff4 100644
--- a/tests/cargo-ui/verbose-cmds/expected
+++ b/tests/cargo-ui/verbose-cmds/expected
@@ -1,5 +1,5 @@
 CARGO_ENCODED_RUSTFLAGS=
-cargo +nightly
+cargo +
 Running: `goto-cc
 Running: `goto-instrument
 Checking harness dummy_harness...
diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
index 38f31a63d5ca..0c43cd901cc9 100644
--- a/tests/expected/function-contract/valid_ptr.expected
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -4,9 +4,7 @@ Failed Checks: |result| kani::mem::can_dereference(result.0)
 VERIFICATION:- FAILED
 
 Checking harness pre_condition::harness_invalid_ptr...
-Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20
 Failed Checks: Kani does not support reasoning about pointer to unallocated memory
-Failed Checks: dereference failure: pointer outside object bounds
 VERIFICATION:- FAILED
 
 Checking harness pre_condition::harness_stack_ptr...