Leyes junto al código
Declara leyes estables, selecciona el inventario de pruebas y vuelve a comprobar las obligaciones admitidas de Lean/Z3. Repara los cuerpos de implementación sin alterar el requisito que deben cumplir.
EvidenciaV0.8.0 BETA · APACHE-2.0
El lenguaje de sistemas creado para agentes de código y legible por personas.
Código legible. Significado consultable. Cambios comprobados.
Ofrece a los agentes de programación los tipos, contratos y relaciones de tu código. Semaprax 0.8.0 reúne leyes y herramientas de prueba, una integración más amplia con Rust, un entorno de orquestación, recarga comprobada e informes de tokens por tarea en una sola cadena de herramientas beta. Empieza con un programa pequeño y conecta después las piezas que necesita tu proyecto.
revision sha256:<program-state>
query app.main --depth 1
context typed · bounded · stable-id
patch expected_revision == current
verify fail_closed
target native | browser/wasm// STATUS
Estado del repositorio en la instantánea auditada
| Instantánea del repositorio | 615e501 · 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 · 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. |
| 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. |
¿Qué es Semaprax?
Semaprax es un lenguaje de programación de sistemas de código abierto, diseñado para agentes y en fase beta. El código .spx legible permanece en Git mientras los agentes de programación consultan su significado tipado, comprueban las leyes del programa y proponen cambios vinculados a una revisión. La versión 0.8.0 también incluye Agents tipados en ejecución, un entorno de orquestación conectado al compilador e integraciones acotadas con Rust, código nativo y WebAssembly.
// v0.8.0
Qué cambia en v0.8.0
Seis avances prácticos en el código de 0.8.0 y en la cadena de herramientas beta publicada.
Una integración más amplia con Rust
Las API Rust seleccionadas, los adaptadores de propiedad y callbacks generados, y las aplicaciones reales con Regex/Url, Serde/iteradores y Tokio/reqwest amplían la integración más allá de las demostraciones escalares.
EvidenciaOrquestación conectada al compilador
Combina contexto semántico con proveedores seleccionados por proyecto, Graft/Graphify, vistas RTK, skills oficiales de Ponytail/Caveman y políticas explícitas de selección de modelos.
EvidenciaRecarga de desarrollo comprobada
El comando dev y los controles de VS Code validan candidatos, esperan un punto seguro de activación y conservan el programa activo tras un cambio inválido.
EvidenciaInformes de tokens y coste por tarea
Compara los datos exactos de contexto, examina aumentos y reducciones durante una sesión y distingue los registros del proveedor de las reservas y los costes estimados.
EvidenciaUn conjunto de archivos de lanzamiento verificado
Los 82 trabajos de la etiqueta exacta finalizaron correctamente. Los tres archivos precompilados incluyen sumas de comprobación, atestaciones de compilación y procedencia firmada verificada de forma independiente.
Evidencia// v0.8.0
¿Prefieres una herramienta de línea de comandos precompilada?
La versión 0.8.0 publica archivos para macOS con Apple Silicon, Linux x86-64 GNU y Windows x86-64 MSVC. Esta versión no incluye un instalador gráfico. Cada archivo contiene la cadena completa con el nombre semaprax, además de semapraxd y un ejemplo de comprobación. La instalación desde el código conserva el nombre separado semaprax-full para la compilación completa.
macOS · Apple Silicon
aarch64-apple-darwin
Linux · x86-64 (GNU)
x86_64-unknown-linux-gnu
Windows · x86-64 (MSVC)
x86_64-pc-windows-msvc
- Elige el archivo que corresponda a tu sistema operativo y CPU. Las descargas Source code de GitHub son copias del repositorio, no ejecutables precompilados.
- Comprueba SHA256SUMS antes de extraer el archivo de tu plataforma. Añade el directorio extraído a PATH o ejecuta semaprax mediante su ruta completa.
- Ejecuta
semaprax --versiony después comprueba y ejecutasmoke/meaning.spxdesde el directorio extraído. Devuelve 42. Las compilaciones nativas necesitan Clang; los ejemplos web utilizan Node.js 22+. - Para verificar la procedencia firmada, reúne los tres archivos de las plataformas y los metadatos firmados en un directorio y sigue las instrucciones enlazadas de
semaprax release verify <release-dir>. El resultado debe confirmar la verificación criptográfica sin conexión; una verificación correcta sin firma no valida ninguna firma.
SHA256SUMS · Sumas de comprobación y procedencia firmada · Manifiesto del lanzamiento · Registro de publicación
// CLI
Ejecuta tu primer programa validado
Ruta desde código fijada al commit revisado. Requiere Git y Rust/Cargo 1.88+. Cargo puede descargar dependencias al comenzar. Estos comandos check/run no necesitan Clang, Node.js ni proveedor de IA; el programa devuelve 42.
git clone https://github.com/wavect/semaprax.git
cd semaprax
git checkout --detach 615e501612895a52b3fdd72a03baf875a8f0df1b
cargo run --locked -p semaprax -- check examples/meaning.spx
cargo run --locked -p semaprax -- run examples/meaning.spx// PROJECT
Instala una vez y crea un proyecto
Continúa en la misma copia del repositorio fijada a la revisión indicada. Cargo instala la CLI independiente; la línea PATH de abajo sirve para Bash y Zsh. La calculadora generada incluye código, manifiesto, pruebas y AGENTS.md. Elige un destino nuevo: new utiliza archivos incluidos y no inicializa Git ni contacta con un registro de paquetes.
cargo install --locked --path . --bin semaprax
export PATH="$HOME/.cargo/bin:$PATH"
semaprax --version
semaprax new first-semaprax
semaprax check first-semaprax/semaprax.toml
semaprax test first-semaprax/semaprax.toml
semaprax run first-semaprax/semaprax.toml// AGENT
Da a tu agente de programación un punto de partida preciso
Desde la raíz del repositorio, inspecciona el mismo programa mediante su identidad estable. Graph, context y la ayuda del lenguaje instalada son puntos de partida de solo lectura. Un cambio semántico posterior necesita la revisión actual, una operación admitida y un paso explícito de aplicación.
semaprax graph examples/meaning.spx
semaprax context examples/meaning.spx app.main --depth 1 --max-bytes 65536 --max-nodes 256
semaprax context examples/meaning.spx math.add --depth 1 --filters contracts
semaprax help language
semaprax help diagnostic SPX-T208// 01
Un programa, tres superficies conectadas
Las personas editan código legible, las herramientas consultan su significado comprobado y los destinos compatibles ejecutan el programa admitido. Cada destino e integración indica qué características del lenguaje acepta.
- Código legibleArchivos .spx canónicos, ID estables de declaraciones, contratos, leyes y propiedad explícita. Los comandos habituales check y run no necesitan una cuenta de un proveedor de modelos.
- Significado comprobado para las herramientasContexto derivado del compilador, análisis de impacto, revisión de candidatos y obligaciones de prueba. El entorno de orquestación puede incorporar recuperación de información, skills y proveedores de modelos seleccionados alrededor de ese núcleo semántico.
- Ejecución controladaIntérprete, perfiles admitidos de C11/Clang y Core Wasm, y Agents tipados cuyas propuestas del modelo pasan por una autorización determinista antes de producir efectos.
Grafo semántico del programa de 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.
// 02
Facilita la comprobación de cada cambio propuesto
Las identidades estables permiten dirigir un cambio a una declaración concreta. El contexto acotado explica su función. Los contratos y las leyes seleccionadas por separado limitan la implementación, mientras que la revisión de candidatos y la repetición de comprobaciones verifican el cambio antes de aplicarlo. El entorno registra el uso real y los resultados de las tareas para contrastar las afirmaciones de eficiencia con evidencia.
MIDE EL RESULTADO
Menos ambigüedad al reparar, con el coste y la corrección de cada tarea comprobados por separado
// 03
Sigue la pregunta que necesitas resolver
Consulta el manual para los pasos prácticos, la arquitectura para el modelo de programación, la evidencia para los perfiles implementados, los benchmarks para las mediciones y la interoperabilidad para conectar con tu tecnología actual.
architecture
Arquitectura
Leyes del código, grafos semánticos, Agents y orquestación
evidenceEvidencia
Qué implementa v0.8.0 y cuáles son sus límites
benchmarksBenchmarks
Tokens medidos, coste por tarea y rendimiento
interoperabilityInteroperabilidad
Matriz de objetivos y ecosistemas
roadmapRoadmap
Hitos, objetivos y brechas abiertas
// 04
Registro de evidencia de capacidades
| Estado actual | Evidence state | Alcance | Evidencia |
|---|---|---|---|
| Código canónico e identidad estable | Parcial | El código `.spx` legible sigue siendo canónico en Git. Los valores `@id` identifican declaraciones independientemente de cambios de nombre admitidos. La revisión vincula código canónico y prelude implícito del compilador, no posiciones accidentales ni el formato serializado del grafo. | GitHub repository |
| Contexto limitado y proyecciones compactas | Parcial | Selecciona el contexto exacto del grafo o de la tarea con límites de profundidad, dirección, nodos y bytes. Model-text v2 reduce tokens en algunas entradas grandes y los aumenta en las pequeñas; los informes conservan el tokenizador y el límite de comparación. | GitHub repository |
| Cambios semánticos, no reescrituras arbitrarias | Parcial | Inspeccionar contexto, derivar candidato, revisar impacto, reproducir comprobaciones y autorizar la aplicación explícitamente. Además de renombrar hay reemplazo limitado de expresiones, cambios estructurales y composición rebase/merge definida. Cada protocolo conserva sus límites de revisión, identidad y operación. | GitHub repository |
| La publicación controlada es un límite independiente | Parcial | Las generaciones de workspace, evidencia de candidatos, almacén de revisiones y flujos MCP mantienen autoridad explícita de escritura y publicación. Validar varios archivos no actualiza atómicamente rutas arbitrarias, Git o editores. La API de integración Rust ofrece límites, cancelación y sesiones opacas, no acceso libre al host. | GitHub repository |
| Evidencia semántica reproducible | Parcial | La evidencia liga hechos validados y cambios candidatos a fuentes y revisiones. Un recibo apoya revisión o rechazo, pero no otorga autoridad para ejecutar, modificar o publicar. | GitHub repository |
| Proyectos multimódulo y plantillas offline | Parcial | Los manifiestos definen el código, las entradas, las pruebas y las exportaciones declaradas. Las plantillas incluidas de calculadora, biblioteca y servicio tienen sus propios perfiles. new crea un proyecto nuevo a partir de archivos integrados; las comprobaciones del código, las pruebas interpretadas y las compilaciones siguen el contrato del manifiesto seleccionado. | GitHub repository |
// 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
La ruta de aprendizaje actual en inglés, publicada desde main.
Copia del manual de 0.8.0
Los archivos del manual en el commit exacto del lanzamiento revisado.
Crea tu primer proyecto
Guía actual en inglés del manifiesto, las comprobaciones, las pruebas y las compilaciones de la calculadora.
Aprende lo esencial del lenguaje
Introducción actual en inglés a valores, funciones y estructura del código.
Trabaja con un agente de programación
Guía actual en inglés de contexto semántico y flujos seguros de cambios.
Referencia de la CLI para 0.8.0
Comandos fijados a la revisión y límites entre la CLI independiente y la cadena completa.
Extensión de VS Code
Configuración, navegación semántica, revisión y controles de desarrollo fijados a la revisión.
Ejemplos ejecutables
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.
- Versión v0.8.0 y descargas por plataforma
- CI de la etiqueta exacta y evidencia del lanzamiento
- Manual correspondiente al código revisado
- Declaraciones de leyes en el código
- Integración nativa ampliada con Rust
- Proveedores de orquestación y registros de los modelos
- Flujo de recarga en caliente comprobada
- Informes de tokens y reutilización del trabajo comprobado
- Matriz de objetivos completos y límites pendientes
- Procedencia firmada y verificación independiente
// FAQ
Preguntas y respuestas prácticas
¿Semaprax está listo para producción?
La versión 0.8.0 es una beta Apache-2.0 publicada el 6 de octubre de 2026. Puedes instalarla, ejecutar programas y explorar sus perfiles implementados. Un lanzamiento correcto de la etiqueta exacta no acredita soporte de producción; la matriz de objetivos completos sigue registrando 55 requisitos Parciales.
¿Semaprax es solo para agentes de IA?
Puedes escribir, comprobar y ejecutar programas .spx habituales sin un modelo de IA ni una cuenta. Los agentes de programación usan contexto semántico y cambios admitidos mediante las herramientas; los Agents definidos en el código son otra abstracción de programación tipada. El manual en inglés explica ambos usos.
¿Tu producto de IA necesita ingeniería con este nivel de evidencia?
Ver el trabajo de ingeniería de IA de Wavect.Creado por Wavect como proyecto de investigación de sistemas de código abierto. GitHub repository. 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.