The field of temporal logic and formal methods is witnessing a significant shift towards the development of more expressive and tractable logical frameworks. Researchers are exploring negation-free fragments of temporal rule-based systems, which preserve monotonicity and enable scalable reasoning. This has led to the discovery of robust fragments capable of capturing both existential and invariant temporal patterns. Additionally, there is a growing interest in applying formal methods to real-world applications, such as protocol specification and verification. The use of large language models and interactive tools is also becoming increasingly popular for enhancing protocol comprehension and supporting robust implementations. Noteworthy papers in this area include: RFSeek, which presents an interactive tool for automatically extracting visual summaries of protocol logic from RFCs. GallinaC, which introduces a proof-oriented imperative language featuring well-behaved semantics and allowing imperative idioms. A Variety of Request-Response Specifications, which classifies and formalizes variations of request-response specifications and surveys tools for monitoring these specifications.