The SAE-standardized AADL modeling language has been a significant enabler for academic and industry research on model-based development with integrated formal methods. However, several factors including industry preference for other modeling languages such as SysML, have hampered adoption of AADL and its associated formal methods technologies. The Object Management Group (OMG) is currently working on the next SysML generation (SysMLv2) that embraces several attractive characteristics of AADL and has chartered the Real-Time Embedded Safety-Critical (RTESC) working group to consider how AADL concepts, semantics, and formal specifications can be brought into the SysMLv2 ecosystem. In this paper, we report on our development of a SysMLv2 front-end for the HAMR formal-methods-integrated model-based development framework. We provide the first illustration of how the RTESC SysMLv2 libraries for AADL concepts can be used in an end-to-end tool for code generation with integrated formal methods at multiple levels. We describe how the GUMBO formal component contract language can be integrated into the SysMLv2 AADL profile to provide: (a) SMT-based integration checking at the model level, and (b) automated testing and verification of component application to architecture contracts. We present a tool architecture that enables HAMR code generation targeting the formally verified seL4 microkernel as well as other formal methods tools being applied to SysMLv2 models in the context of the Collins Aerospace DARPA PROVERS INSPECTA project.