MAPE-KV: Una Arquitectura Neuro-Simbólica Verificada para la Orquestación de Enjambres Robóticos - Narváez, Daniel; Balich, Néstor; Rossi, Gustavo (Anais do Congresso Ibero-Americano em Engenharia de Software (CIbSE); 2026: Anais do XXIX Congresso Ibero-Americano em Engenharia de Software, 2026)
Robotic swarm orchestration in the Edge–Cloud Continuum increasingly depends on adaptive planning, yet the use of LLMs introduces stochastic risk into safety-critical cyber-physical systems. We present MAPE-KV, an extension of the MAPE-K loop that inserts a formal verification gate in Lean 4 between planning and execution. The proposal aims to block unsafe plans ante hoc through explicit physical-safety and software-quality invariants. A preliminary proof of concept in the Ester Grid simulator with five robots showed that, in the evaluated scenario, the gate intercepted all unsafe plans observed before execution. This work should be read as an architectural proposal with initial feasibility evidence, not as exhaustive experimental validation.