Agent Policy State Machine

Problema y utilidad para agentes

Un agente puede planificar una acción sin tener permiso para ejecutarla. Los reintentos, los resultados tardíos y los fallos de compensación también necesitan una política explícita antes de producir efectos.

Un entorno de ejecución serializado aplica la aprobación y la contabilidad de efectos para una operación sintética, mientras un modelo formal separado expone las transiciones inválidas.

Arquitectura

1. Restringir la operación. Una capacidad opaca de aprobación habilita un único efecto unitario en memoria. Los identificadores de eventos aceptados se deduplican dentro de la misma sección crítica.
2. Explorar el modelo finito. TLC comprueba tipos, autorización, contabilidad, reversión y estabilidad de los estados terminales en nueve símbolos de eventos y nueve fases.
3. Comparar el modelo y la ejecución. Un analizador del grafo reproduce un camino representativo hacia cada nodo y cada arista saliente, y compara el resultado con el estado exportado por el modelo.

• Política y límites de confianza
• Modelo TLA+

Qué demuestra

• Exploración real con TLC, una transición de autorización deliberadamente defectuosa y su contraejemplo conservado.
• Coincidencia en las 981 aristas exportadas y una prueba de regresión ejecutable que bloquea el efecto no autorizado.
• Veintidós pruebas de ejecución y conformidad, incluidas concurrencia, conflictos, capacidades inválidas y recuperación de la compensación.

Resultados publicados

Las comprobaciones locales registradas usaron un Intel Xeon W-3223, 48 GiB de RAM y macOS 26.7.1 el 9 de noviembre de 2026.

TLC se ejecutó con un trabajador, un procesador activo y un máximo de 512 MiB de memoria dinámica. Exploró todo el grafo finito correcto sin un límite de profundidad. La configuración defectuosa permitió ejecutar antes de aprobar y se detuvo al detectar una violación de autorización.

Estas observaciones demuestran propiedades de seguridad dentro de la abstracción finita y coincidencia de aristas desde historiales representativos. No prueban el refinamiento para todos los historiales de ejecución, propiedades de progreso ni corrección sin límites.

Los tiempos incluyen el inicio de la JVM o de Python y son observaciones individuales. No se midieron el máximo de memoria residente, la energía, el costo ni la variabilidad del rendimiento.

El repositorio conserva por separado el error inicial de sintaxis y el fallo del analizador del grafo, sin contarlos como comprobaciones exitosas. README y reproducción.

Reproducir

Usá uv 0.8.23 y Python 3.14.7. El comando de preparación crea un entorno dentro del repositorio; uv debe poder encontrar el intérprete indicado. Instalá primero esa versión de Python si no está disponible en el catálogo de descargas de uv. La preparación inicial y las dependencias de pruebas pueden necesitar acceso a Internet. La reproducción solo usa la biblioteca estándar. Las pruebas de regresión usan el archivo de dependencias congelado de uv. Java y el JAR de TLC, descargado por separado, solo son necesarios para una nueva comprobación del modelo.

Después de preparar el entorno, el comando de reproducción funciona sin conexión. El comando de reproducción verifica hashes y reproduce la evidencia guardada sin Java ni una nueva exploración del modelo. El segundo bloque ejecuta las pruebas pequeñas de regresión. Para nuevas mediciones de TLC, seguí el README y usá benchmark_lock.py en el equipo original o una ejecución exclusiva en otro equipo.

git clone https://github.com/lucioduran/agent-policy-state-machine.git
cd agent-policy-state-machine
git checkout bb96a1ace19ac0c7a90fb0e1059a2a58f6b06c70
UV_CACHE_DIR="$PWD/.tools/uv-cache" UV_PYTHON_INSTALL_DIR="$PWD/.tools/python" uv venv --python 3.14.7 .venv
PYTHONPATH=src .venv/bin/python scripts/replay.py

UV_CACHE_DIR="$PWD/.tools/uv-cache" UV_PYTHON_INSTALL_DIR="$PWD/.tools/python" uv sync --frozen --python 3.14.7
.venv/bin/pytest -q

Alcance y límites

• El modelo cubre una operación y un identificador fijo por símbolo de evento. Los conflictos con identificadores nuevos y los hilos reales se prueban fuera de la abstracción formal.
• El efecto y su compensación son cambios sintéticos en un registro en memoria. No hay recuperación tras fallos, adaptadores para herramientas externas, registro durable ni garantía distribuida de ejecución única.
• El código de la aplicación debe ser confiable y mantener privada la capacidad de aprobación. La interfaz de línea de comandos proporciona su propia capacidad y es una demostración, no un servicio de autenticación.
• La compensación puede quedar sin resolver. No se garantiza equidad ni progreso, y la consistencia de los hashes guardados no constituye una certificación independiente de las mediciones.

• Artículo técnico relacionado

Fuentes y revisión

La comprobación del modelo usó el commit 9a8273d57ecf691f5dc36207f2ce4877875f1dd4 y comenzó en la fecha del informe indicada abajo. La reproducción contra el entorno de ejecución usó el commit 30aa48bfe943dc84b8ae2cdf8fde74e138046f13 a las 2026-11-09T20:20:14.821954+00:00. La release final agrega pruebas y documentación; su manifiesto vincula los archivos medidos del modelo y del entorno de ejecución con la revisión publicada.

• Revisión consultada: bb96a1ace19ac0c7a90fb0e1059a2a58f6b06c70
• Revisión registrada por el experimento: 9a8273d57ecf691f5dc36207f2ce4877875f1dd4
• Fecha del informe (UTC): 2026-11-09T20:18:39.861683+00:00
• Release publicada: v0.1.0 · 2026-11-09T20:24:33Z
• Metadatos de la medición con TLC SHA-256: c0989f1de2c3fd310475bdbad711764fe6e9748ed08176d53a5f47f65d64277e

• README y reproducción
• Metadatos de la medición con TLC
• Metadatos de la reproducción contra el entorno de ejecución
• Licencia MIT
• Política y límites de confianza
• Modelo TLA+
• Registro exitoso de TLC
• Contraejemplo del modelo defectuoso
• Grafo exportado por TLC
• Observaciones de las aristas ejecutadas
• Manifiesto de hashes de la evidencia