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

Il Linguaggio di Programmazione Binario a 128 Bit per Agenti IA.

L'IA pensa in numeri e le CPU eseguono binario — eppure C, Go e Rust costringono l'IA a digitare testo umano e ad attendere secondi affinché un compilatore indovini cosa intendesse. Rul (.rl) elimina quell'intermediario testuale: l'IA emette mattoni binari fissi da 16 byte contenenti in anticipo Algoritmo, Scheduling CPU e Biglietto di Sicurezza della Memoria. Risultato: verifica di sicurezza in 5.8 ns, compilazione autonoma in 6.4 µs ed esecuzione 4.72 volte più veloce del C scritto a mano.

PRINCIPI PRIMI IN 10 SECONDI · ELIMINA L'INTERMEDIARIO TESTUALE
✗ VECCHIO MODO (C / Go / Rust) L'IA Pensa (Numeri) → Digita Testo Umano → Il Compilatore Analizza & Indovina l'Intento (Secondi) → Codice Macchina (0/1)
✓ PRINCIPI PRIMI RUL (.rl) L'IA Pensa (Numeri) → Emette Mattone Binario da 16 Byte (Prova 5.8 ns + Compilazione 6.4 µs) → Gira 4.72x Più Veloce del C
Mattone Binario da 16 Byte (0ms Parse) + 6.4 µs ELF64 Nativo (Zero LLVM) + Prova di Sicurezza 5.8 ns (O(N) Lineare)
# 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)
IMMAGINE BINARIA .RL LIVE · 7 NODI SSA = 208 BYTE -> ELF64 DA 817 BYTE CAP_NONE=0x0

Clicca su qualsiasi frame di istruzione da 16 byte qui sotto per decodificare bit, prova del verificatore e traccia:

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] Frame a 128 Bit
16 Byte

Ogni Istruzione È un Mattone Binario Fisso · 0 ms di Parsing Testuale

[0x50] per istruzione
5.78 ns

Prova Istantanea di Memoria & Limiti (Singola Passata O(N))

[0x60] compilazione nativa
6.4 µs

Binario Linux x86_64 ELF64 Autonomo Senza LLVM

[0x70] 4.72x vs C
51.53 GB/s

10M di Numeri (80 MB) Accelerati dalla Mutazione di 1 Byte

[0x80] WORKBENCH INTERATTIVO A 128 BIT

Un'Istruzione da 16 Byte = Algoritmo + Scheduling + Prova

Seleziona qualsiasi nodo di istruzione (#0..#6) o clicca su qualsiasi byte (0..15) per ispezionare il suo registro binario a 8 bit, il certificato di sicurezza O(N) e la traccia di esecuzione white-box.

Corsia Algoritmo (Cosa calcolare: Opcode / Operandi) Corsia Scheduling (Come eseguire: SIMD / MultiCore) Corsia Prova (Sicurezza: Biglietto di Versione / Limiti)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS
ANALISI DEL REGISTRO A 8 BIT · 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 Verificatore O(N) Controllato al Caricamento (~5.78 ns) (fusion_group << 4) | exec_policy

Byte ortogonale di scheduling hardware: mutare 0x11 (SimdStream) -> 0x12 (MultiCore) cambia l'esecuzione della CPU senza alterare le prove di sicurezza.

Nodo #3: Quadrato vettoriale elemento per elemento a 8 vie ($n0 * $n0) fuso nei registri di cache L1 con zero allocazioni sull'heap.
Vista Assembly Simbolico (src/main.rls — 208 B in .rl) ~8.8 µs assemble
cap 0x0
arena 0 len=4096 lane=f64x8 mut=false align=64 ver=1
output $n6
Tracciatore di Esecuzione White-Box (rul trace — 7 Nodi SSA) Clicca su qualsiasi riga per sincronizzare il frame binario da 16 byte e l'assembly
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] MUTAZIONE DI SCHEDULING HARDWARE DI 1 BYTE

Muta 1 Byte (Byte 2). Accelera 4.72x Oltre il C Scritto a Mano.

Carico di lavoro reale: 10.000.000 di numeri in virgola mobile (array da 80 MB) — filtra i valori > 1000.0, elevali al quadrato e sommali in un unico risultato. Clicca per mutare il Byte 2 (schedule_hint) qui sotto: l'algoritmo resta identico al 100%, mentre l'esecuzione scende da 5.91 ms a 1.55 ms:

