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

Le langage binaire 128 bits conçu pour les agents IA.

L'IA pense en nombres et les processeurs exécutent du binaire — pourtant C, Go et Rust obligent l'IA à taper du texte humain et à attendre des secondes qu'un compilateur devine son intention. Rul (.rl) supprime cet intermédiaire textuel : l'IA émet des briques binaires fixes de 16 octets portant l'Algorithme, l'Ordonnancement CPU et le Ticket de sécurité mémoire dès le départ. Résultat : vérification en 5,8 ns, compilation autonome en 6,4 µs et exécution 4,72x plus rapide que du C écrit à la main.

PREMIERS PRINCIPES EN 10 SECONDES · SUPPRIMER L'INTERMÉDIAIRE TEXTUEL
✗ ANCIENNE VOIE (C / Go / Rust) L'IA pense (Nombres) → Tape du texte humain → Le compilateur parse & devine (Secondes) → Code machine (0/1)
✓ PREMIERS PRINCIPES RUL (.rl) L'IA pense (Nombres) → Émet une brique binaire de 16 octets (Preuve 5,8 ns + Compile 6,4 µs) → 4,72x plus rapide que C
Brique binaire 16 octets (0ms de parsing) + 6,4 µs ELF64 natif (Zéro LLVM) + Preuve mémoire 5,8 ns (O(N) linéaire)
# 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)
IMAGE BINAIRE .RL EN DIRECT · 7 NŒUDS SSA = 208 OCTETS -> ELF64 DE 817 OCTETS CAP_NONE=0x0

Cliquez sur n'importe quelle trame d'instruction de 16 octets ci-dessous pour décoder ses bits, sa preuve et sa trace :

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] Trame 128 bits
16 Octets

Chaque instruction est une brique binaire fixe · 0 ms de parsing

[0x50] par instruction
5,78 ns

Preuve instantanée de mémoire et de bornes (Passe unique O(N))

[0x60] compilation native
6,4 µs

Exécutable autonome Linux x86_64 ELF64 sans LLVM

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

10M de nombres (80 Mo) accélérés par la mutation d'un seul octet

[0x80] ATELIER INTERACTIF 128 BITS

Une instruction de 16 octets = Algorithme + Ordonnancement + Preuve

Sélectionnez un nœud d'instruction (#0..#6) ou cliquez sur un octet (0..15) pour inspecter son registre 8 bits, son invariant O(N) et sa trace d'exécution boîte blanche.

Voie Algorithme (Quoi calculer : Opcode / Opérandes) Voie Ordonnancement (Comment exécuter : SIMD / Multi-cœur) Voie Preuve (Sécurité : Ticket de version / Bornes)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS
DÉCOMPOSITION DU REGISTRE 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
Champ: schedule_hint Type: u8
✓ Invariant du vérificateur O(N) contrôlé au chargement (~5.78 ns) (fusion_group << 4) | exec_policy

Octet d'ordonnancement matériel orthogonal : muter 0x11 (SimdStream) -> 0x12 (MultiCore) change l'exécution CPU sans altérer les preuves de sécurité.

Nœud #3: Élévation au carré vectorielle à 8 voies élément par élément ($n0 * $n0) fusionnée dans les registres de cache L1 sans allocation sur le tas.
Vue assembleur symbolique (src/main.rls — 208 o dans .rl) ~8.8 µs assemble
cap 0x0
arena 0 len=4096 lane=f64x8 mut=false align=64 ver=1
output $n6
Traceur d'exécution boîte blanche (rul trace — 7 nœuds SSA) Cliquez sur une ligne pour synchroniser la trame binaire de 16 octets et l'assembleur
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] MUTATION D'ORDONNANCEMENT D'UN SEUL OCTET

Mutez 1 octet (Octet 2). Accélérez 4,72x au-delà du C écrit à la main.

Charge réelle : 10 000 000 de nombres flottants (tableau de 80 Mo) — filtrer > 1000.0, élever au carré et sommer. Cliquez pour muter l'Octet 2 (schedule_hint) ci-dessous : l'algorithme reste 100 % identique, tandis que le temps passe de 5,91 ms à 1,55 ms :

