The field of automated reasoning and compiler design is experiencing a significant shift towards the integration of large language models (LLMs) and traditional symbolic algorithms. This trend is driven by the need for more robust and scalable reasoning tools that can effectively leverage the strengths of both paradigms. Researchers are exploring new computational models, such as neurosymbolic transition systems, that can provide a principled foundation for building LLM-powered reasoning tools. Additionally, there is a growing focus on addressing the security vulnerabilities in compilers, particularly with regards to microarchitectural side channels and constant-time code. Novel approaches, such as stress testing microarchitectural isolation boundaries and analyzing compiler optimizations, are being developed to detect and mitigate these vulnerabilities. Furthermore, advances in verified compilation and modular metatheory are enabling the creation of more robust and extensible compiler frameworks. Noteworthy papers in this area include:

• Enter, Exit, Page Fault, Leak, which presents a tool for stress testing microarchitectural isolation boundaries and detects critical gaps in current isolation mechanisms.
• Fun with flags, which proposes a practical mitigation for compiler-introduced constant-time violations by disabling selected optimization passes via compiler flags.
• Pyrosome, which introduces a generic framework for modular language metatheory and enables the creation of verified compilers that are fully extensible.