--- title: "Arquitectura de Semaprax: Grafo semántico del programa" canonical: https://wavect.io/es/semaprax/architecture/ language: es description: "Arquitectura de Semaprax 0.8.0: ID estables, grafos semánticos comprobados, leyes del código, cambios verificados, agentes tipados y proveedores de desarrollo conectados al compilador." image: "https://wavect.io/img/general/bak/open_graph_preview.jpg" --- ARQUITECTURA · CÓDIGO, SIGNIFICADO, AUTORIDAD # Un modelo de programa que los agentes consultan sin reconstruir el significado desde texto. Primero identidad estable. Después cambios de fuente. El grafo semántico permite consultar declaraciones, tipos, efectos, contratos, propiedad y relaciones de llamadas mediante identidades estables. La versión 0.8.0 amplía ese modelo con leyes del código, reparación protegida de implementaciones, integraciones Rust más completas y un entorno de orquestación. semaprax://architecture v0.8.0 ``` entity Semaprax status beta snapshot 615e501 authority github.com/wavect/semaprax ``` // STATUS ## Estado del repositorio en la instantánea auditada | Instantánea del repositorio | [`615e501`](https://github.com/wavect/semaprax/commit/615e501612895a52b3fdd72a03baf875a8f0df1b) · 2026-10-06. La etiqueta v0.8.0 apunta al commit de código fijado. La CI exacta de la etiqueta terminó correctamente. Esto no garantiza aptitud para producción ni seguridad general. | | --- | --- | | Estado del producto completo | 55 Parcial · 0 Implementado · 0 Faltante | | Contrato de grafo y proyecto | El código canónico, los ID estables y las representaciones comprobadas del compilador conectan leyes, consultas semánticas, cambios y ejecución. Los esquemas de grafo y Project seleccionados por funcionalidad conservan sus propios contratos de admisión, compatibilidad y autoridad del anfitrión. | | Versión beta publicada | [`v0.8.0`](https://github.com/wavect/semaprax/releases/tag/v0.8.0) · Publicada el 6 de octubre de 2026 a las 07:37 UTC. Los 82 trabajos de CI de la etiqueta exacta finalizaron correctamente. Se publicaron tres archivos de la cadena de herramientas, SHA256SUMS, atestaciones por archivo y procedencia agregada firmada. El trabajo de lanzamiento verificó de forma independiente el conjunto firmado antes de publicarlo. Los archivos no están notarizados ni se afirma que las compilaciones sean reproducibles; la verificación sin conexión no acredita el estado actual de revocación. [CI de la etiqueta exacta](https://github.com/wavect/semaprax/actions/runs/37403651320). | | Previews de paquetes y API | La versión incluye perfiles útiles del lenguaje, leyes del programa, orquestación e integración con el sistema anfitrión. La publicación y el soporte de los paquetes Rust/npm generados, las ABI genéricas públicas y otras plataformas siguen requiriendo decisiones independientes. | ## ¿Cómo funciona Semaprax? Semaprax comprueba el código.spx legible y lo resuelve a HIR, su representación tipada del compilador. Las identidades del código y de su significado vinculan consultas, obligaciones de prueba, cambios candidatos y ejecución al programa inspeccionado. Los agentes de programación pueden usar la orquestación alrededor de este núcleo; los Agents en ejecución decodifican propuestas, autorizan efectos y actualizan el estado mediante capacidades suministradas explícitamente por el anfitrión. // 01 ## Primero identidad estable. Después cambios de fuente. ### Código canónico e identidad estable El código.spx legible sigue siendo la representación canónica en Git. Un @id explícito identifica una declaración durante los cambios de nombre admitidos. Las revisiones derivadas del compilador vinculan el código y el preludio seleccionado; las codificaciones del grafo exponen esos hechos sin sustituir el código fuente. ### Contexto limitado y proyecciones compactas Selecciona una declaración, dirección, profundidad, número de nodos y límite de bytes. El contexto de tarea y las proyecciones text, binary o model-text mantienen la comprobación exacta frente a los hechos seleccionados. El gestor nativo de contexto semántico puede usar Graft o Graphify para navegar por el repositorio sin atribuir a un índice externo la autoridad del compilador. ### Leyes del código y reparación protegida de implementaciones Las declaraciones nativas de leyes asignan identidades persistentes a los requisitos contractuales y relacionales. Un LawSet seleccionado por separado fija el inventario completo y la política estricta. Los adaptadores Lean/Z3 instalados prueban las leyes escalares, modulares, estructuradas y de listas admitidas; distinguen los resultados obsoletos, no admitidos, desconocidos y refutados. La reparación candidata debe satisfacer el requisito conservado. ### Cambios semánticos con comprobación de revisiones Inspecciona el contexto, deriva un candidato, examina su impacto y revisión, repite las comprobaciones y autoriza su aplicación. La sustitución acotada de expresiones, los cambios estructurales y la composición especificada mantienen sus límites de operación y revisión. Los cambios en leyes y las reparaciones de implementación siguen reglas de protección distintas. ### Publicación gestionada e integración embebida Las generaciones gestionadas del espacio de trabajo, la evidencia del candidato y los almacenes de revisiones Project vinculan la publicación al candidato comprobado. La API de integración Rust ofrece entradas acotadas y sesiones opacas. Validar varios archivos no actualiza por sí solo archivos arbitrarios, referencias Git ni búferes del editor. ### Lenguaje cotidiano y colecciones Los perfiles admitidos incluyen registros, variantes, clases, herencia, genéricos con inferencia de argumentos acotada, Option/Result, bucles, iteradores, valores de función, cadenas y bytes. `List` inmutable añade operaciones persistentes nil/cons/uncons. Las restricciones generales y las combinaciones arbitrarias siguen necesitando su propia admisión. ### Propiedad y tiempos de vida de callbacks Los valores con propietario, las vistas prestadas, los planes de liberación y ciertas composiciones de recursos son ejecutables. Los perfiles acotados de closures incluyen capturas de Bytes con propietario, copias de valores escalares, estado escalar mutable transaccional y capturas síncronas de texto prestado. Cada perfil comprueba sus reglas de escape, movimiento, reversión y liberación; las relaciones de tiempo de vida más amplias siguen pendientes. ### API Rust con contratos de integración explícitos Los índices preparados de API Rust seleccionan importaciones admitidas y entradas Cargo exactas. Los adaptadores generados de propiedad, vistas prestadas y callbacks conectan código comprobado con consumidores reales de Regex/Url y Serde/iteradores. La integración de Futures en un mismo hilo utiliza un ejecutor controlado por el llamador. Las suposiciones sobre código externo permanecen explícitas; el código de enlace generado no prueba el interior de una crate. ### Agents tipados en ejecución Inicializar, observar, proponer, decodificar, autorizar, ejecutar y reducir. La autorización se repite en cada turno y el reductor elige Continue, Complete, Suspend o Fail. Las rutas de ejecución predeterminadas usan el intérprete; las rutas opcionales de biblioteca aceptan anfitriones de etapas C11 nativas o Core Wasm retenidos por el llamador, con evidencia local acotada de equivalencia. ### Presupuestos, recuperación persistente y llamadas a modelos Los adaptadores explícitos aportan transporte, credenciales y almacenamiento. Los perfiles persistentes confirman la intención antes de despachar y conservan como inciertos los intentos no resueltos. Los límites y registros separan llamadas, trabajo, bytes, tokens y costes. Los reintentos y la conmutación del anfitrión genérico tienen un contrato distinto al de la ruta vinculada de modelo y código; esta última no cambia automáticamente de proveedor ni reintenta trabajo incierto. ### Código reanudable y continuaciones con propiedad El intérprete dispone de yields secuenciales y dependientes del control acotados, conservación selectiva de Bytes con propietario y perfiles persistentes autenticados. El perfil público de Agents con propiedad tiene un ciclo de dos turnos y comprobaciones de reinicio de proceso seleccionadas. Los emisores nativos/Wasm habituales siguen rechazando funciones con yields; quedan pendientes un planificador general y una ABI universal de continuaciones. ### Entorno de desarrollo conectado al compilador La orquestación de la cadena completa coordina tareas explícitas, respuestas del compilador, descriptores de proveedores, bloqueos y confianza por proyecto, selección de modelos, skills y conexiones. Los paquetes oficiales Ponytail/Caveman, los adaptadores Graft/Graphify y las vistas RTK sirven a flujos seleccionados. Los resultados autoritativos de comandos permanecen separados de las salidas compactas dirigidas al modelo. ### Recarga de desarrollo comprobada Una sesión de intérprete retenida admite un candidato, planifica la compatibilidad y lo activa entre invocaciones. El sondeo vigila las entradas declaradas del Project; los cambios inválidos dejan utilizable la revisión activa. Los controles de VS Code muestran el estado activo, pendiente y modificado sin guardar. La migración del diario de Agents definidos en el código es una ruta separada de la cadena completa. ### Perfiles de aplicaciones y agentes económicos Un servicio de referencia combina decisiones comprobadas de sesiones, tareas y trabajos con un anfitrión de instantáneas, HTTP/TLS explícito y telemetría seleccionada de eventos JSON u OTLP. El recorrido aceptado con Linux/Podman mantiene un alcance acotado; se rechazan los adaptadores SQL. Los agentes económicos conservan en el anfitrión el control de la cartera, aprobación, firma y conciliación. ### Paquetes generados y confianza en registros locales Los perfiles Project de datos con propiedad y un endpoint Wasm genérico privado del compilador tienen evidencia de consumidores generados. El soporte genérico público sigue sin estar admitido ni publicado. Los metadatos firmados del registro local, las generaciones retenidas y las lecturas vinculadas al bloqueo no proporcionan por sí solos un registro de paquetes alojado ni autoridad para descargar por red. ### Pruebas y procedencia del lanzamiento El trabajo Lean de la etiqueta exacta comprueba su núcleo formal acotado y la exportación de obligaciones. Los trabajos de lanzamiento atestiguan por separado los tres archivos y firman y verifican la procedencia agregada. Son cadenas de evidencia distintas; ninguna demuestra la corrección de todo el lenguaje, notarización ni compilaciones reproducibles entre anfitriones. // 02 ## La proyección de código sigue siendo legible ``` module examples.meaning; @id("math.add") fn add(left: i64, right: i64) -> i64 requires left >= 0 requires right >= 0 ensures result == left + right { left + right } @id("app.main") fn main() -> i64 ensures result == 42 { add(19, 23) } ``` Revisado frente a la etiqueta v0.8.0 y su commit de código fijado. Las especificaciones versionadas definen admisión y autoridad; los títulos de versiones anteriores en la matriz y el roadmap son históricos. [GitHub repository](https://github.com/wavect/semaprax). // DOCS ## Abre el manual de Semaprax El manual en línea es la guía en inglés publicada desde main y puede incluir cambios posteriores a 0.8.0. Utiliza la copia fijada a la revisión al reproducir esta versión. ### [Manual en línea](https://wavect.github.io/semaprax/) La ruta de aprendizaje actual en inglés, publicada desde main. ### [Copia del manual de 0.8.0](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/handbook/README.md) Los archivos del manual en el commit exacto del lanzamiento revisado. ### [Crea tu primer proyecto](https://wavect.github.io/semaprax/getting-started/first-project.html) Guía actual en inglés del manifiesto, las comprobaciones, las pruebas y las compilaciones de la calculadora. ### [Aprende lo esencial del lenguaje](https://wavect.github.io/semaprax/language/essentials.html) Introducción actual en inglés a valores, funciones y estructura del código. ### [Trabaja con un agente de programación](https://wavect.github.io/semaprax/practices/agents.html) Guía actual en inglés de contexto semántico y flujos seguros de cambios. ### [Referencia de la CLI para 0.8.0](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/CLI-GUIDE.md) Comandos fijados a la revisión y límites entre la CLI independiente y la cadena completa. ### [Extensión de VS Code](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/editors/vscode/README.md) Configuración, navegación semántica, revisión y controles de desarrollo fijados a la revisión. ### [Ejemplos ejecutables](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/examples/README.md) Ejemplos fijados a la revisión para el lenguaje, proyectos, leyes, Agents e integraciones con el anfitrión. // REF ## Fuentes primarias de esta página Revisado frente a la etiqueta v0.8.0 y su commit de código fijado. Las especificaciones versionadas definen admisión y autoridad; los títulos de versiones anteriores en la matriz y el roadmap son históricos. 1. [Arquitectura del compilador y límites de confianza](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md) 2. [Implementación del grafo semántico](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/src/graph.rs) 3. [Leyes nativas en el código fuente](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/NATIVE-LAW-DECLARATIONS-V1.md) 4. [Garantías estrictas sobre las leyes seleccionadas](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/STRICT-LAW-ASSURANCE-V1.md) 5. [Perfiles instalados de Lean y Z3](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/INSTALLED-PROOF-TOOLS-V1.md) 6. [Orquestación, proveedores, registros del modelo y construcción de prompts](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/HARNESS-PROVIDER-V1.md) 7. [Ejecución y límites actuales de implementación](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/COMPLETION-MATRIX.md) 8. [Continuaciones reanudables del código](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/RESUMABLE-EFFECTS-CONTINUATION-V1.md) 9. [Entrada pública de Agents con propiedad definida en el código](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/SOURCE-AGENT-OWNED-WAIT-PUBLIC-V1.md) 10. [Sesión de recarga en caliente comprobada](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/HOT-RELOAD-SESSION-V1.md) 11. [Anfitrión del servicio de referencia](https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/REFERENCE-SERVICE-HOST-V1.md) // FAQ ## Preguntas y respuestas prácticas ### ¿El grafo semántico es un knowledge graph o RAG? El compilador deriva el grafo central del código comprobado, con declaraciones, tipos, contratos y relaciones estables. La orquestación puede usar también Graft o Graphify para navegar por el repositorio. Esos índices externos complementan los hechos semánticos del compilador y no sustituyen sus reglas de revisión y validación. ### ¿Un agente puede editar cualquier programa con parches semánticos? La cadena expone operaciones de edición concretas vinculadas a revisiones, revisión de candidatos y repetición de comprobaciones. Los inventarios protegidos de leyes mantienen separados los requisitos y los cuerpos de implementación editables. Un agente debe usar una operación admitida y una ruta de aplicación autorizada; una consulta de contexto o una prueba correcta no da permiso para sobrescribir archivos arbitrarios. Proyecto de investigación de Wavect: [Wavect GmbH](/es/). Creado por Wavect como proyecto de investigación de sistemas de código abierto. ## Structured Data ```json { "@context": "https://schema.org", "@graph": [ { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ], "employee": [ { "@id": "https://wavect.io/team/kevin-riedl/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Kevin Riedl", "url": "https://wavect.io/team/kevin-riedl/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } }, { "@id": "https://wavect.io/team/christof-jori/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Christof Jori", "url": "https://wavect.io/team/christof-jori/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } } ], "founder": [ { "@id": "https://wavect.io/team/kevin-riedl/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Kevin Riedl", "url": "https://wavect.io/team/kevin-riedl/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } }, { "@id": "https://wavect.io/team/christof-jori/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Christof Jori", "url": "https://wavect.io/team/christof-jori/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } } ], "legalRepresentative": [ { "@id": "https://wavect.io/team/kevin-riedl/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Kevin Riedl", "url": "https://wavect.io/team/kevin-riedl/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } }, { "@id": "https://wavect.io/team/christof-jori/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Christof Jori", "url": "https://wavect.io/team/christof-jori/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } } ], "name": "Wavect GmbH", "subjectOf": { "@id": "https://wavect.io/verified-claims.json#dataset", "@type": "Dataset", "creator": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "description": "A machine-readable registry of quantitative and qualitative claims published by Wavect, with review dates, localized page appearances and public third-party citations where available.", "inLanguage": "en", "isAccessibleForFree": true, "license": "https://creativecommons.org/licenses/by/4.0/", "name": "Wavect verified publication claims", "url": "https://wavect.io/verified-claims.json" }, "url": "https://wavect.io/" }, { "@id": "https://wavect.io/team/kevin-riedl/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Kevin Riedl", "sameAs": [ "https://www.wikidata.org/wiki/Q139796365", "https://www.linkedin.com/in/wsdt", "https://github.com/wsdt" ], "url": "https://wavect.io/team/kevin-riedl/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } }, { "@id": "https://wavect.io/team/christof-jori/#person", "@type": "Person", "jobTitle": "Managing Director", "name": "Christof Jori", "sameAs": [ "https://www.wikidata.org/wiki/Q139796367", "https://www.linkedin.com/in/jocr77/", "https://github.com/jo-chris" ], "url": "https://wavect.io/team/christof-jori/", "worksFor": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] } }, { "@id": "https://wavect.io/#website", "@type": "WebSite", "inLanguage": [ "en", "de", "es", "zh" ], "name": "Wavect", "potentialAction": { "@type": "SearchAction", "query-input": "required name=search_term_string", "target": { "@type": "EntryPoint", "urlTemplate": "https://wavect.io/search/?q={search_term_string}" } }, "publisher": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "url": "https://wavect.io/" }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v02-semantic-graph-patches", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v02-semantic-graph-patches", "inLanguage": "en", "text": "Semaprax v0.8.0 retains canonical .spx source and validated semantic identities, bounded context queries and revision-bound semantic changes. The exact-tag workflow succeeded; admitted edit families and public support remain separately scoped." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v02-bounded-project-agent-surfaces", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/COMPLETION-MATRIX.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v02-bounded-project-agent-surfaces", "inLanguage": "en", "text": "Semaprax v0.8.0 includes multi-module Projects, typed iterative source Agents, explicit host-model integration, durable recovery and a compiler-assisted development harness. Generated Project v8-v11 packages and public ABI support require separate promotion and publication decisions." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v02-managed-workspace-operations", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v02-managed-workspace-operations", "inLanguage": "en", "text": "Semaprax v0.8.0 includes bounded semantic changes, managed workspace/revision workflows and evidence-based review. Read-only tools and receipts do not authorize arbitrary filesystem, Git or publication operations." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v060-resumable-effects-boundary", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/RESUMABLE-EFFECTS-V1.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v060-resumable-effects-boundary", "inLanguage": "en", "text": "Semaprax v0.8.0 implements bounded source yield and resume profiles, including separately admitted control-dependent and owned-frame routes. Ordinary native and Wasm emitters, durable execution and Rust Future integration retain distinct admission and execution boundaries." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v060-local-registry-trust", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/PACKAGE-REGISTRY-TRUST-V2.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v060-local-registry-trust", "inLanguage": "en", "text": "Semaprax v0.8.0 implements signed Registry-v3 snapshots, held generations and lock-bound local reads; this is not a hosted public registry service." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v060-hosted-lean-proof-gate", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/actions/runs/37403651320" }, "dateModified": "2026-10-06", "identifier": "semaprax-v060-hosted-lean-proof-gate", "inLanguage": "en", "text": "The Semaprax v0.8.0 exact-tag CI includes a successful hosted Lean proof job for the pinned obligation kernel; it does not prove the entire language safe." } ] } ``` ```json { "@context": "https://schema.org", "@graph": [ { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "citation": [ { "@type": "CreativeWork", "name": "Arquitectura del compilador y límites de confianza", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md" }, { "@type": "CreativeWork", "name": "Implementación del grafo semántico", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/src/graph.rs" }, { "@type": "CreativeWork", "name": "Leyes nativas en el código fuente", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/NATIVE-LAW-DECLARATIONS-V1.md" }, { "@type": "CreativeWork", "name": "Garantías estrictas sobre las leyes seleccionadas", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/STRICT-LAW-ASSURANCE-V1.md" }, { "@type": "CreativeWork", "name": "Perfiles instalados de Lean y Z3", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/INSTALLED-PROOF-TOOLS-V1.md" }, { "@type": "CreativeWork", "name": "Orquestación, proveedores, registros del modelo y construcción de prompts", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/HARNESS-PROVIDER-V1.md" }, { "@type": "CreativeWork", "name": "Ejecución y límites actuales de implementación", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/COMPLETION-MATRIX.md" }, { "@type": "CreativeWork", "name": "Continuaciones reanudables del código", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/RESUMABLE-EFFECTS-CONTINUATION-V1.md" }, { "@type": "CreativeWork", "name": "Entrada pública de Agents con propiedad definida en el código", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/SOURCE-AGENT-OWNED-WAIT-PUBLIC-V1.md" }, { "@type": "CreativeWork", "name": "Sesión de recarga en caliente comprobada", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/HOT-RELOAD-SESSION-V1.md" }, { "@type": "CreativeWork", "name": "Anfitrión del servicio de referencia", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/REFERENCE-SERVICE-HOST-V1.md" } ], "creator": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "dateModified": "2026-10-06", "description": "Arquitectura de Semaprax 0.8.0: ID estables, grafos semánticos comprobados, leyes del código, cambios verificados, agentes tipados y proveedores de desarrollo conectados al compilador.", "inLanguage": "es", "mainEntity": { "@id": "https://wavect.io/es/semaprax/architecture/#article", "@type": "TechArticle" }, "name": "Arquitectura de Semaprax: Grafo semántico del programa | Wavect", "url": "https://wavect.io/es/semaprax/architecture/" }, { "@id": "https://wavect.io/es/semaprax/architecture/#article", "@type": "TechArticle", "about": { "@id": "https://wavect.io/semaprax/#software", "@type": "SoftwareSourceCode" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": [ { "@type": "CreativeWork", "name": "Arquitectura del compilador y límites de confianza", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md" }, { "@type": "CreativeWork", "name": "Implementación del grafo semántico", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/src/graph.rs" }, { "@type": "CreativeWork", "name": "Leyes nativas en el código fuente", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/NATIVE-LAW-DECLARATIONS-V1.md" }, { "@type": "CreativeWork", "name": "Garantías estrictas sobre las leyes seleccionadas", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/STRICT-LAW-ASSURANCE-V1.md" }, { "@type": "CreativeWork", "name": "Perfiles instalados de Lean y Z3", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/INSTALLED-PROOF-TOOLS-V1.md" }, { "@type": "CreativeWork", "name": "Orquestación, proveedores, registros del modelo y construcción de prompts", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/HARNESS-PROVIDER-V1.md" }, { "@type": "CreativeWork", "name": "Ejecución y límites actuales de implementación", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/COMPLETION-MATRIX.md" }, { "@type": "CreativeWork", "name": "Continuaciones reanudables del código", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/RESUMABLE-EFFECTS-CONTINUATION-V1.md" }, { "@type": "CreativeWork", "name": "Entrada pública de Agents con propiedad definida en el código", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/SOURCE-AGENT-OWNED-WAIT-PUBLIC-V1.md" }, { "@type": "CreativeWork", "name": "Sesión de recarga en caliente comprobada", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/HOT-RELOAD-SESSION-V1.md" }, { "@type": "CreativeWork", "name": "Anfitrión del servicio de referencia", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/REFERENCE-SERVICE-HOST-V1.md" } ], "dateModified": "2026-10-06", "datePublished": "2026-08-11", "description": "Arquitectura de Semaprax 0.8.0: ID estables, grafos semánticos comprobados, leyes del código, cambios verificados, agentes tipados y proveedores de desarrollo conectados al compilador.", "headline": "Un modelo de programa que los agentes consultan sin reconstruir el significado desde texto.", "inLanguage": "es", "isPartOf": { "@id": "https://wavect.io/semaprax/#webpage", "@type": "WebPage" }, "mainEntityOfPage": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage" }, "publisher": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "url": "https://wavect.io/es/semaprax/architecture/" }, { "@id": "https://wavect.io/semaprax/#software", "@type": "SoftwareSourceCode" }, { "@id": "https://wavect.io/es/semaprax/architecture/#faq", "@type": "FAQPage", "inLanguage": "es", "mainEntity": [ { "@type": "Question", "acceptedAnswer": { "@type": "Answer", "text": "El compilador deriva el grafo central del código comprobado, con declaraciones, tipos, contratos y relaciones estables. La orquestación puede usar también Graft o Graphify para navegar por el repositorio. Esos índices externos complementan los hechos semánticos del compilador y no sustituyen sus reglas de revisión y validación." }, "name": "¿El grafo semántico es un knowledge graph o RAG?" }, { "@type": "Question", "acceptedAnswer": { "@type": "Answer", "text": "La cadena expone operaciones de edición concretas vinculadas a revisiones, revisión de candidatos y repetición de comprobaciones. Los inventarios protegidos de leyes mantienen separados los requisitos y los cuerpos de implementación editables. Un agente debe usar una operación admitida y una ruta de aplicación autorizada; una consulta de contexto o una prueba correcta no da permiso para sobrescribir archivos arbitrarios." }, "name": "¿Un agente puede editar cualquier programa con parches semánticos?" } ], "url": "https://wavect.io/es/semaprax/architecture/" }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v02-semantic-graph-patches", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v02-semantic-graph-patches", "inLanguage": "en", "text": "Semaprax v0.8.0 retains canonical .spx source and validated semantic identities, bounded context queries and revision-bound semantic changes. The exact-tag workflow succeeded; admitted edit families and public support remain separately scoped." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v02-bounded-project-agent-surfaces", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/COMPLETION-MATRIX.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v02-bounded-project-agent-surfaces", "inLanguage": "en", "text": "Semaprax v0.8.0 includes multi-module Projects, typed iterative source Agents, explicit host-model integration, durable recovery and a compiler-assisted development harness. Generated Project v8-v11 packages and public ABI support require separate promotion and publication decisions." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v02-managed-workspace-operations", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/ARCHITECTURE.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v02-managed-workspace-operations", "inLanguage": "en", "text": "Semaprax v0.8.0 includes bounded semantic changes, managed workspace/revision workflows and evidence-based review. Read-only tools and receipts do not authorize arbitrary filesystem, Git or publication operations." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v060-resumable-effects-boundary", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/RESUMABLE-EFFECTS-V1.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v060-resumable-effects-boundary", "inLanguage": "en", "text": "Semaprax v0.8.0 implements bounded source yield and resume profiles, including separately admitted control-dependent and owned-frame routes. Ordinary native and Wasm emitters, durable execution and Rust Future integration retain distinct admission and execution boundaries." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v060-local-registry-trust", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/blob/615e501612895a52b3fdd72a03baf875a8f0df1b/docs/PACKAGE-REGISTRY-TRUST-V2.md" }, "dateModified": "2026-10-06", "identifier": "semaprax-v060-local-registry-trust", "inLanguage": "en", "text": "Semaprax v0.8.0 implements signed Registry-v3 snapshots, held generations and lock-bound local reads; this is not a hosted public registry service." }, { "@id": "https://wavect.io/verified-claims.json#semaprax-v060-hosted-lean-proof-gate", "@type": "Claim", "appearance": { "@id": "https://wavect.io/es/semaprax/architecture/#webpage", "@type": "WebPage", "inLanguage": "es", "url": "https://wavect.io/es/semaprax/architecture/" }, "author": { "@id": "https://wavect.io/#organization", "@type": [ "Organization", "ProfessionalService", "LocalBusiness" ] }, "citation": { "@type": "WebPage", "url": "https://github.com/wavect/semaprax/actions/runs/37403651320" }, "dateModified": "2026-10-06", "identifier": "semaprax-v060-hosted-lean-proof-gate", "inLanguage": "en", "text": "The Semaprax v0.8.0 exact-tag CI includes a successful hosted Lean proof job for the pinned obligation kernel; it does not prove the entire language safe." } ] } ``` ```json { "@context": "https://schema.org", "@type": "BreadcrumbList", "itemListElement": [ { "@type": "ListItem", "item": "https://wavect.io/es/", "name": "Inicio", "position": 1 }, { "@type": "ListItem", "item": "https://wavect.io/es/semaprax/", "name": "Semaprax", "position": 2 }, { "@type": "ListItem", "item": "https://wavect.io/es/semaprax/architecture/", "name": "Un modelo de programa que los agentes consultan sin reconstruir el significado desde texto.", "position": 3 } ] } ```