The field of formal verification and security is rapidly evolving, with a focus on developing innovative methods to ensure the integrity and reliability of complex systems. Recent research has explored the application of formal verification techniques to real-time embedded systems, cyber-physical systems, and blockchain-based cryptocurrencies. Notably, there has been a shift towards developing more expressive and efficient formal verification frameworks, such as relational Hoare logic and team semantics, to tackle the challenges of verifying complex systems. Additionally, the importance of privacy and security in these systems has led to the development of novel methods for privacy-preserving runtime verification and secure outsourcing of verification computations. Noteworthy papers in this area include:

• Inquisitive Team Semantics of LTL, which introduces a novel team semantics of LTL and identifies a meaningful fragment with a decidable model-checking problem.
• Provable Execution in Real-Time Embedded Systems, which formulates a new security goal called Real-Time Proof of Execution and develops an architecture to achieve it.
• Relational Hoare Logic for Realistically Modelled Machine Code, which introduces a Hoare-style logic for low-level relational verification and demonstrates its applicability to large assembly codebases.
• Model Checking the Security of the Lightning Network, which formalizes the Lightning Network protocol and enables computer-aided security verification using model checking.
• Monitoring in the Dark: Privacy-Preserving Runtime Verification of Cyber-Physical Systems, which proposes a protocol for privacy-preserving robustness monitoring of cyber-physical systems.