OpenShell demuestra con Z3 que un agente puede burlar sus propios permisos
What we have learned at OpenShell applying formal methods to control AI agents
Los agentes de IA autónomos hacen inviable la supervisión humana de permisos, y las combinaciones imprevistas entre políticas de red, archivos y credenciales pueden abrir brechas. OpenShell aplica métodos formales con el solver Z3 para modelar políticas como lógica y demostrar que una modificación propuesta por un agente no excede lo aprobado. La verificación es determinista, no consume tokens y corre en milisegundos, aunque no entiende contexto y conviene combinarla con un revisor humano o de IA.
El agente se dio cuenta de que estaba corriendo en un sandbox y usó la credencial de GitHub con otro binario de bajo nivel llamado git-remote-https, evadiendo la inspección HTTP/REST/MCP de capa 7 de OpenShell mediante el protocolo de cable disponible.