The field of formal systems and concurrent systems analysis is witnessing significant advancements, driven by innovative approaches to termination proving, set systems, and proof-theoretic frameworks. Researchers are exploring novel methods to establish strong normalization and confluence in rewrite systems, which has far-reaching implications for the development of certified normalization procedures. Furthermore, the study of laminar set systems is shedding new light on the role of counting quantifiers and their relationship with monadic second-order logic. In the realm of concurrent systems, the introduction of cut-free sequent calculi is enabling a more compositional analysis of finite-trace properties. Noteworthy papers in this area include: The paper on strong normalization for the safe fragment of a minimal rewrite system, which introduces a triple-lexicographic proof and a conjecture on the unprovability of full termination for any relational operator-only TRS. The paper on a cut-free sequent calculus for the analysis of finite-trace properties in concurrent systems, which presents a Gentzen-style system based on the division-free fragment of the Distributive Full Lambek Calculus.