The field of program safety and verification is moving towards more modular and compositional approaches, enabling the separate verification of safety for heterogeneous modules and composition of safety results at the target level. This shift is driven by the need to ensure end-to-end safety in modern safe programming languages like Rust, which often require mixing safe and unsafe modules. Researchers are exploring new definitions of safety, such as open safety, that can be preserved by verified compositional compilation. Additionally, there is a growing interest in leveraging type systems and large language models to improve code generation and ensure type correctness. Noteworthy papers include: Project-Level C-to-Rust Translation via Synergistic Integration of Knowledge Graphs and Large Language Models, which proposes a novel approach to translating C code into safe Rust. TypePilot: Leveraging the Scala Type System for Secure LLM-generated Code, which introduces an agentic AI framework to enhance the security and robustness of LLM-generated code.