Todos los sistemas
En construcciónsistemas operativos2026
workaOS
Esto es lo más profundo que construimos, y es la razón por la que el resto nos sale bien. workaOS no se apoya en Linux: es un kernel no_std que arranca por el protocolo Limine, pide su propio framebuffer y funciona igual bajo BIOS que bajo UEFI. Encima va un modelo de capacidades donde la autoridad se otorga de forma explícita y lo demás se deniega, más un registro append-only con cadena de hash: si algo tuvo efecto, hay una entrada que lo prueba.
Stack
- Rust no_std
- Limine
- QEMU/KVM
- virtio-vsock
- virtio-blk
- Kani
- SMP
Recibos
Sin recibo, no hay efecto.
- Arranca bajo BIOS y bajo UEFI, con salida por serie verificable
Se comprueba con: scripts/qemu-test.sh --firmware bios | --firmware uefi - La imagen se reconstruye bit a bit idéntica
Se comprueba con: scripts/repro-check.sh - La cadena de hash del ledger se verifica en runtime
Se comprueba con: cap::ledger::verify_chain() - Sin autoridad no hay despacho: denegar es el default
Se comprueba con: cap::table — missing_authority_never_dispatches - Chromium real dentro de una microVM sobre vsock real
Se comprueba con: qemu-test.sh --test cu1b_chromium → CU1B-CHROMIUM-OK - La auditoría del kernel corre en estricto, sin filas pendientes
Se comprueba con: node gates/reaudit-os.mjs --strict
Lo que no reclamamos
No reclamamos verificación formal. Los arneses Kani están escritos pero no corren como gate, y eso queda dicho en PROOFS.md en lugar de escondido. Que una invariante pase en QEMU es evidencia, no una demostración sobre las entradas posibles.