BYTE 2 ATTIVO (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 il tiling L1 MultiCore con i metadati min/max di blocco (ArenaZoneMap) per saltare i blocchi freddi da 1.024 elementi in O(1) senza letture dalla DRAM.

[A] Imperativo AoS + Vec::collect()
70.66 ms 1.13 GB/s
[B] Rust Idiomatico SoA (filter().map().sum())
19.12 ms 4.18 GB/s
[C] C/Rust Scritto a Mano SoA a 8 Accumulatori
7.32 ms 10.92 GB/s
[D] Rul (.rl) Tier 2 SIMD Fuso (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
Prova di Pipeline Profonda: BM-HORNER-50 (Polinomio a 50 Passi · 104 Nodi SSA · 80 MB)

L'allocatore lineare di registri YMM in src/aot.rs compila un binario ELF64 autonomo da 3.872 byte in ~20.4 µs ed esegue in 106.58 ms — eguagliando il C/Rust a 8 accumulatori scritto a mano (107.96 ms) con zero LLVM.

[0x140] QUATTRO MECCANISMI BASATI SUI PRINCIPI PRIMI

Semplice nei Principi Primi. Matematicamente Esatto nel Silicio.

I linguaggi tradizionali sono lenti a compilare perché la macchina deve leggere il testo umano e indovinare il tuo intento. Rul elimina ogni congettura attraverso quattro meccanismi evidenti:

01 · UNICA FONTE DI VERITÀ BINARIA src/bytecode.rs

1. Zero Parsing del Testo (0% di Errori di Sintassi)

Invece di costringere l'IA a digitare migliaia di caratteri soggetti a punti e virgola mancanti, l'IA emette direttamente mattoni binari da 16 byte (o assembla listati .rls piatti in ~8.8 µs). Una pipeline a 7 passi che elabora 10 milioni di numeri occupa solo 208 byte in .rl e compila in un eseguibile Linux ELF64 autonomo da 817 byte.

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 · PROPRIETÀ LINEARE IN O(N) src/verifier.rs

2. Biglietti di Memoria Versionati (Sicurezza di Livello Rust in Nanosecondi)

Immagina ogni buffer di memoria (Arena) come una stanza con un biglietto numerato che parte dalla versione 1. Più istruzioni possono leggere insieme la versione 1 (ReadLease 0b01). Nel momento in cui un'istruzione modifica i dati in-place (AffineConsume 0b10), la stanza passa alla versione 2 — qualsiasi istruzione successiva con un vecchio biglietto di versione 1 viene respinta alla porta in 5.78 ns senza un lento Borrow Checker.

TOKEN_OP (32-BIT) = [mode: 2b | arena_id: 14b | version: 16b]
0b01 ReadLease(arena=0, ver=1) ✓ Lettura Condivisa (ver resta 1)
0b10 AffineConsume(arena=0, ver=1) → Muta & Incrementa ver = 2
Reuse stale ReadLease(arena=0, ver=1) ✗ Rifiuta: StaleOrConsumedToken
03 · SANDBOX ZERO-TRUST & LIMITI ProofEntry + CapMask

3. Certificati dei Limiti Anticipati & Interruttore di Capacità Hardware

Le colonne di uguale lunghezza girano alla massima velocità con zero controlli dei limiti nel ciclo interno (TRIVIAL_BY_SHAPE). Affettare un array (ArenaSlice) o saltare per indice (Gather) richiede la presentazione di un certificato dei limiti da 16 byte (ProofEntry) al caricamento. E quando l'interruttore dei permessi hardware (CapabilityMask) è 0x0, il binario è fisicamente bloccato dal toccare la rete o il 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 · VERIFICABILITÀ WHITE-BOX rul trace & decompile

4. Trasparenza White-Box a Raggi X (Mai una Scatola Nera)

Gli esseri umani non devono mai digitare il binario per mantenere il 100% del controllo: gli ingegneri impostano il layout dei dati (ArenaDescriptor), i permessi hardware (CapabilityMask) e i contratti di output (AssertContract); l'IA rigenera il binario .rl in microsecondi. In qualsiasi momento, esegui rul decompile per ottenere testo leggibile o rul trace per ispezionare min, max, somma e NaN=0 esatti ad ogni passo.

Contratto Umano → L'IA Rigenera .rl
Verifica + Compila in ~12 µs totali
Specifica a 29 Opcode →
[0x180] MATRICE DI SISTEMA & AGENTE MCP

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

Confronto architetturale su overhead di parsing, complessità della sicurezza della memoria, controllo dei limiti, latenza di compilazione e sicurezza della sandbox.

DIMENSIONEC (clang -O3)Go (gc)Rust (rustc + LLVM)Rul (.rl) v0.4
Autore PrincipaleProgrammatore umanoTeam di ingegneria umaniIngegneri di sistema umaniAgenti IA (con strumenti verificabili dall'uomo)
Formato dell'ArtefattoTesto (.c, .h)Testo (.go)Testo (.rs)Binario Piatto .rl (Istruzioni da 16 Byte)
Overhead di ParsingAltoMedioMolto Alto (Macro, AST)0 ms (mmap binario zero-copy diretto)
Sicurezza della MemoriaNessuna (Puntatori manuali)Garbage Collector (Pause a runtime)Borrow Checker (Risolutore di vincoli)TokenOp Versionato (Controllo O(1) per nodo)
Controllo dei LimitiNon controllato (Buffer overflow)Diramazione a runtime per accessoDiramazione a runtime (salvo elisione)Forma al caricamento + tabella ausiliaria ProofEntry
Tempo di Verifica + CompilazioneSecondiDa frazioni di secondo a secondiDa secondi a minuti~5.8 ns/nodo Verifica + ~6.4 µs ELF64 AOT
Sicurezza della SandboxIntero processo del SOIntero processo del SOIntero processo del SO (crate unsafe)CapabilityMask a 64 Bit nell'Header del File
STDIO JSON-RPC 2.0 · src/mcp.rs

Server Model Context Protocol Integrato (rul-mcp)

Server JSON-RPC 2.0 stdio senza dipendenze che espone 6 strumenti nativi di verifica, testing differenziale, autotuning e compilazione AOT direttamente agli agenti IA autonomi.

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

Assembla istruzioni simboliche .rls in un'immagine binaria .rl a 128 bit ed esegue il verificatore statico O(N) a passata singola.

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

Esegue il programma verificato sui Tier 0 (Oracolo), Tier 1 (Stencil) e Tier 2 (Fusione L1) per dimostrare l'equivalenza bit a bit/ULP.

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

Esplora le politiche AutoL1Tile (0x10), SimdStream (0x11) e MultiCore (0x12) e seleziona il punteggio di ricompensa hardware GB/s più elevato.

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

Emette un eseguibile Linux x86_64 AVX2 ELF64 senza dipendenze (628 B – 1.037 B) utilizzando l'allocazione lineare dei registri YMM.

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

Restituisce la telemetria esatta per nodo di min, max, somma/veri, conteggio NaN/Inf e sample[0..4] su ogni istruzione SSA.

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

Esegue kernel verificati I64/U8 indirizzati dal contenuto (sort, hash_join, group_by, simd_scan_byte) in RulCasStore.

[0x1C0] ROADMAP VERSO v1.0

Da Motore Colonnare Verificato (v0.4) a Linguaggio di Sistema General-Purpose (v1.0)

Abbiamo limitato le versioni v0.1–v0.4 alle pipeline di array e vettori (29 opcode) per dimostrare prima il formato binario da 16 byte sul silicio reale. Attraverso quattro milestone, Rul si espande per sostituire Rust e Go nel software di sistema generato dall'IA:

Vedi Roadmap Tecnica Completa & Non-Obiettivi →
v0.1.0 → v0.4.0 Baseline di Produzione Rilasciata
✓ IN PRODUZIONE

Core SSA-DAG Colonnare a 29 Opcode, Tracciatore White-Box & AOT AVX2 ELF64

Ha dimostrato il formato di istruzione binario da 16 byte, il verificatore O(N) a passata singola (~5.8 ns/nodo), il motore di esecuzione a 3 livelli, il server rul-mcp e il compilatore nativo Linux ELF64 senza LLVM (~6.4 µs) su hardware reale.

  • [1] RulHeader da 64 byte, ArenaDescriptor da 16 byte, ProofEntry da 16 byte e NodeFrame da 16 byte su 29 opcode.
  • [2] Assembler simbolico senza perdite .rls <-> .rl, CLI rul autonoma, rul-bench e server rul-mcp a 6 strumenti.
  • [3] Allocatore lineare di registri YMM (ymm2..ymm13) che raggiunge 51.53 GB/s (4.72x rispetto al C) su array da 80 MB.
v0.5 Milestone 1 (Mesi 1–2)
● IN CORSO

Flusso di Controllo General-Purpose, Funzioni & Tipi di Dati Composti

Espandere il set di istruzioni da 16 byte oltre gli array numerici per supportare scalari generali, struct, enum, stringhe UTF-8, hash map, diramazioni condizionali e cicli con terminazione dimostrata.

  • [1] Supporto nativo per i64, i32, u8, f32, struct a layout fisso, unioni etichettate algebriche, stringhe UTF-8 convalidate e hash map d'arena.
  • [2] SelectBranch: diramazione condizionale che richiede a entrambi i rami di convergere nello stesso stato di versione della memoria (controllato in O(1)).
  • [3] RegionLoop & Call: cicli limitati con certificati di terminazione ProofEntry e funzioni modulari verificate senza inlining dell'intero programma.
v0.6 – v0.7 Milestone 2 (Mesi 2–3)
○ PIANIFICATO

Proprietà dell'Heap di Livello Rust & Lifetime delle Struct in Tempo O(N)

Generalizzare le versioni TokenOp a 32 bit e i certificati ProofEntry da 16 byte dagli array piatti alle allocazioni sull'heap basate su regioni e ai prestiti dei campi delle struct.

  • [1] Allocazione e deallocazione deterministica dell'heap in regioni legata a token di proprietà lineare con zero GC e zero frammentazione da malloc/free.
  • [2] Certificati ausiliari ProofEntry per mutazioni disgiunte dei campi delle struct e lifetime di sotto-slice zero-copy controllati in O(1) per istruzione.
  • [3] Protezione completa contro use-after-free, double-free e aliasing senza risoluzione di vincoli del borrow-checker di diversi secondi.
v0.8 – v0.9 Milestone 3 (Mesi 4–5)
○ PIANIFICATO

Concorrenza Deterministica in Stile Go & I/O del SO Controllato da Capacità

Introdurre task leggeri, canali con trasferimento di proprietà e bit granulari di capacità nell'header che regolano le syscall di file, rete e processi.

  • [1] L'invio di un buffer su un canale tipizzato esegue un AffineConsume sul token del mittente e trasferisce la proprietà al destinatario — prevenendo data race al caricamento senza GC.
  • [2] Estendere RulHeader.capability_mask a 64 bit per controllare letture/scritture su filesystem, socket di rete, timer e sottoprocessi.
  • [3] Un binario .rl con CAP_NONE (0x0) è matematicamente bloccato dall'effettuare qualsiasi chiamata di rete o disco prima dell'inizio dell'esecuzione.
v1.0 Milestone 4 (Mese 6)
○ PIANIFICATO

Backend Nativi Multi-Architettura (x86_64, ARM64, WASI) & Prove Formali di Correttezza

Emettere eseguibili autonomi per Linux, macOS, Windows e WebAssembly senza LLVM, supportati dal model checking Kani e da una suite di conformità v1.0 di 50 programmi.

  • [1] Generazione di codice nativo senza LLVM per x86_64 e AArch64 (ARM64) su Linux, macOS e Windows, oltre a moduli WASI deterministici.
  • [2] Prove di bounded model-checking (Kani) e fuzzing differenziale continuo su decodificatore binario, verificatore O(N) e codegen nativo.
  • [3] Specifica binaria .rl v1.0 congelata e suite pubblica di test di conformità di 50 programmi.
[0x1F0] RISPOSTE TECNICHE DIRETTE (AEO / FAQ)

Domande Frequenti — Dal Linguaggio Semplice ai Sistemi Profondi

Spiegazioni chiare basate sui principi primi abbinate a misurazioni empiriche esatte per ingegneri, ricercatori e motori di risposta IA.

Q01 Cos'è Rul (.rl) e perché usa un formato binario da 16 byte invece del testo umano? +
L'IA pensa in numeri e le CPU eseguono binario — eppure linguaggi come C, Go e Rust costringono l'IA a digitare migliaia di parole umane e ad aspettare secondi affinché un compilatore (rustc/LLVM) ritraduca quel testo in binario. Rul (.rl) elimina l'intermediario del testo umano: gli agenti IA emettono mattoni binari fissi da 16 byte (128 bit) che portano in anticipo Algoritmo, Scheduling CPU e Biglietto di Sicurezza della Memoria — eliminando il parsing del testo (0 ms) e compilando eseguibili Linux ELF64 autonomi in ~6.4 µs.
Q02 Come fa Rul a verificare una sicurezza della memoria di livello Rust in ~5.8 ns per istruzione senza un lento borrow checker? +
Immagina ogni buffer di memoria (Arena) come una stanza con un biglietto di versione numerato che parte dalla versione 1. Più istruzioni possono leggere la versione 1 contemporaneamente usando un ReadLease condiviso (0b01). Quando un'istruzione modifica il buffer in-place tramite AffineConsume (0b10), controlla che il buffer sia mutabile e porta la stanza alla versione 2. Qualsiasi istruzione successiva con un vecchio biglietto di versione 1 viene respinta alla porta in tempo O(1) durante una singola passata in avanti (~5.78 ns/nodo) — senza alcun bisogno di un risolutore borrow-checker di diversi secondi.
Q03 Se gli umani non scrivono file binari .rl a mano, come fanno i team di ingegneria a fare debug e mantenere i sistemi Rul? +
Gli umani mantengono il 100% del controllo senza digitare binario — proprio come i medici leggono le radiografie senza disegnarle a mano: (1) Gli umani fissano le regole in anticipo — gli ingegneri definiscono gli schemi dei dati (ArenaDescriptor), gli interruttori di permesso hardware (CapabilityMask a 64 bit) e i controlli di accettazione (AssertContract), mentre l'IA rigenera il binario .rl verificato in microsecondi; (2) Testo leggibile istantaneo tramite `rul decompile` converte qualsiasi file .rl nell'assembly simbolico .rls; (3) L'ispezione a raggi X tramite `rul trace` stampa i valori esatti di min, max, somma, conteggio NaN/Inf e sample[0..4] ad ogni passo d'istruzione.
Q04 Perché la toolchain di Rul è implementata in Rust se Rul è progettato per sostituire i linguaggi testuali umani per gli agenti IA? +
Ogni nuovo linguaggio di sistema richiede un linguaggio ospite iniziale per il suo compilatore di bootstrap — proprio come il primo compilatore C è stato scritto in assembly e il primo compilatore Rust in OCaml. Abbiamo costruito il verificatore Rul, il motore di esecuzione a 3 livelli e il compilatore nativo ELF64 in Rust privo di dipendenze sotto #![forbid(unsafe_code)]. Una volta installato il binario autonomo `rul`, utenti e agenti IA verificano, compilano ed eseguono programmi .rl direttamente senza bisogno di rustc, Cargo o LLVM.
Q05 Come fa Rul a raggiungere 51.53 GB/s (4.72 volte più veloce del C scritto a mano) mutando un singolo byte? +
In Rul, lo scheduling hardware (Byte 2: schedule_hint) è ortogonale alla logica dell'algoritmo (Byte 0: opcode). Su una pipeline di filtro-quadrato-somma da 80 MB (10.000.000 f64), Rul a singolo core (`0x11 SimdStream`) fonde tutte le operazioni in blocchi di cache L1 da 1.024 elementi nei registri AVX2 YMM, girando in 5.91 ms contro i 7.32 ms del C a 8 accumulatori scritto a mano (1.24x più veloce). Mutare il Byte 2 da 0x11 a 0x12 (`MultiCore`) parallelizza quei blocchi L1 su tutti i core della CPU (3.19 ms, 2.29x), e l'attivazione dei metadati min/max di blocco `ArenaZoneMap` salta i blocchi freddi in O(1) per terminare in 1.55 ms (51.53 GB/s, 4.72x più veloce del C a 1 core e 45.51x più veloce di AoS imperativo).
Q06 Rul può sostituire Rust e Go per il software backend general-purpose e di sistema? +
Sì — questo è esattamente l'obiettivo della roadmap v1.0 in quattro milestone: la Milestone 1 (v0.5) aggiunge i64/i32/u8/f32, struct, unioni etichettate, stringhe UTF-8, hash map, condizionali SelectBranch verificati in O(1) e iterazione RegionLoop con terminazione dimostrata; la Milestone 2 (v0.6–0.7) estende TokenOp e ProofEntry alle allocazioni sull'heap basate su regioni e ai prestiti dei campi delle struct; la Milestone 3 (v0.8–0.9) introduce task leggeri in stile Go e canali con trasferimento di proprietà più syscall del SO controllate da CapabilityMask; la Milestone 4 (v1.0) fornisce backend nativi senza LLVM per x86_64, ARM64 e WASI supportati da prove formali di correttezza Kani.