The meta-agent post ended with a claim: that treating agent architecture as an optimization problem — rather than a design artifact — unlocks a fundamentally different approach to building AI systems. Lab 11 proved the meta-agent could generate, optimize, and distill its own agents dynamically. But proof of concept and proof of generality are different things.
Lab 12: Formal Evolution closes that gap. The same meta-agent — zero lines of Python changed — now integrates Z3 SMT solvers for constraint verification, Lean4 theorem provers for formal proof, ArXiv for academic research, OpenRouter for multi-model consensus, and MLflow for observability. The only modification was a single JSON configuration file.
This is not a new tool. It is the same substrate, extended horizontally into formal verification, distributed consensus, and experimental science — all through configuration.
El artículo del meta-agente terminó con una afirmación: que tratar la arquitectura de agentes como un problema de optimización — en lugar de un artefacto de diseño — desbloquea un enfoque fundamentalmente diferente para construir sistemas de IA. El Lab 11 demostró que el meta-agente podía generar, optimizar y destilar sus propios agentes dinámicamente. Pero una prueba de concepto y una prueba de generalidad son cosas distintas.
Lab 12: Evolución Formal cierra esa brecha. El mismo meta-agente — sin cambiar una línea de Python — ahora integra solvers SMT Z3 para verificación de restricciones, demostradores de teoremas Lean4 para prueba formal, ArXiv para investigación académica, OpenRouter para consenso multi-modelo y MLflow para observabilidad. La única modificación fue un solo archivo de configuración JSON.
Esto no es una herramienta nueva. Es el mismo sustrato, extendido horizontalmente hacia verificación formal, consenso distribuido y ciencia experimental — todo a través de configuración.
1. The One-Config Change
1. El Único Cambio de Configuración
The meta-agent’s tool access is defined entirely through config/mcp_servers.json. Lab 11 shipped with three MCP servers: crawl4ai, fetch, and a disabled filesystem server. Lab 12 expands this to nine — and the pattern is worth examining closely:
El acceso a herramientas del meta-agente se define enteramente a través de config/mcp_servers.json. Lab 11 incluía tres servidores MCP: crawl4ai, fetch y un servidor de sistema de archivos deshabilitado. Lab 12 expande esto a nueve — y el patrón merece un examen detenido:
{
"mcpServers": {
"crawl4ai": { "type": "sse", "url": "http://localhost:11235/mcp/sse", "enabled": true },
"fetch": { "type": "stdio", "command": "uvx", "args": ["mcp-server-fetch"], "enabled": true },
"openrouter": { "type": "stdio", "command": "npx", "args": ["@physics91/openrouter-mcp", "start"], "enabled": true },
"z3-solver": { "type": "stdio", "command": "uv", "args": ["run", "--directory", "lab/12_formal_evolution/z3_mcp", "python", "-m", "z3_mcp.server.main"], "enabled": true },
"arxiv": { "type": "stdio", "command": "uvx", "args": ["arxiv-mcp-server"], "enabled": true },
"lean-lsp": { "type": "stdio", "command": "uvx", "args": ["lean-lsp-mcp"], "enabled": false },
"filesystem": { "type": "stdio", "command": "npx", "args": ["-y", "@modelcontextprotocol/server-filesystem", "."], "enabled": false },
"git": { "type": "stdio", "command": "uvx", "args": ["mcp-server-git", "--repository", "."], "enabled": false },
"mlflow": { "type": "stdio", "command": "uv", "args": ["run", "--with", "mlflow[mcp]>=3.5.1", "mlflow", "mcp", "run"], "enabled": false }
}
}Each server follows the same protocol: transport type, command, arguments, and an enabled flag. The meta-agent reads this at startup, connects all enabled servers, and flattens their tool lists into a unified pool of 20+ callable tools. Toggle any server on or off by flipping a boolean.
The architectural insight: the meta-agent does not know what Z3 is. It does not know what ArXiv is. It discovers smt_solve, check_satisfiability, search_papers, download_paper as opaque callable functions with descriptions. The agent decides at runtime, based on the task, which tools to invoke. Capability emerges from tool diversity, not hardcoded logic.
Cada servidor sigue el mismo protocolo: tipo de transporte, comando, argumentos y una bandera de activación. El meta-agente lee esto al iniciar, conecta todos los servidores activados y aplana sus listas de herramientas en un pool unificado de 20+ herramientas invocables. Activa o desactiva cualquier servidor cambiando un booleano.
La idea arquitectónica: el meta-agente no sabe qué es Z3. No sabe qué es ArXiv. Descubre smt_solve, check_satisfiability, search_papers, download_paper como funciones opacas invocables con descripciones. El agente decide en tiempo de ejecución, basado en la tarea, qué herramientas invocar. La capacidad emerge de la diversidad de herramientas, no de la lógica hardcodeada.
2. The MCPBridge: Tools as DSPy Callables
2. El MCPBridge: Herramientas como Invocables DSPy
The glue that makes this work is MCPBridge (mcp/bridge.py). It converts any MCP server’s tool definitions into Python functions that DSPy’s module types — RLM, ReAct, CodeAct — can invoke naturally:
El pegamento que hace que esto funcione es MCPBridge (mcp/bridge.py). Convierte las definiciones de herramientas de cualquier servidor MCP en funciones de Python que los tipos de módulo de DSPy — RLM, ReAct, CodeAct — pueden invocar de forma natural:
def get_dspy_tools(self) -> list:
fns = []
for td in self.tool_defs:
srv, tn, desc = td["server"], td["name"], td.get("description", "")
def make(srv=srv, tn=tn, desc=desc):
def fn(**kwargs: Any) -> str:
return self.client.call_tool(srv, tn, kwargs)
fn.__name__ = tn
fn.__doc__ = desc
return fn
fns.append(make())
return fnsEach MCP tool becomes a first-class DSPy tool with its original name and description. The RLM module sees smt_solve, reads its description — “Solve SMT constraints and return SAT/UNSAT with model” — and decides to call it, exactly as it would call a web fetch or a code execution. There is no special casing. The bridge is the abstraction that makes zero-code extension possible.
The protocol is bidirectional: the agent calls MCP tools, and MCP servers can push results back. The Z3 solver returns counter-examples; the agent reads them, adjusts its constraints, and re-verifies. This feedback loop is where the formal verification power lives.
Cada herramienta MCP se convierte en una herramienta DSPy de primera clase con su nombre y descripción originales. El módulo RLM ve smt_solve, lee su descripción — “Resuelve restricciones SMT y devuelve SAT/UNSAT con modelo” — y decide invocarla, exactamente como invocaría un fetch web o una ejecución de código. No hay casos especiales. El bridge es la abstracción que hace posible la extensión sin código.
El protocolo es bidireccional: el agente llama a herramientas MCP, y los servidores MCP pueden enviar resultados de vuelta. El Z3 solver devuelve contra-ejemplos; el agente los lee, ajusta sus restricciones y re-verifica. Este bucle de retroalimentación es donde reside el poder de la verificación formal.
3. The SAT/UNSAT Loop: CEGAR in Practice
3. El Bucle SAT/UNSAT: CEGAR en la Práctica
The most consequential pattern Lab 12 enables is the SAT/UNSAT verification loop. An agent proposes a logical constraint system — a financial rewards formula, an IAM policy, a smart contract invariant — and submits it to Z3 for verification. Z3 responds with one of two outcomes:
- UNSAT — No possible assignment satisfies all constraints. No violation can exist. The system is provably correct.
- SAT — A satisfying assignment exists, meaning a violation is possible. Z3 returns a counter-example — specific values that trigger the violation.
When Z3 returns SAT with a counter-example, the agent doesn’t give up. It reads the counter-example, identifies the vulnerable constraint, adjusts the formula, and re-submits. This iterative refinement — Counter-Example Guided Abstraction Refinement (CEGAR) — is a formal methods pattern that the meta-agent implements spontaneously through tool discovery:
El patrón más importante que Lab 12 habilita es el bucle de verificación SAT/UNSAT. Un agente propone un sistema de restricciones lógicas — una fórmula de recompensas financieras, una política IAM, un invariante de smart contract — y lo envía a Z3 para verificación. Z3 responde con uno de dos resultados:
- UNSAT — No existe asignación posible que satisfaga todas las restricciones. No puede existir ninguna violación. El sistema es demostrablemente correcto.
- SAT — Existe una asignación satisfactoria, lo que significa que es posible una violación. Z3 devuelve un contra-ejemplo — valores específicos que desencadenan la violación.
Cuando Z3 devuelve SAT con un contra-ejemplo, el agente no se rinde. Lee el contra-ejemplo, identifica la restricción vulnerable, ajusta la fórmula y re-envía. Este refinamiento iterativo — Refinamiento de Abstracción Guiado por Contra-Ejemplos (CEGAR) — es un patrón de métodos formales que el meta-agente implementa espontáneamente a través del descubrimiento de herramientas:
# Conceptual flow — the meta-agent discovers this pattern naturally
def verify_rewards_formula(formula: str, z3_tool, max_iterations: int = 5):
for i in range(max_iterations):
result = z3_tool(smt_script=formula)
if result["status"] == "UNSAT":
return {"verified": True, "iterations": i}
counter_example = result["model"]
formula = refine_constraints(formula, counter_example)
return {"verified": False, "reason": "Max iterations reached"}Workflow 1 from the README — “Bulletproof Fintech Auditor” — demonstrates this concretely. The agent receives a rewards algorithm, encodes it as SMT-LIB constraints, and iterates with Z3 until UNSAT is returned. The final output is a provably correct rewards formula with a Z3 proof certificate. No stochastic guessing. No hallucinated edge cases. Formal proof.
This is the bridge between stochastic LLMs and deterministic verification. The LLM handles the creative work — proposing constraint systems, interpreting counter-examples, adjusting logic. Z3 handles the provable guarantee. Neuro-symbolic AI, in production.
El Workflow 1 del README — “Bulletproof Fintech Auditor” — demuestra esto concretamente. El agente recibe un algoritmo de recompensas, lo codifica como restricciones SMT-LIB e itera con Z3 hasta que se devuelve UNSAT. El resultado final es una fórmula de recompensas demostrablemente correcta con un certificado de prueba Z3. Sin adivinanzas estocásticas. Sin casos límite alucinados. Prueba formal.
Este es el puente entre los LLMs estocásticos y la verificación determinista. El LLM maneja el trabajo creativo — proponer sistemas de restricciones, interpretar contra-ejemplos, ajustar lógica. Z3 maneja la garantía demostrable. IA neuro-simbólica, en producción.
4. Six Production Workflows
4. Seis Workflows de Producción
The README documents six end-to-end workflows that Lab 12’s tool diversity enables. Each exercises a different combination of MCP servers:
El README documenta seis workflows completos que la diversidad de herramientas de Lab 12 permite. Cada uno ejercita una combinación diferente de servidores MCP:
| Workflow | Servers Used | Outcome |
|---|---|---|
| 1. Bulletproof Fintech Auditor | Z3 solver | Provably correct rewards formula with UNSAT certificate |
| 2. Formal Scientific Researcher | ArXiv → Lean4 → Z3 → Distill | Verified research paper + distilled student model |
| 3. Zero-Trust Security Auditor | OpenRouter (debate) → Z3 (symbolic exec) | Proven no privilege escalation path exists |
| 4. Distributed Systems Audit | ArXiv + crawl4ai + fetch → OpenRouter consensus → Z3 → filesystem/git | Concurrent research + cross-model verification + versioned report |
| 5. Self-Evaluating Distillation | Teacher (all tools) → Z3 → MLflow → Student | Student trained only on formally verified truths |
| 6. Full R&D Lifecycle | ArXiv → crawl4ai → OpenRouter → Z3 → GFL → Distill | End-to-end: research → verify → optimize → ship |
| Workflow | Servidores Usados | Resultado |
|---|---|---|
| 1. Auditor Fintech Blindado | Z3 solver | Fórmula de recompensas correcta con certificado UNSAT |
| 2. Investigador Científico Formal | ArXiv → Lean4 → Z3 → Destilar | Artículo verificado + modelo estudiante destilado |
| 3. Auditor de Seguridad Zero-Trust | OpenRouter (debate) → Z3 (ejecución simbólica) | Ruta de escalación de privilegios demostrablemente inexistente |
| 4. Auditoría de Sistemas Distribuidos | ArXiv + crawl4ai + fetch → consenso OpenRouter → Z3 → filesystem/git | Investigación concurrente + verificación multi-modelo + informe versionado |
| 5. Destilación Auto-Evaluativa | Teacher (todas) → Z3 → MLflow → Student | Estudiante entrenado solo con verdades formalmente verificadas |
| 6. Ciclo I+D Completo | ArXiv → crawl4ai → OpenRouter → Z3 → GFL → Destilar | Completo: investigar → verificar → optimizar → publicar |
Workflow 4 — “Distributed Systems Audit” — is the most architecturally dense. It launches two parallel discovery phases (ArXiv search + web crawl + URL fetch), converges on a research question via OpenRouter consensus across multiple models, runs sequential Z3 verification on each claim, and finally writes a versioned report via filesystem and git tools. The agent orchestrates 5+ concurrent servers, manages state across them, and gates sequential dependencies — all without hardcoded orchestration logic. The meta-agent discovers this execution plan at runtime based on the task description.
El Workflow 4 — “Auditoría de Sistemas Distribuidos” — es el más denso arquitectónicamente. Lanza dos fases de descubrimiento paralelas (búsqueda ArXiv + crawl web + fetch URL), converge en una pregunta de investigación mediante consenso OpenRouter a través de múltiples modelos, ejecuta verificación Z3 secuencial en cada afirmación y finalmente escribe un informe versionado mediante herramientas filesystem y git. El agente orquesta 5+ servidores concurrentes, gestiona el estado entre ellos y controla dependencias secuenciales — todo sin lógica de orquestación hardcodeada. El meta-agente descubre este plan de ejecución en tiempo de ejecución basado en la descripción de la tarea.
5. Self-Evaluating Distillation: Training on Proven Truths
5. Destilación Auto-Evaluativa: Entrenando con Verdades Demostradas
Workflow 5 introduces a pattern that deserves its own section: self-evaluating distillation. The idea is simple but the implications are profound:
- A large “Teacher” agent (with full tool access) solves a problem using Z3 verification
- Only the solutions that pass formal verification (UNSAT) are logged as training data
- A smaller “Student” model is distilled exclusively on this verified dataset
- MLflow tracks teacher-vs-student accuracy across runs
- When student accuracy drops below 0.85 of the teacher’s, the system auto-escalates: re-run the GFL pipeline with fresh training data
This creates a self-purifying dataset — the student never sees unverified or hallucinated content. Every training example carries a Z3 proof certificate. The MLflow observability layer turns the entire system into an experimental science platform:
El Workflow 5 introduce un patrón que merece su propia sección: destilación auto-evaluativa. La idea es simple pero las implicaciones son profundas:
- Un agente “Teacher” grande (con acceso completo a herramientas) resuelve un problema usando verificación Z3
- Solo las soluciones que pasan la verificación formal (UNSAT) se registran como datos de entrenamiento
- Un modelo “Student” más pequeño se destila exclusivamente en este conjunto de datos verificado
- MLflow rastrea la precisión teacher-vs-student entre ejecuciones
- Cuando la precisión del student cae por debajo de 0.85 de la del teacher, el sistema auto-escala: re-ejecuta el pipeline GFL con datos de entrenamiento frescos
Esto crea un conjunto de datos auto-purificante — el student nunca ve contenido no verificado o alucinado. Cada ejemplo de entrenamiento lleva un certificado de prueba Z3. La capa de observabilidad de MLflow convierte todo el sistema en una plataforma de ciencia experimental:
Teacher solves → Z3 verifies (SAT/UNSAT) → MLflow logs → Student distills → Accuracy check → GFL if < 0.85This is the “garbage in, garbage out” problem inverted. Instead of filtering bad data out, the system only lets proven data in. The formal verifier acts as a semantic firewall between training and deployment.
Este es el problema “garbage in, garbage out” invertido. En lugar de filtrar datos malos, el sistema solo deja entrar datos demostrados. El verificador formal actúa como un cortafuegos semántico entre el entrenamiento y el despliegue.
6. Optimization Patterns: Config-Driven Steering
6. Patrones de Optimización: Dirección por Configuración
Beyond the workflows, the README documents six config-driven steering patterns that require zero code changes to apply:
Más allá de los workflows, el README documenta seis patrones de dirección por configuración que no requieren cambios de código para aplicarse:
| Pattern | Mechanism |
|---|---|
| Config Profiles | Swap mcp_servers.json files for domain-specific tool presets (security, research, fintech) |
| Tool Budget Steering | --iterations, --max-llm, --max-agents flags control exploration depth per task |
| Query Engineering | Keywords in the task query (e.g. "verify" + "Z3") map to tool selection via BestOfN analysis |
| Escalation Chains | Automatic fallback: single LLM → Z3 verification → OpenRouter consensus → CoT deep reasoning |
| Multi-Profile Orchestration | Run same task across different config profiles in parallel, compare results |
| GFL Self-Optimization | gfl command: BootstrapFewShot → MIPROv2 → GEPA optimizes agent instructions and tool selection |
| Patrón | Mecanismo |
|---|---|
| Perfiles de Config | Intercambia archivos mcp_servers.json para presets de herramientas por dominio (seguridad, investigación, fintech) |
| Dirección por Presupuesto | Banderas --iterations, --max-llm, --max-agents controlan la profundidad de exploración por tarea |
| Ingeniería de Consultas | Palabras clave en la consulta (ej. "verify" + "Z3") mapean a selección de herramientas mediante análisis BestOfN |
| Cadenas de Escalación | Fallback automático: LLM único → verificación Z3 → consenso OpenRouter → razonamiento profundo CoT |
| Orquestación Multi-Perfil | Ejecuta la misma tarea con diferentes perfiles de configuración en paralelo, compara resultados |
| Auto-Optimización GFL | Comando gfl: BootstrapFewShot → MIPROv2 → GEPA optimiza instrucciones de agentes y selección de herramientas |
7. The Architecture Insight: Substrate Over Tool
7. La Idea Arquitectónica: Sustrato sobre Herramienta
Lab 12 proves something that extends beyond any specific integration. The meta-agent architecture is tool-agnostic by construction. The MCP bridge, the BestOfN task decomposition, the MultiChainComparison agent selection, the GFL optimization pipeline — none of these modules know or care about Z3, Lean4, or ArXiv. They operate on function descriptions and string outputs.
This means the system’s capability ceiling is determined not by what is hardcoded, but by what MCP servers exist in the ecosystem. When a new verification tool, a new data source, or a new computation engine becomes MCP-compatible, it integrates automatically. The system gets more capable without being modified.
The practical implication: building an agentic system today means choosing a substrate — a meta-agent architecture with an MCP bridge and a DSPy optimization loop — and then populating it with domain-specific tools via configuration. The substrate handles the reasoning, the selection, the optimization, and the consolidation. The configuration defines the capabilities.
Lab 12 demuestra algo que va más allá de cualquier integración específica. La arquitectura del meta-agente es agnóstica a las herramientas por construcción. El bridge MCP, la descomposición de tareas BestOfN, la selección de agentes MultiChainComparison, el pipeline de optimización GFL — ninguno de estos módulos sabe o le importa Z3, Lean4 o ArXiv. Operan sobre descripciones de funciones y salidas de texto.
Esto significa que el techo de capacidad del sistema está determinado no por lo que está hardcodeado, sino por qué servidores MCP existen en el ecosistema. Cuando una nueva herramienta de verificación, una nueva fuente de datos o un nuevo motor de cómputo se vuelve compatible con MCP, se integra automáticamente. El sistema se vuelve más capaz sin ser modificado.
La implicación práctica: construir un sistema de agentes hoy significa elegir un sustrato — una arquitectura de meta-agente con un bridge MCP y un bucle de optimización DSPy — y luego poblarlo con herramientas específicas del dominio mediante configuración. El sustrato maneja el razonamiento, la selección, la optimización y la consolidación. La configuración define las capacidades.
How to Run It
Cómo Ejecutarlo
The experiment is available in the lab-experiments repository. To run it:
El experimento está disponible en el repositorio lab-experiments. Para ejecutarlo:
git clone https://github.com/OctAg0nO/lab-experiments
cd lab-experiments
uv sync
cp .env.example .env # Set DEEPSEEK_API_KEY and any other keysThe CLI commands mirror Lab 11:
Los comandos CLI reflejan los de Lab 11:
| Command | Description |
|---|---|
generate | Analyze task and generate agents without executing them |
run | Full pipeline: generate, execute, consolidate |
optimize | Generate agents then run GEPA optimization on each |
gfl | Run the full GFL pipeline comparing all optimizers |
distill | Distill compiled agents to a smaller student model |
distill | Distill compiled agents to a smaller student model |
| Comando | Descripción |
|---|---|
generate | Analizar tarea y generar agentes sin ejecutarlos |
run | Pipeline completo: generar, ejecutar, consolidar |
optimize | Generar agentes y ejecutar optimización GEPA en cada uno |
gfl | Ejecutar el pipeline GFL completo comparando todos los optimizadores |
distill | Destilar agentes compilados a un modelo estudiante más pequeño |
# Fintech auditor workflow — Z3 formal verification
uv run python -m lab.12_formal_evolution --query "Verify this rewards formula: balance * 0.05 if balance > 1000 else balance * 0.01" run
# Self-evaluating distillation with MLflow tracking
uv run python -m lab.12_formal_evolution --query "Prove invariant: total_supply >= sum(all_balances)" distillLab 12 represents a shift from building specific AI tools to architecting a general-purpose agentic substrate. The same meta-agent that researched transformer attention mechanisms in Lab 11 can now prove financial invariants, verify IAM policies, and distill provably correct student models — all because we changed a configuration file.
The meta-agent architecture is not a tool. It is a platform for tool discovery and use. The distinction matters: tools solve specific problems. Platforms enable the solving of problems you haven’t anticipated.
Lab 12 representa un cambio de construir herramientas de IA específicas a arquitecturar un sustrato agéntico de propósito general. El mismo meta-agente que investigó mecanismos de atención en transformers en Lab 11 ahora puede probar invariantes financieros, verificar políticas IAM y destilar modelos estudiante demostrablemente correctos — todo porque cambiamos un archivo de configuración.
La arquitectura del meta-agente no es una herramienta. Es una plataforma para el descubrimiento y uso de herramientas. La distinción importa: las herramientas resuelven problemas específicos. Las plataformas permiten resolver problemas que no anticipaste.
References
Referencias
- Lab 12: Formal Evolution — Lab Experiments Repository. github.com/OctAg0nO/lab-experiments
- Lab 11: Meta-Agent — The foundation Lab 12 extends. github.com/OctAg0nO/lab-experiments
- Building a Meta-Agent — Previous blog post in this series. octagono.org/blog/meta-agent-dspy
- DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines. ICLR 2024 (Spotlight). github.com/stanfordnlp/dspy
- Model Context Protocol — Specification for MCP tool integration. modelcontextprotocol.io
- Z3 Theorem Prover — Microsoft Research. github.com/Z3Prover/z3
- Lean4 Theorem Prover — lean-lang.org
- Lab 12: Evolución Formal — Repositorio de Experimentos. github.com/OctAg0nO/lab-experiments
- Lab 11: Meta-Agent — La fundación que Lab 12 extiende. github.com/OctAg0nO/lab-experiments
- Construyendo un Meta-Agente — Artículo anterior en esta serie. octagono.org/blog/meta-agent-dspy
- DSPy: Compilando Llamadas Declarativas de Modelos de Lenguaje en Pipelines Auto-Mejorables. ICLR 2024 (Spotlight). github.com/stanfordnlp/dspy
- Model Context Protocol — Especificación para integración de herramientas MCP. modelcontextprotocol.io
- Z3 Theorem Prover — Microsoft Research. github.com/Z3Prover/z3
- Lean4 Theorem Prover — lean-lang.org
