Formal Verification Under Evolution in Microservice-Based Systems: A Systematic Literature Review

Abstract

Microservice-based systems evolve continuously through API changes, service splits and merges, dependency churn, and deployment-topology drift driven by DevOps practices. This rapid evolution erodes the assumptions encoded in formal models, test suites, and architectural descriptions, leaving practitioners with limited guidance on how to keep verification artifacts aligned with evolving implementations. Prior surveys cover microservices design, deployment, performance, and isolated verification techniques, but, to our knowledge, none consolidate the intersection of evolution and formal/rigorous verification, nor map how repository-derived signals and CI/CD pipelines support continuous verification of microservice-based systems. This paper addresses that gap through a systematic literature review (SLR). Following the Kitchenham et al. guidelines and PRISMA-style reporting, we defined a review protocol with four research questions covering (i) formal modeling and verification approaches, (ii) the impact of architectural and API evolution on verifiability, (iii) repository-derived signals for updating formal artifacts, and (iv) continuous and incremental verification in CI/CD pipelines. Structured searches in IEEE Xplore, ACM Digital Library, SpringerLink, and Scopus returned 1187 records, which were screened in seven stages and reduced to 18 included studies (13 primary studies that supply evidence and five background studies retained for transparency and framing) through inclusion/exclusion criteria and a weighted 15-item quality-assessment instrument. We synthesized the included studies thematically and compared them along five dimensions: verification technique, evolution dimension, automation level, empirical evidence, and tool/artifact availability. The synthesis shows that actor-based model checking, TLA+ control-plane verification, static code analysis, continuous certification, and runtime/self-adaptive testing form five complementary clusters, but empirical evaluation is dominated by small academic case studies, only a minority of approaches automate model updates from repository signals, and few are integrated end-to-end into CI/CD. We discuss methodological limitations of the body of work, including a lack of industrial-scale validation and shared datasets, contrast intrinsic (build-time, model-driven) and extrinsic (recovery-based) verification strategies, and outline a research agenda toward repository-aware, pipeline-integrated verification for evolving microservices. The present synthesis distils a set of immediate, evidence-based actions for practitioners together with a focused agenda of open research challenges.