*Result*: Logika: the Sireum verification framework.

*This article gives an overview of Logika – a highly automated and interactive verification framework, that is designed for scalability and usability across a wide spectrum of users from beginners to experts in formal methods. To support the intuition of developers, it emphasizes programming constructs and idioms in both its contract-based specifications and integrated proof language. To integrate with developer workflows, verification feedback is provided directly within the industrial strength IntelliJ & VSCode-based Sireum Integrated Verification Environment (IVE & CodeIVE) and is expressed directly in terms of code features instead of lower-level SMT constraints or theorem prover languages. To support tailoring to different domains and properties, Logika includes multiple extensibility mechanisms to customize property specifications, verification rules, and proof tactics. To scale to large systems, Logika provides carefully engineered incremental verification, and it leverages modern hardware for (massive) parallelization on server-based platforms. To illustrate the wide range of Logika use cases for effective formal methods, we describe how Logika is being used to teach large classes of undergraduate students as well as to support industrial defense-related research projects. We present Logika performance experiments on both infrastructure and application code used on industry projects within the HAMR model-driven development tool chain for the AADL SAE International and the upcoming SysML v2 standard architecture specification languages. [ABSTRACT FROM AUTHOR]*