El equipo OpenShell ha desarrollado un enfoque basado en métodos formales para garantizar que los sistemas de agentes de inteligencia artificial no superen los permisos autorizados por los operadores humanos. A medida que los agentes se vuelven más autónomos y realizan tareas de larga duración, la supervisión humana directa se vuelve inviable, creando un riesgo de que los agentes accedan a recursos prohibidos mediante combinaciones no intencionadas de políticas de red, archivos y credenciales.
Para resolver esto, el equipo utiliza la librería de código abierto Z3, un solucionador de SMT (Satisfiability Modulo Theories), para modelar las políticas de acceso de los agentes como fórmulas lógicas. Este proceso permite generar pruebas formales que verifican si ciertas invariantes de seguridad, como la restricción de escritura a un repositorio específico, se mantienen intactas. A diferencia de las revisiones probabilísticas de modelos de IA, que pueden fallar o duplicar costes de cómputo, las pruebas formales son deterministas, requieren milisegundos de ejecución y no consumen tokens.
Esta técnica, inspirada en el trabajo previo de AWS con Zelkova para verificar políticas IAM y S3, ofrece una auditoría formal auditable que complementa la revisión humana. Al combinar la precisión lógica de Z3 con la capacidad de los modelos de IA, se crea un sistema de control más robusto que mitiga los riesgos de seguridad en entornos críticos y regulados.