sergio/takana

Verificado en OVMF con el kernel linux-metal-kexec recién construido
(b3:965acc37…, CONFIG_KEXEC_FILE=y confirmado en el .config sellado):

  BdsDxe: starting Boot0002 "UEFI Misc Device"   ← el firmware, UNA vez
  KEXEC-PRUEBA: kernel = 6.16.12
  ✓ kernel cargado en memoria
  ⚡ saltando — el userspace muere ACÁ. Esto no vuelve.
  KEXEC-PRUEBA: kernel = 7.1.2
  KEXEC-PRUEBA-LLEGADA: este kernel NO lo arrancó el firmware

La prueba no es que aparezca el 7.1.2: es que "BdsDxe: starting" aparece
UNA SOLA VEZ. Dos kernels distintos corrieron y el firmware sólo
intervino en el primero. Y el 7.1.2 vive dentro del initramfs, sin
entrada de arranque, así que el firmware no podría haberlo lanzado.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HHAKWoBqof9XvsYCvDicEj

diff --git a/docs/adr/0017-ciclo-de-vida-del-kernel.md b/docs/adr/0017-ciclo-de-vida-del-kernel.md
index 7b1ba98c..e817dadf 100644
--- a/docs/adr/0017-ciclo-de-vida-del-kernel.md
+++ b/docs/adr/0017-ciclo-de-vida-del-kernel.md
@@ -92,6 +92,27 @@ la norma del mercado.
 > workspace que comparten dos frentes. El cmdline viaja **con su NUL** — el kernel cuenta
 > `cmdline_len` incluyendo el terminador, y es el error clásico de esta llamada.
 >
+> **VERIFICADO SALTANDO DE VERDAD (2026-09-12), en OVMF:**
+>
+> ```
+>   BdsDxe: starting Boot0002 "UEFI Misc Device"      ← el firmware arranca UNA vez
+>   KEXEC-PRUEBA: kernel = 6.16.12                    ← linux-metal-kexec, con CONFIG_KEXEC_FILE
+>   --- cargando el destino (7.1.2) y saltando:
+>   ✓ kernel cargado en memoria
+>   ⚡ saltando — el userspace muere ACÁ. Esto no vuelve.
+>   KEXEC-PRUEBA: kernel = 7.1.2                      ← linux-metal-dual, OTRO kernel
+>   KEXEC-PRUEBA-LLEGADA: este kernel NO lo arrancó el firmware
+> ```
+>
+> **La prueba no es que aparezca el 7.1.2: es que `BdsDxe: starting` aparece UNA SOLA VEZ.** Dos
+> kernels distintos corrieron y el firmware sólo intervino en el primero. Y el 7.1.2 no está en
+> ninguna entrada de arranque —vive dentro del initramfs—, así que no hay forma de que el firmware lo
+> hubiera lanzado aunque hubiera querido.
+>
+> *(El banner `Linux version` sale una sola vez en el log porque el cmdline horneado del kernel de
+> arranque lleva `quiet loglevel=3`. No es que arrancara un solo kernel: los dos `uname -r` lo
+> desmienten.)*
+>
 > **Y esto responde media decisión abierta n.º 2.** `recipes/linux-metal-kexec.toml` es una variante
 > cuya única diferencia es `CONFIG_KEXEC_FILE=y`. Variante y no flag en la canónica porque el
 > `.config` **es** la identidad del artefacto (SDD 22 §1) y esa decisión es del usuario; comprobado