La creciente complejidad de los sistemas ciberfísicos está impulsando la necesidad de asegurar la infraestructura crítica y los sistemas embebidos. Sin embargo, los métodos tradicionales para asegurar los sistemas ciberfísicos, como el uso de mejores prácticas cibernéticas, la adaptación de mecanismos de sistemas de tecnología de la información y las pruebas de penetración seguidas de parches, están volviéndose ineficaces. Este documento describe, en detalle, la Evidencia de Verificación y el Diseño Resiliente en anticipación a las Amenazas de Ciberseguridad (VERDICT), un lenguaje y marco para abordar la resiliencia cibernética. Cuando usamos el término resiliencia, nos referimos a endurecer un sistema de tal manera que anticipe y resista ataques. VERDICT analiza un sistema frente a amenazas cibernéticas y recomienda mejoras de diseño que se pueden aplicar temprano en el proceso de ingeniería del sistema. Esto se realiza en dos pasos: (1) Analizando a nivel arquitectónico del sistema, con respecto a los requisitos cibernéticos y de seguridad, y (2) analizando a nivel de comportamiento de componentes, con respecto a un conjunto de propiedades de resiliencia cibernética. El marco consta de tres partes: (1) Análisis y Síntesis Arquitectónica Basada en Modelos (MBAAS); (2) Generación de Fragmentos de Casos de Aseguramiento (ACFG); y (3) Verificador de Resiliencia Cibernética (CRV). El lenguaje VERDICT es un anexo del Lenguaje de Análisis y Diseño de Arquitectura (AADL) para modelar los aspectos de seguridad y protección de la arquitectura de un sistema. MBAAS realiza análisis probabilísticos, sugiere defensas para mitigar ataques y genera árboles de ataque-defensa y árboles de fallos como evidencia de resiliencia y seguridad. También puede sintetizar soluciones de defensa óptimas en relación con los costos de implementación. Además, ACFG ensambla la evidencia de MBAAS en notación de estructuración de objetivos para fines de certificación. CRV analiza aspectos de comportamiento del sistema (es decir, el modelo de diseño), modelado utilizando el anexo del Entorno de Razonamiento Asumir-Garantizar (AGREE) y verificado contra propiedades de resiliencia cibernética utilizando el verificador de modelos Kind 2. Cuando se prueba o se refuta una propiedad, se identifica un conjunto mínimo de componentes vitales del sistema responsables de la prueba/refutación. CRV también proporciona diagnósticos ricos y localizados para que el usuario pueda identificar rápidamente problemas y corregir el modelo de diseño. Este documento describe el lenguaje VERDICT y cada parte del marco en detalle e incluye un estudio de caso para demostrar la efectividad de VERDICT, en este caso, un dron de entrega.