The field of formal verification and programming languages is witnessing significant developments, with a focus on enhancing the safety, correctness, and efficiency of software systems. Researchers are exploring innovative approaches to combine reasoning principles from distinct dynamic logics, enabling the verification of heterogeneous systems. Furthermore, new type theories are being proposed to provide precise resource annotations for higher-order functions, and domain-specific languages are being designed to ensure the safety and correctness of kernel extensions. Additionally, there is a growing interest in understanding the relationship between effect systems and modal effect types, as well as developing semantic notions of memory safety. Noteworthy papers in this area include:

• Heterogeneous Dynamic Logic, which introduces a framework for combining dynamic logics in a modular and compositional way.
• BeePL, a domain-specific language for eBPF with a formally verified type system, which statically enforces key safety properties.
• Rows and Capabilities as Modal Effects, which proposes a uniform framework for encoding and comparing effect systems.
• The downgrading semantics of memory safety, which proposes a notion of gradual allocator independence to capture allocator-specific aspects of memory safety.