[0x00..0x3F] magic = b"RUL\x00\x01\x00\x00\x00" · IR Binario de 128 Bits
Release v0.4.0 (2026-11-07) ↗

El lenguaje de programación binario de 128 bits para agentes de IA.

La IA piensa en números y las CPU ejecutan binario; sin embargo, C, Go y Rust obligan a la IA a teclear texto humano y esperar segundos a que un compilador adivine qué quiso decir. Rul (.rl) elimina ese intermediario de texto: la IA emite bloques binarios fijos de 16 bytes con el Algoritmo, la Planificación de CPU y el Ticket de Seguridad de Memoria desde el inicio. Resultado: verificación en 5,8 ns, compilación autónoma en 6,4 µs y ejecución 4,72 veces más rápida que C escrito a mano.

PRIMEROS PRINCIPIOS EN 10 SEGUNDOS · ELIMINAR EL INTERMEDIARIO DE TEXTO
✗ VÍA ANTIGUA (C / Go / Rust) La IA piensa (Números) → Escribe texto humano → El compilador analiza y adivina (Segundos) → Código máquina (0/1)
✓ PRIMEROS PRINCIPIOS RUL (.rl) La IA piensa (Números) → Emite bloque binario de 16 bytes (5,8 ns prueba + 6,4 µs compilación) → 4,72x más rápido que C
Bloque binario de 16 bytes (0ms parseo) + 6,4 µs ELF64 nativo (Cero LLVM) + 5,8 ns Prueba de seguridad (O(N) lineal)
# 1. Install standalone rul binary (0 rustc/LLVM runtime deps)
$ curl -fsSL https://raw.githubusercontent.com/rul-lang/rul/main/install.sh | sh

# 2. Scaffold, O(N) verify in ~5.8ns/node, compile 817B ELF64 & trace
$ rul new my-ai-pipeline && cd my-ai-pipeline
$ rul check   # ✓ Verified 7 SSA nodes in 0.04 µs (CAP_NONE = 0x0)
$ rul run     # ✓ Compiled 817-byte ELF64 in 6.4 µs -> Output: 77999800.0
$ rul trace   # ✓ White-Box Inspector: #0..#6 (NaN/Inf = 0)
IMAGEN BINARIA .RL EN VIVO · 7 NODOS SSA = 208 BYTES -> ELF64 DE 817 BYTES CAP_NONE=0x0

Haz clic en cualquier trama de instrucción de 16 bytes abajo para decodificar sus bits, prueba y traza:

RulHeader
64 Bytes (0x00..0x3F)
Arena[0] + Proof[0]
32 Bytes (0x40..0x5F)
NodeFrame[0..6]
112 Bytes (7 × 16B)
Artifact (.rl) = Algorithm + Schedule + Proof ✓ 5.78 ns/node
[0x40] Trama de 128 bits
16 Bytes

Cada instrucción es un bloque binario fijo · 0 ms de análisis de texto

[0x50] por instrucción
5,78 ns

Prueba instantánea de memoria y límites (Un solo pase O(N))

[0x60] compilación nativa
6,4 µs

Ejecutable autónomo Linux x86_64 ELF64 sin LLVM

[0x70] 4,72x vs C
51,53 GB/s

10M de números (80 MB) acelerados mutando un solo byte

[0x80] LABORATORIO INTERACTIVO DE 128 BITS

Una instrucción de 16 bytes = Algoritmo + Planificación + Prueba