OCTET 2 ACTIF (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: Combine le tuilage L1 multi-cœur avec les métadonnées min/max de bloc (ArenaZoneMap) pour sauter les tuiles froides en O(1) sans lecture DRAM.

[A] AoS impératif + Vec::collect()
70.66 ms 1.13 GB/s
[B] Rust SoA idiomatique (filter().map().sum())
19.12 ms 4.18 GB/s
[C] C/Rust SoA à 8 accumulateurs écrit à la main
7.32 ms 10.92 GB/s
[D] Rul (.rl) Tier 2 SIMD fusionné (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
Preuve sur pipeline profond : BM-HORNER-50 (Polynôme à 50 étapes · 104 nœuds SSA · 80 Mo)

L'allocateur de registres YMM par balayage linéaire dans src/aot.rs compile un binaire ELF64 autonome de 3 872 octets en ~20,4 µs et s'exécute en 106,58 ms — égalant le C/Rust à 8 accumulateurs (107,96 ms) avec zéro LLVM.

[0x140] QUATRE MÉCANISMES DE PREMIERS PRINCIPES

Simple dans les premiers principes. Mathématiquement exact sur le silicium.

Les langages traditionnels compilent lentement car la machine doit lire du texte humain et deviner votre intention. Rul élimine toute supposition grâce à quatre mécanismes évidents :

01 · LE BINAIRE COMME UNIQUE SOURCE DE VÉRITÉ src/bytecode.rs

1. Zéro analyse de texte (0 % d'erreur de syntaxe)

Au lieu de forcer l'IA à taper des milliers de caractères sujets aux oublis de point-virgule, l'IA émet directement des briques binaires de 16 octets (ou assemble du .rls en ~8,8 µs). Un pipeline de 7 étapes traitant 10 millions de nombres ne pèse que 208 octets en .rl et compile en un exécutable Linux ELF64 autonome de 817 octets.

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 · PROPRIÉTÉ LINÉAIRE EN TEMPS O(N) src/verifier.rs

2. Tickets mémoire versionnés (Sécurité niveau Rust en nanosecondes)

Imaginez chaque tampon mémoire (Arena) comme une salle avec un ticket numéroté commençant à la version 1. Plusieurs instructions peuvent lire la version 1 ensemble (ReadLease 0b01). Dès qu'une instruction modifie les données sur place (AffineConsume 0b10), la salle passe en version 2 — toute instruction ultérieure détenant un ancien ticket version 1 est rejetée à la porte en 5,78 ns sans Borrow Checker lent.

TOKEN_OP (32-BIT) = [mode: 2b | arena_id: 14b | version: 16b]
0b01 ReadLease(arena=0, ver=1) ✓ Lecture partagée (ver reste à 1)
0b10 AffineConsume(arena=0, ver=1) → Mutation sur place & ver = 2
Reuse stale ReadLease(arena=0, ver=1) ✗ Rejet : StaleOrConsumedToken
03 · SANDBOX ZÉRO CONFIANCE & BORNES ProofEntry + CapMask

3. Certificats de bornes préalables & interrupteur matériel

Les colonnes de même longueur s'exécutent à pleine vitesse sans vérification de bornes dans la boucle (TRIVIAL_BY_SHAPE). Découper un tableau (ArenaSlice) ou indexer (Gather) exige un certificat de bornes de 16 octets (ProofEntry) au chargement. Et lorsque le masque matériel (CapabilityMask) vaut 0x0, le binaire est physiquement bloqué de tout accès réseau ou disque.

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 · AUDITABILITÉ BOÎTE BLANCHE rul trace & decompile

4. Transparence boîte blanche par rayons X (Jamais une boîte noire)

Les humains n'ont jamais besoin de taper du binaire pour garder 100 % du contrôle : les ingénieurs fixent la structure des données (ArenaDescriptor), les permissions matérielles (CapabilityMask) et les contrats de sortie (AssertContract) ; l'IA régénère le binaire .rl en quelques microsecondes. À tout moment, lancez rul decompile pour du texte lisible ou rul trace pour inspecter min, max, somme et NaN=0 à chaque étape.

Contrat humain → L'IA régénère le .rl
Vérification + Compilation en ~12 µs au total
Spéc. des 29 opcodes →
[0x180] MATRICE SYSTÈME & AGENT MCP

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

Comparaison architecturale sur le coût de parsing, la sécurité mémoire, la vérification des bornes, la latence de compilation et la sécurité du bac à sable.

DIMENSIONC (clang -O3)Go (gc)Rust (rustc + LLVM)Rul (.rl) v0.4
Auteur principalProgrammeur humainÉquipes d'ingénierie humainesIngénieurs système humainsAgents IA (avec outils d'audit boîte blanche pour humains)
Format de l'artefactTexte (.c, .h)Texte (.go)Texte (.rs)Binaire plat .rl (Instructions de 16 octets)
Coût d'analyse syntaxiqueÉlevéMoyenTrès élevé (Macros, AST)0 ms (mmap binaire direct sans copie)
Sécurité mémoireAucune (Pointeurs manuels)Ramasse-miettes (Pauses à l'exécution)Borrow Checker (Solveur de contraintes)TokenOp versionné (Vérification O(1) par nœud)
Vérification des bornesNon vérifiée (Débordements de tampon)Branchement à l'exécution à chaque accèsBranchement à l'exécution (sauf élision)Vérifiée au chargement via Shape + table ProofEntry
Temps de vérif. + compilationSecondesSub-seconde à secondesSecondes à minutes~5,8 ns/nœud Vérif. + ~6,4 µs ELF64 AOT
Sécurité du bac à sableProcessus OS completProcessus OS completProcessus OS complet (crates unsafe)CapabilityMask de 64 bits dans l'en-tête du fichier
STDIO JSON-RPC 2.0 · src/mcp.rs

Serveur Model Context Protocol intégré (rul-mcp)

Serveur stdio JSON-RPC 2.0 sans dépendance exposant directement aux agents IA autonomes 6 outils natifs de vérification, test différentiel, autotuning et compilation AOT.

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

Assemble les instructions symboliques .rls en une image binaire .rl 128 bits et exécute le vérificateur statique O(N) en une passe.

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

Exécute le programme vérifié sur Tier 0 (Oracle), Tier 1 (Stencil) et Tier 2 (L1 Fused) pour prouver l'équivalence bit à bit/ULP.

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

Balaye les politiques AutoL1Tile (0x10), SimdStream (0x11) et MultiCore (0x12) et sélectionne le meilleur débit matériel Go/s.

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

Génère un exécutable autonome Linux x86_64 AVX2 ELF64 (628 o – 1 037 o) par allocation linéaire de registres YMM.

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

Retourne les valeurs exactes min, max, somme/vrais, le compte NaN/Inf et l'échantillon sample[0..4] pour chaque instruction SSA.

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

Exécute des noyaux I64/U8 adressés par le contenu et vérifiés (sort, hash_join, group_by, simd_scan_byte) dans RulCasStore.

[0x1C0] FEUILLE DE ROUTE VERS v1.0

Du moteur colonnaire vérifié (v0.4) au langage système généraliste (v1.0)

Nous avons limité les versions v0.1–v0.4 aux pipelines de tableaux et vecteurs (29 opcodes) pour prouver d'abord le format binaire de 16 octets sur du vrai silicium. En quatre jalons, Rul s'étend pour remplacer Rust et Go :

Voir la feuille de route complète et les règles d'ingénierie →
v0.1.0 → v0.4.0 Base de production livrée
✓ EN PRODUCTION

Cœur SSA-DAG colonnaire à 29 opcodes, traceur boîte blanche & compilateur AVX2 ELF64 AOT

Validation sur matériel réel du format d'instruction binaire de 16 octets, du vérificateur O(N) en une passe (~5,8 ns/nœud), du moteur à 3 niveaux, du serveur rul-mcp et du compilateur Linux ELF64 sans LLVM (~6,4 µs).

  • [1] RulHeader de 64 octets, ArenaDescriptor de 16 octets, ProofEntry de 16 octets et NodeFrame de 16 octets sur 29 opcodes.
  • [2] Assembleur symbolique bidirectionnel sans perte .rls <-> .rl, CLI autonome rul, rul-bench et serveur rul-mcp à 6 outils.
  • [3] Allocateur de registres YMM par balayage linéaire (ymm2..ymm13) atteignant 51,53 Go/s (4,72x plus rapide que C) sur des tableaux de 80 Mo.
v0.5 Jalon 1 (Mois 1–2)
● EN COURS

Flux de contrôle généraliste, fonctions modulaires & types de données composites

Extension du jeu d'instructions de 16 octets au-delà des tableaux numériques pour gérer scalaires, structs, enums, chaînes UTF-8, tables de hachage, branchements et boucles à terminaison prouvée.

  • [1] Prise en charge native de i64, i32, u8, f32, structs à disposition fixe, unions étiquetées algébriques, chaînes UTF-8 validées et tables de hachage en arène.
  • [2] SelectBranch : branchement conditionnel exigeant que les deux branches convergent vers un état de version mémoire identique (vérifié en O(1)).
  • [3] RegionLoop & Call : boucles bornées avec témoins de terminaison ProofEntry et fonctions modulaires vérifiées sans inlining global.
v0.6 – v0.7 Jalon 2 (Mois 2–3)
○ PLANIFIÉ

Propriété du tas de niveau Rust & durées de vie des structs en temps O(N)

Généralisation des versions TokenOp 32 bits et des témoins ProofEntry 16 octets des tableaux plats vers les allocations de régions sur le tas et les emprunts de champs de structs.

  • [1] Allocation et désallocation déterministes de régions sur le tas liées à des jetons de propriété linéaire, avec zéro GC et zéro fragmentation malloc/free.
  • [2] Témoins ProofEntry pour les mutations disjointes de champs de structs et les durées de vie de sous-tranches sans copie vérifiés en O(1) par instruction.
  • [3] Protection complète contre use-after-free, double-free et aliasing sans résolution de contraintes Borrow Checker prenant plusieurs secondes.
v0.8 – v0.9 Jalon 3 (Mois 4–5)
○ PLANIFIÉ

Concurrence déterministe de style Go & E/S système contrôlées par CapabilityMask

Introduction de tâches légères, de canaux à transfert de propriété et de bits de capacité fins dans l'en-tête régissant les appels système fichiers, réseau et processus.

  • [1] Envoyer un tampon sur un canal typé effectue un AffineConsume sur le jeton émetteur et transfère la propriété au récepteur — éliminant les courses aux données au chargement sans GC.
  • [2] Extension du RulHeader.capability_mask 64 bits pour contrôler les lectures/écritures de fichiers, sockets réseau, minuteurs et sous-processus.
  • [3] Un binaire .rl avec CAP_NONE (0x0) est mathématiquement bloqué de tout appel réseau ou disque avant même le début de l'exécution.
v1.0 Jalon 4 (Mois 6)
○ PLANIFIÉ

Backends natifs multi-architectures (x86_64, ARM64, WASI) & preuves formelles Kani

Génération d'exécutables autonomes pour Linux, macOS, Windows et WebAssembly sans LLVM, appuyée par la vérification de modèles Kani et une suite de conformité v1.0 de 50 programmes.

  • [1] Génération de code natif zéro-LLVM pour x86_64 et AArch64 (ARM64) sur Linux, macOS et Windows, plus modules WASI déterministes.
  • [2] Preuves par model-checking borné (Kani) et fuzzing différentiel continu sur le décodeur binaire, le vérificateur O(N) et le générateur natif.
  • [3] Spécification binaire .rl v1.0 figée et suite publique de 50 programmes de test de conformité.
[0x1F0] RÉPONSES TECHNIQUES DIRECTES (AEO / FAQ)

Questions fréquemment posées — Du langage courant aux systèmes profonds

Des explications claires issues des premiers principes associées à des mesures empiriques exactes pour les ingénieurs, chercheurs et moteurs de réponse IA.

Q01 Qu'est-ce que Rul (.rl) et pourquoi utilise-t-il un format binaire de 16 octets au lieu du texte humain ? +
L'IA pense en nombres et les CPU exécutent du binaire — pourtant des langages comme C, Go et Rust forcent l'IA à taper des milliers de mots humains et à attendre des secondes qu'un compilateur (rustc/LLVM) retraduise ce texte en binaire. Rul (.rl) supprime l'intermédiaire textuel humain : les agents IA émettent des briques binaires fixes de 16 octets (128 bits) portant l'Algorithme, l'Ordonnancement CPU et le Ticket de sécurité mémoire dès le départ — éliminant l'analyse de texte (0 ms) et compilant des exécutables Linux ELF64 autonomes en ~6,4 µs.
Q02 Comment Rul vérifie-t-il une sécurité mémoire de niveau Rust en ~5,8 ns par instruction sans Borrow Checker lent ? +
Imaginez chaque tampon mémoire (Arena) comme une pièce dotée d'un ticket de version numéroté commençant à la version 1. Plusieurs instructions peuvent lire la version 1 en même temps grâce à un bail partagé ReadLease (0b01). Lorsqu'une instruction modifie le tampon sur place via AffineConsume (0b10), elle vérifie que le tampon est mutable et fait passer la pièce à la version 2. Toute instruction ultérieure détenant un ticket périmé de version 1 est rejetée à l'entrée en temps O(1) lors d'une seule passe avant (~5,78 ns/nœud) — aucun solveur Borrow Checker de plusieurs secondes n'est requis.
Q03 Si les humains n'écrivent pas les fichiers binaires .rl à la main, comment les équipes déboguent-elles et maintiennent-elles les systèmes Rul ? +
Les humains gardent 100 % du contrôle sans taper de binaire — tout comme les médecins lisent des radiographies sans les dessiner à la main : (1) Les humains fixent les règles en amont — les ingénieurs définissent les schémas de données (ArenaDescriptor), les interrupteurs de permissions matérielles (CapabilityMask 64 bits) et les contrôles d'acceptation (AssertContract), tandis que l'IA régénère le binaire .rl vérifié en quelques microsecondes ; (2) Texte lisible instantané via `rul decompile` qui reconvertit tout fichier .rl en assembleur symbolique `.rls` ; (3) Inspection par rayons X via `rul trace` qui affiche les valeurs exactes min, max, somme, le nombre de NaN/Inf et sample[0..4] à chaque étape.
Q04 Pourquoi la chaîne d'outils Rul est-elle écrite en Rust si Rul est conçu pour remplacer les langages textuels pour les agents IA ? +
Chaque nouveau langage système nécessite un langage hôte initial pour son premier compilateur d'amorçage (bootstrap) — tout comme le premier compilateur C a été écrit en assembleur et le premier compilateur Rust en OCaml. Nous avons construit le vérificateur Rul, le moteur d'exécution à 3 niveaux et le compilateur natif ELF64 en Rust pur sans dépendance sous `#![forbid(unsafe_code)]`. Une fois le binaire autonome `rul` installé, les utilisateurs et les agents IA vérifient, compilent et exécutent directement les programmes `.rl` sans avoir besoin de rustc, Cargo ou LLVM.
Q05 Comment Rul atteint-il 51,53 Go/s (4,72x plus rapide que le C écrit à la main) en ne modifiant qu'un seul octet ? +
Dans Rul, l'ordonnancement matériel (Octet 2 : schedule_hint) est orthogonal à la logique algorithmique (Octet 0 : opcode). Sur un pipeline de filtrage, élévation au carré et somme de 80 Mo (10 000 000 de f64), Rul sur un seul cœur (`0x11 SimdStream`) fusionne toutes les opérations dans des tuiles de cache L1 de 1 024 éléments au sein des registres AVX2 YMM, s'exécutant en 5,91 ms contre 7,32 ms pour du C à 8 accumulateurs écrit à la main (1,24x plus rapide). Muter l'Octet 2 de 0x11 à 0x12 (`MultiCore`) parallélise ces tuiles L1 sur tous les cœurs CPU (3,19 ms, 2,29x), et activer les métadonnées min/max de bloc `ArenaZoneMap` saute les tuiles froides en O(1) pour terminer en 1,55 ms (51,53 Go/s, 4,72x plus rapide que le C monocœur et 45,51x plus rapide que l'AoS impératif).
Q06 Rul peut-il remplacer Rust et Go pour les logiciels backend et systèmes généralistes ? +
Oui — c'est précisément l'objectif de la feuille de route v1.0 en quatre jalons : le Jalon 1 (v0.5) ajoute i64/i32/u8/f32, structs, unions étiquetées, chaînes UTF-8, tables de hachage, branchements SelectBranch vérifiés en O(1) et boucles RegionLoop à terminaison prouvée ; le Jalon 2 (v0.6–0.7) étend TokenOp et ProofEntry aux allocations sur le tas par régions et aux emprunts de champs de structs ; le Jalon 3 (v0.8–0.9) introduit des tâches légères et des canaux à transfert de propriété de style Go ainsi que des appels système OS contrôlés par CapabilityMask ; le Jalon 4 (v1.0) livre des backends natifs sans LLVM pour x86_64, ARM64 et WASI appuyés par des preuves formelles Kani.