Selecciona cualquier nodo de instrucción (#0..#6) o haz clic en cualquier byte (0..15) para inspeccionar su registro de 8 bits, invariante O(N) y traza de ejecución de caja blanca.

Carril de Algoritmo (Qué calcular: Opcode / Operandos) Carril de Planificación (Cómo ejecutar: SIMD / Multinúcleo) Carril de Prueba (Seguridad: Ticket de versión / Límites)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS
DESGLOSE DEL REGISTRO DE 8 BITS · BYTE 2 (b16..b23) 0x12
0 2^7
0 2^6
0 2^5
1 2^4
0 2^3
0 2^2
1 2^1
0 2^0
Campo: schedule_hint Tipo: u8
✓ Invariante del verificador O(N) comprobado al cargar (~5.78 ns) (fusion_group << 4) | exec_policy

Byte de planificación de hardware ortogonal: mutar 0x11 (SimdStream) -> 0x12 (MultiCore) cambia la ejecución de la CPU sin alterar las pruebas de seguridad.

Nodo #3: Cuadrado vectorial de 8 carriles elemento por elemento ($n0 * $n0) fusionado en registros de caché L1 sin asignaciones intermedias en el heap.
Vista de ensamblador simbólico (src/main.rls — 208 B en .rl) ~8.8 µs assemble
cap 0x0
arena 0 len=4096 lane=f64x8 mut=false align=64 ver=1
output $n6
Trazador de ejecución de caja blanca (rul trace — 7 nodos SSA) Haz clic en cualquier fila para sincronizar la trama binaria de 16 bytes y el ensamblador
NODEOPCODEKINDLENMINMAXSUM/TRUESNANSAMPLE[0..4]
#0ArenaInputColumnF6440960.5000249.5000504608.00000[0.500, 1.500, 2.500, 3.500]
#1ConstF64Scalar1100.0000100.0000100.00000[100.000]
#2CmpGtColumnMask40960.00001.00002400.00000[0.000, 0.000, 0.000, 0.000]
#3MulColumnF6440960.250062250.250083627904.00000[0.250, 2.250, 6.250, 12.250]
#4SelectZeroColumnF6440960.000062250.250077999800.00000[0.000, 0.000, 0.000, 0.000]
#5ReduceSumScalar177999800.000077999800.000077999800.00000[77999800.000]
#6AssertContractScalar177999800.000077999800.000077999800.00000[77999800.000]
[0x100] MUTACIÓN DE PLANIFICACIÓN DE 1 BYTE

Muta 1 byte (Byte 2). Supera 4,72 veces al C escrito a mano.

Carga real: 10.000.000 de números en coma flotante (matriz de 80 MB) — filtrar valores > 1000.0, elevarlos al cuadrado y sumarlos. Haz clic para mutar el Byte 2 (schedule_hint) abajo: el algoritmo permanece 100 % idéntico mientras la ejecución baja de 5,91 ms a 1,55 ms:

BYTE 2 ACTIVO (schedule_hint): 0x12 + ZM bits[16..23] = 0001 0010
1.55 ms · 51.53 GB/s (4.72x vs C)

fg=1 pol=multicore + ArenaZoneMap: Combina la paralelización L1 multinúcleo con metadatos mín/máx por bloque (ArenaZoneMap) para saltar bloques fríos en O(1) sin lecturas de DRAM.

[A] AoS imperativo + Vec::collect()
70.66 ms 1.13 GB/s
[B] Rust SoA idiomático (filter().map().sum())
19.12 ms 4.18 GB/s
[C] C/Rust SoA de 8 acumuladores escrito a mano
7.32 ms 10.92 GB/s
[D] Rul (.rl) Tier 2 SIMD fusionado (0x11)
5.91 ms 13.53 GB/s
[E] Rul (.rl) Tier 2 MultiCore (0x12)
3.19 ms 25.04 GB/s
[F] Rul (.rl) Tier 2 MultiCore + ZoneMap
1.55 ms 51.53 GB/s
Prueba de pipeline profundo: BM-HORNER-50 (Polinomio de 50 pasos · 104 nodos SSA · 80 MB)

El asignador de registros YMM de escaneo lineal en src/aot.rs compila un binario ELF64 autónomo de 3.872 bytes en ~20,4 µs y lo ejecuta en 106,58 ms — igualando al C/Rust de 8 acumuladores escrito a mano (107,96 ms) sin LLVM.

[0x140] CUATRO MECANISMOS DE PRIMEROS PRINCIPIOS

Simple en primeros principios. Matemáticamente exacto en el silicio.

Los lenguajes tradicionales compilan lento porque la máquina tiene que leer texto humano y adivinar tu intención. Rul elimina toda suposición mediante cuatro mecanismos evidentes:

01 · EL BINARIO COMO ÚNICA FUENTE DE VERDAD src/bytecode.rs

1. Cero análisis de texto (0 % de errores de sintaxis)

En lugar de obligar a la IA a teclear miles de caracteres propensos a olvidar un punto y coma, la IA emite bloques binarios de 16 bytes directamente (o ensambla listados .rls en ~8,8 µs). Un pipeline de 7 pasos que procesa 10 millones de números ocupa solo 208 bytes en .rl y compila en un ejecutable Linux ELF64 autónomo de 817 bytes.

1. RulHeader 64 Bytes (64B-aligned)
2. ArenaDescriptor Table arena_count × 16 Bytes
3. ProofEntry Sidecar Table proof_count × 16 Bytes
4. NodeFrame Instruction DAG node_count × 16 Bytes
02 · PROPIEDAD LINEAL EN TIEMPO O(N) src/verifier.rs

2. Tickets de memoria versionados (Seguridad nivel Rust en nanosegundos)

Imagina cada búfer de memoria (Arena) como una sala con un ticket numerado que empieza en la versión 1. Múltiples instrucciones pueden leer la versión 1 al mismo tiempo (ReadLease 0b01). En cuanto una instrucción modifica datos en el sitio (AffineConsume 0b10), la sala sube a la versión 2: cualquier instrucción posterior con un ticket antiguo de versión 1 es rechazada en la puerta en 5,78 ns sin un Borrow Checker lento.

TOKEN_OP (32-BIT) = [mode: 2b | arena_id: 14b | version: 16b]
0b01 ReadLease(arena=0, ver=1) ✓ Lectura compartida (ver sigue en 1)
0b10 AffineConsume(arena=0, ver=1) → Mutación in situ y ver = 2
Reuse stale ReadLease(arena=0, ver=1) ✗ Rechazo: StaleOrConsumedToken
03 · SANDBOX DE CONFIANZA CERO Y LÍMITES ProofEntry + CapMask

3. Certificados de límites previos e interruptor de permisos de hardware

Las columnas de igual longitud corren a máxima velocidad sin comprobaciones de límites dentro del bucle (TRIVIAL_BY_SHAPE). Recortar una matriz (ArenaSlice) o saltar por índice (Gather) exige presentar un certificado de límites de 16 bytes (ProofEntry) al cargar. Y cuando el interruptor de hardware (CapabilityMask) es 0x0, el binario queda físicamente bloqueado de tocar la red o el disco.

proof_idx == 0 (90%+ nodes): TRIVIAL_BY_SHAPE (0 runtime checks)
proof_idx > 0 (ArenaSlice / Gather): lo <= hi <= effective_target_len
RulHeader.capability_mask = 0x0: CAP_NONE (Pure Compute Sandbox)
04 · AUDITABILIDAD DE CAJA BLANCA rul trace & decompile

4. Transparencia de rayos X en caja blanca (Nunca una caja negra)

Los humanos nunca tienen que escribir binario para mantener el 100 % del control: los ingenieros definen el esquema de datos (ArenaDescriptor), los permisos de hardware (CapabilityMask) y los contratos de salida (AssertContract); la IA regenera el binario .rl en microsegundos. En cualquier momento, ejecuta rul decompile para texto legible o rul trace para inspeccionar mín, máx, suma y NaN=0 en cada paso.

Contrato humano → La IA regenera .rl
Verificación + Compilación en ~12 µs en total
Espec. de 29 opcodes →
[0x180] MATRIZ DE SISTEMAS Y AGENT MCP

C vs. Go vs. Rust vs. Rul (.rl)

Comparación arquitectónica en sobrecarga de análisis, seguridad de memoria, comprobación de límites, latencia de compilación y seguridad de sandbox.

DIMENSIÓNC (clang -O3)Go (gc)Rust (rustc + LLVM)Rul (.rl) v0.4
Autor principalProgramador humanoEquipos de ingeniería humanosIngenieros de sistemas humanosAgentes de IA (con herramientas auditables por humanos)
Formato del artefactoTexto (.c, .h)Texto (.go)Texto (.rs)Binario plano .rl (Instrucciones de 16 bytes)
Sobrecarga de parseoAltaMediaMuy alta (Macros, AST)0 ms (mmap binario directo sin copia)
Seguridad de memoriaNinguna (Punteros manuales)Recolector de basura (Pausas en ejecución)Borrow Checker (Solucionador de restricciones)TokenOp versionado (Comprobación O(1) por nodo)
Comprobación de límitesSin comprobar (Desbordamientos de búfer)Salto condicional en cada accesoSalto en ejecución (salvo optimización)En tiempo de carga mediante Shape + tabla ProofEntry
Tiempo de verif. + compilaciónSegundosSubsegundos a segundosSegundos a minutos~5,8 ns/nodo Verif. + ~6,4 µs ELF64 AOT
Seguridad de sandboxProceso completo del SOProceso completo del SOProceso completo del SO (crates unsafe)CapabilityMask de 64 bits en la cabecera del archivo
STDIO JSON-RPC 2.0 · src/mcp.rs

Servidor Model Context Protocol integrado (rul-mcp)

Servidor stdio JSON-RPC 2.0 sin dependencias que expone directamente a los agentes de IA autónomos 6 herramientas nativas de verificación, pruebas diferenciales, autoajuste y compilación AOT.

GET /.well-known/mcp.json ↗
rul_assemble_and_verify ~8.8 µs + 5.8 ns/node
(rls_source: string) -> VerifiedSummary + .rl hex

Ensambla instrucciones simbólicas .rls en una imagen binaria .rl de 128 bits y ejecuta el verificador estático O(N) de un solo pase.

rul_test_differential Tier 0 == Tier 1 == Tier 2
(rls_source: string, arenas: ArenaData[]) -> DiffReport

Ejecuta el programa verificado en Tier 0 (Oracle), Tier 1 (Stencil) y Tier 2 (L1 Fused) para demostrar equivalencia bit a bit/ULP.

rul_autotune_schedule 1-Byte Sweep
(rls_source: string) -> Optimal ScheduleHint + Telemetry

Recorre las políticas AutoL1Tile (0x10), SimdStream (0x11) y MultiCore (0x12) y selecciona la mayor puntuación de ancho de banda GB/s.

rul_compile_standalone ~6.4 µs ELF64
(rls_source: string) -> Standalone Linux x86_64 ELF64

Emite un ejecutable autónomo Linux x86_64 AVX2 ELF64 sin dependencias (628 B – 1.037 B) mediante asignación lineal de registros YMM.

rul_trace White-Box Inspector
(rls_source: string) -> NodeTraceRow[0..N-1]

Devuelve telemetría exacta por nodo de mín, máx, suma/verdaderos, recuento de NaN/Inf y sample[0..4] en cada instrucción SSA.

rul_cas_intrinsics 64-Bit FNV-1a CAS
(op: sort | hash_join | group_by | simd_scan) -> CasHash

Ejecuta núcleos I64/U8 direccionados por contenido y verificados (sort, hash_join, group_by, simd_scan_byte) en RulCasStore.

[0x1C0] HOJA DE RUTA HACIA v1.0

Del motor columnar verificado (v0.4) al lenguaje de sistemas de propósito general (v1.0)

Restringimos las versiones v0.1–v0.4 a pipelines de matrices y vectores (29 opcodes) para demostrar primero el formato binario de 16 bytes en silicio real. En cuatro hitos, Rul se expande para reemplazar a Rust y Go:

Ver hoja de ruta técnica completa y reglas de ingeniería →
v0.1.0 → v0.4.0 Línea base de producción publicada
✓ EN PRODUCCIÓN

Núcleo SSA-DAG columnar de 29 opcodes, trazador de caja blanca y compilador AVX2 ELF64 AOT

Demostró en hardware real el formato binario de 16 bytes, el verificador O(N) de un solo pase (~5,8 ns/nodo), el motor de 3 niveles, el servidor rul-mcp y el compilador nativo Linux ELF64 sin LLVM (~6,4 µs).

  • [1] RulHeader de 64 bytes, ArenaDescriptor de 16 bytes, ProofEntry de 16 bytes y NodeFrame de 16 bytes en 29 opcodes.
  • [2] Ensamblador simbólico bidireccional sin pérdidas .rls <-> .rl, CLI autónomo rul, rul-bench y servidor rul-mcp de 6 herramientas.
  • [3] Asignador de registros YMM de escaneo lineal (ymm2..ymm13) que alcanza 51,53 GB/s (4,72x sobre C) en matrices de 80 MB.
v0.5 Hito 1 (Meses 1–2)
● EN PROGRESO

Flujo de control de propósito general, funciones modulares y tipos de datos compuestos

Expandir el conjunto de instrucciones de 16 bytes más allá de las matrices numéricas para admitir escalares generales, structs, enums, cadenas UTF-8, mapas hash, ramas condicionales y bucles con prueba de terminación.

  • [1] Soporte de primera clase para i64, i32, u8, f32, structs de diseño fijo, uniones etiquetadas algebraicas, cadenas UTF-8 validadas y mapas hash en arena.
  • [2] SelectBranch: bifurcación condicional que exige que ambas ramas converjan en un estado idéntico de versión de memoria (comprobado en O(1)).
  • [3] RegionLoop y Call: bucles acotados con testigos de terminación en ProofEntry y funciones modulares verificadas sin inlining global.
v0.6 – v0.7 Hito 2 (Meses 2–3)
○ PROGRAMADO

Propiedad del heap de nivel Rust y tiempos de vida de structs en tiempo O(N)

Generalizar las versiones TokenOp de 32 bits y los testigos ProofEntry de 16 bytes desde matrices planas hacia asignaciones de heap basadas en regiones y préstamos de campos de structs.

  • [1] Asignación y liberación determinista de regiones del heap vinculadas a tokens de propiedad lineal con cero GC y cero fragmentación malloc/free.
  • [2] Testigos ProofEntry para mutaciones disjuntas de campos de structs y tiempos de vida de sub-rebanadas zero-copy comprobados en O(1) por instrucción.
  • [3] Protección total contra use-after-free, double-free y aliasing sin resolución de restricciones Borrow Checker de varios segundos.
v0.8 – v0.9 Hito 3 (Meses 4–5)
○ PROGRAMADO

Concurrencia determinista al estilo Go y E/S del SO controlada por CapabilityMask

Introducir tareas ligeras, canales con transferencia de propiedad y bits de capacidad detallados en la cabecera que gobiernen llamadas al sistema de archivos, red y procesos.

  • [1] Enviar un búfer por un canal tipado realiza un AffineConsume sobre el token emisor y transfiere la propiedad al receptor — evitando carreras de datos al cargar sin GC.
  • [2] Ampliar el RulHeader.capability_mask de 64 bits para controlar lecturas/escrituras de archivos, sockets de red, temporizadores y subprocesos.
  • [3] Un binario .rl con CAP_NONE (0x0) queda bloqueado matemáticamente de realizar cualquier llamada de red o disco antes de iniciar la ejecución.
v1.0 Hito 4 (Mes 6)
○ PROGRAMADO

Backends nativos multiarquitectura (x86_64, ARM64, WASI) y pruebas formales de solidez

Emitir ejecutables autónomos en Linux, macOS, Windows y WebAssembly sin LLVM, respaldados por model checking con Kani y una suite de conformidad v1.0 de 50 programas.

  • [1] Generación de código nativo cero-LLVM para x86_64 y AArch64 (ARM64) en Linux, macOS y Windows, más módulos WASI deterministas.
  • [2] Pruebas de model checking acotado (Kani) y fuzzing diferencial continuo en el decodificador binario, verificador O(N) y generador nativo.
  • [3] Especificación binaria .rl v1.0 congelada y suite pública de pruebas de conformidad de 50 programas.
[0x1F0] RESPUESTAS TÉCNICAS DIRECTAS (AEO / FAQ)

Preguntas frecuentes — Del lenguaje sencillo a los sistemas profundos

Explicaciones claras desde primeros principios combinadas con mediciones empíricas exactas para ingenieros, investigadores y motores de respuesta de IA.

Q01 ¿Qué es Rul (.rl) y por qué utiliza un formato binario de 16 bytes en lugar de texto humano? +
La IA piensa en números y las CPU ejecutan binario; sin embargo, lenguajes como C, Go y Rust obligan a la IA a teclear miles de palabras humanas y esperar segundos a que un compilador (rustc/LLVM) traduzca ese texto de vuelta a binario. Rul (.rl) elimina al intermediario de texto humano: los agentes de IA emiten bloques binarios fijos de 16 bytes (128 bits) que llevan el Algoritmo, la Planificación de CPU y el Ticket de Seguridad de Memoria desde el principio — eliminando el análisis de texto (0 ms) y compilando ejecutables autónomos Linux ELF64 en ~6,4 µs.
Q02 ¿Cómo verifica Rul la seguridad de memoria de nivel Rust en ~5,8 ns por instrucción sin un Borrow Checker lento? +
Imagina cada búfer de memoria (Arena) como una habitación con un ticket de versión numerado que empieza en la versión 1. Múltiples instrucciones pueden leer la versión 1 al mismo tiempo usando un permiso compartido ReadLease (0b01). Cuando una instrucción modifica el búfer in situ mediante AffineConsume (0b10), comprueba que sea mutable y sube la habitación a la versión 2. Cualquier instrucción posterior que conserve un ticket obsoleto de versión 1 es rechazada en la puerta en tiempo O(1) durante un único pase hacia adelante (~5,78 ns/nodo) — sin necesidad de un solucionador Borrow Checker de varios segundos.
Q03 Si los humanos no escriben archivos binarios .rl a mano, ¿cómo depuran y mantienen los equipos de ingeniería los sistemas Rul? +
Los humanos mantienen el 100 % del control sin teclear binario — igual que los médicos leen radiografías sin dibujarlas a mano: (1) Los humanos fijan las reglas al principio — los ingenieros definen esquemas de datos (ArenaDescriptor), interruptores de permisos de hardware (CapabilityMask de 64 bits) y controles de aceptación (AssertContract), mientras la IA regenera el binario .rl verificado en microsegundos; (2) Texto legible al instante mediante `rul decompile`, que convierte cualquier archivo .rl de vuelta a ensamblador simbólico `.rls`; (3) Inspección por rayos X mediante `rul trace`, que imprime los valores exactos de mín, máx, suma, recuento de NaN/Inf y sample[0..4] en cada paso.
Q04 ¿Por qué la cadena de herramientas de Rul está implementada en Rust si Rul está diseñado para reemplazar los lenguajes de texto para agentes de IA? +
Todo nuevo lenguaje de sistemas requiere un lenguaje anfitrión inicial para su primer compilador de arranque (bootstrap) — igual que el primer compilador de C se escribió en ensamblador y el primer compilador de Rust en OCaml. Construimos el verificador de Rul, el motor de ejecución de 3 niveles y el compilador nativo ELF64 en Rust puro sin dependencias bajo `#![forbid(unsafe_code)]`. Una vez instalado el binario autónomo `rul`, los usuarios y agentes de IA verifican, compilan y ejecutan programas `.rl` directamente sin necesitar rustc, Cargo ni LLVM.
Q05 ¿Cómo logra Rul alcanzar 51,53 GB/s (4,72 veces más rápido que C escrito a mano) mutando un solo byte? +
En Rul, la planificación de hardware (Byte 2: schedule_hint) es ortogonal a la lógica del algoritmo (Byte 0: opcode). En un pipeline de filtrado, cuadrado y suma de 80 MB (10.000.000 de f64), Rul en un solo núcleo (`0x11 SimdStream`) fusiona todas las operaciones en bloques de caché L1 de 1.024 elementos dentro de los registros AVX2 YMM, ejecutándose en 5,91 ms frente a los 7,32 ms del C de 8 acumuladores escrito a mano (1,24x más rápido). Mutar el Byte 2 de 0x11 a 0x12 (`MultiCore`) paraleliza esos bloques L1 en todos los núcleos de la CPU (3,19 ms, 2,29x), y activar los metadatos mín/máx de bloque `ArenaZoneMap` salta los bloques fríos en O(1) para terminar en 1,55 ms (51,53 GB/s, 4,72x más rápido que C mononúcleo y 45,51x más rápido que AoS imperativo).
Q06 ¿Puede Rul reemplazar a Rust y Go para software backend y de sistemas de propósito general? +
Sí — ese es exactamente el objetivo de la hoja de ruta v1.0 de cuatro hitos: el Hito 1 (v0.5) añade i64/i32/u8/f32, structs, uniones etiquetadas, cadenas UTF-8, mapas hash, condicionales SelectBranch verificados en O(1) y bucles RegionLoop con prueba de terminación; el Hito 2 (v0.6–0.7) extiende TokenOp y ProofEntry a asignaciones de heap basadas en regiones y préstamos de campos de structs; el Hito 3 (v0.8–0.9) introduce tareas ligeras y canales con transferencia de propiedad al estilo Go además de llamadas al sistema del SO controladas por CapabilityMask; el Hito 4 (v1.0) ofrece backends nativos sin LLVM para x86_64, ARM64 y WASI respaldados por pruebas formales de solidez en Kani.