# Código y señal de AlphaProof: pruebas de seguridad de código de máquina verificadas y suposiciones confiables

Published: 2026-11-11

Google DeepMind informa pruebas verificadas por máquina de propiedades de seguridad seleccionadas para un arnés de línea de comandos de libsignal compilado. Lean verifica la prueba, mientras los humanos aprueban la especificación y sus suposiciones. Un comparador separado verifica el teorema y todas las definiciones dependientes contra el objetivo aprobado.

Canonical: https://thedailydiff.dev/es-US/video/2026-11-10-signal-machine-proof/

## Lo que cubre este video

- Los agentes de IA producen pruebas candidatas; el kernel de Lean verifica si establecen la afirmación formal aprobada por humanos.
- El objetivo verificado es un arnés CLI de libsignal compilado particular, con semántica y contratos criptográficos de confianza.
- Probar el binario compilado elimina el compilador de Rust de la base de confianza para las propiedades declaradas de ese binario.
- Los investigadores informan dos reintroducciones aisladas de errores previamente corregidos que violan su teorema de seguridad simbólico.
- El comparador verifica el teorema y cada definición dependiente contra una especificación aprobada protegida; las enmiendas pasan por un proceso de revisión separado.

## Preguntas y respuestas

### ¿Qué probó AlphaProof Code sobre la implementación de Signal?

Google DeepMind informa pruebas verificadas de propiedades de seguridad seleccionadas para un arnés de línea de comandos de libsignal compilado. El documento técnico cubre la confidencialidad y autenticación de mensajes, con secreto hacia adelante y seguridad post-compromiso bajo modelos establecidos. El resultado mantiene condiciones sobre el atacante, la sesión y las suposiciones criptográficas. Su alcance excluye una garantía general para cada aplicación o instalación de Signal.

### ¿Quién decide qué debe establecer una prueba de seguridad generada por IA?

Los revisores humanos aprueban la especificación y sus suposiciones. El documento técnico de Google DeepMind describe a los agentes elaborando especificaciones con guía humana y a los revisores probando si las declaraciones capturan propiedades de seguridad significativas. Lean verifica la lógica de la prueba resultante. Los humanos siguen siendo responsables de elegir un objetivo sólido, revisar las suposiciones y juzgar los cambios propuestos a la especificación aprobada.

### ¿Por qué verificar el código de máquina compilado en lugar de confiar en el compilador de Rust?

Una prueba sobre el binario compilado establece las propiedades declaradas para ese artefacto directamente. El documento de Google DeepMind explica que un error del compilador que violara una de esas propiedades haría que el teorema fuera falso. Por lo tanto, el compilador de Rust deja la base de confianza para esta afirmación. La prueba todavía confía en el modelo de instrucciones, el kernel de Lean y los contratos criptográficos especificados.

### ¿Cómo evita el comparador que un agente de prueba debilite su objetivo?

El comparador verifica el teorema y cada definición de la que depende contra una especificación aprobada protegida. El documento de Google DeepMind dice que los agentes de prueba no pueden escribir en esa copia reservada. El verificador también verifica los axiomas permitidos y reproduce la prueba en un nuevo kernel. Las enmiendas de especificación propuestas siguen un proceso de revisión separado, mientras que los humanos siguen siendo responsables de la solidez del objetivo.

### ¿Cuál fue el veredicto de The Daily Diff sobre el flujo de trabajo de prueba verificada?

El veredicto de The Daily Diff fue SHIP IT. Niko implementaría el flujo de trabajo de prueba verificada porque la afirmación aprobada se mantiene separada del agente que produce la respuesta. Mantendría el alcance y las suposiciones adjuntos a cada resultado. El episodio informa el artefacto de prueba publicado de Google sin reconstruirlo de forma independiente y aprueba el flujo de trabajo dentro de esos límites de evidencia.

## Capítulos

- 0:00 ¿Quién verifica una prueba de seguridad de IA?
- 0:57 ¿Cómo se convierte una afirmación en un objetivo de prueba?
- 1:39 ¿Por qué probar el binario compilado?
- 2:16 ¿Qué propiedades de seguridad sobrevivieron a la brecha de implementación?
- 2:59 ¿Puede la especificación rechazar código defectuoso?
- 3:36 ¿Puede una prueba correcta responder la pregunta equivocada?
- 4:13 ¿Qué atrapa los objetivos cambiantes?
- 4:53 ¿Implementaría este flujo de trabajo de prueba?

## Transcripción traducida

Traducido de la narración original en inglés. El audio y los subtítulos disponibles son controlados por YouTube.

### ¿Quién verifica una prueba de seguridad de IA?

0:00 Una auditoría de seguridad de IA todavía suena como confiar en un chatbot. El nuevo resultado de Signal de Google viene con pruebas matemáticas, un kernel separado las verifica. En este video, ¿qué probó Google? ¿Y cómo evitan que un agente cambie los objetivos? Aquí está la respuesta útil. Los modelos escriben pruebas candidatas, y Lean verifica las pruebas contra una afirmación aprobada por humanos sobre código compilado seleccionado. Los humanos siguen siendo dueños de la afirmación y las suposiciones.

0:21 Puede verificar el resultado sin creer el discurso de victoria del modelo. Una verificación separada detecta el cambio silencioso de la pregunta. Lo seguiremos hasta las definiciones. Es martes, diez de noviembre, y este es The Daily Diff. AlphaProof Code es el marco de Google para escribir especificaciones de software con guía humana y generar pruebas verificadas con agentes de IA. Este estudio se enfoca en libsignal, la biblioteca de Rust que implementa el protocolo de mensajería de Signal dentro de un programa de línea de comandos particular.

0:45 Google anunció el trabajo hoy. Su artículo dice que cinco investigadores trabajaron durante cuatro semanas. Los agentes escribieron las pruebas, mientras los humanos dedicaron la mayor parte de su esfuerzo a las especificaciones. Los requisitos han encontrado una manera de convertirse en reuniones aún más costosas. La especificación dice lo que el programa debe hacer,

### ¿Cómo se convierte una afirmación en un objetivo de prueba?

0:59 qué controla un atacante y qué suposiciones necesita el argumento. Los revisores preguntan si captura la seguridad que le importa a la gente. Una respuesta bellamente verificada a una pregunta débil deja esa pregunta intacta. El equipo se basa en investigaciones anteriores sobre el handshake de Signal y su ratchet de clave de mensaje. Los análisis formales ya estudiaron esos diseños. La afirmación de Google conecta sus argumentos de seguridad a una implementación compilada de una biblioteca de producción sin modificar, donde el diseño debe sobrevivir al contacto con código real. El director de tecnología de Signal, Ehren Kret,

1:27 describe una expansión más allá de los alcances más pequeños de la verificación anterior. Los detalles de implementación incluyen mensajes fuera de orden y sesiones archivadas para mensajes retrasados. El software real guarda los recibos que su elegante diagrama tiró a la basura. Los investigadores compilan la biblioteca de Rust sin modificar con el compilador estándar

### ¿Por qué probar el binario compilado?

1:41 en un ejecutable de Arm sesenta y cuatro Linux. Sus teoremas describen ese binario usando un modelo de instrucción formal, alcanzando la brecha entre el código fuente y el código de máquina optimizado. Un error del compilador que rompa una propiedad declarada haría que su teorema fuera falso. Por lo tanto, el compilador sale de la base de confianza para este binario. Todavía se confía en el modelo de instrucciones y en el verificador de Lean. El límite de confianza se movió y tiene una dirección. Cerca de seis millones y medio de líneas de prueba verificada se basan en aproximadamente veintiséis

2:06 mil líneas de especificación y semántica de instrucciones confiables. Estos son recuentos de artefactos. Tratarlos como puntuaciones de inteligencia es como clasificar a los desarrolladores por el tamaño de su carpeta de módulos de nodos.

### ¿Qué propiedades de seguridad sobrevivieron a la brecha de implementación?

2:16 Los argumentos cubren la confidencialidad y autenticación de mensajes, con secreto hacia adelante y seguridad post-compromiso bajo modelos establecidos. Esas dos últimas describen límites al daño por clave robada y la recuperación después de intercambios recientes. Cada garantía tiene condiciones sobre el atacante y la sesión. Las primitivas criptográficas se encuentran detrás de contratos de confianza. La prueba asume que esas rutinas se comportan como se especifica y se basa en suposiciones de seguridad criptográfica. Una prueba idealiza la criptografía; la otra razona sobre las probabilidades de éxito del atacante.

2:42 Ambas tienen restricciones sobre los escenarios que cubren. Pregunte qué compilación, qué propiedad y qué suposiciones. Este resultado concierne al arnés de línea de comandos de los investigadores. La mensajería grupal es trabajo futuro, y el modelo computacional excluye el estado multi-dispositivo. Llamar a cada instalación de Signal libre de errores se sale del teorema. Los investigadores reintrodujeron dos errores de Signal previamente corregidos en

### ¿Puede la especificación rechazar código defectuoso?

3:02 copias aisladas y los compilaron. Las pruebas verificadas mostraron que esos binarios violaban el teorema de seguridad simbólico. Eso probó si la especificación podía rechazar implementaciones defectuosas reales. Su marca de verificación verde necesita una prueba roja. Google publica las especificaciones y pruebas con instrucciones de verificación. El repositorio dice que una compilación limpia lleva horas y mucha memoria. Leer el anuncio es considerablemente más fácil en la computadora portátil. El modelo de hardware y los contratos de confianza aún necesitan revisión.

3:26 No he reconstruido el enorme artefacto para este episodio. Estamos informando el resultado publicado y sus límites. Los de afuera tienen un camino para inspeccionarlo, lo que me importa más que otra vuelta de victoria de la IA. Ahora, la trampa.

### ¿Puede una prueba correcta responder la pregunta equivocada?

3:36 Lean puede aceptar una prueba correcta de una afirmación que no pide casi nada. Las suposiciones imposibles pueden hacer que un teorema sea vacío. Cambiar una definición enterrada debajo del teorema principal puede debilitar el objetivo. El documento diseña controles contra esto. El guardián mantiene una especificación aprobada reservada a la que los agentes de prueba no pueden escribir. Pueden proponer correcciones a través de un proceso de enmienda separado. El debilitamiento de la seguridad se escala como un posible error. La declaración de éxito del probador no tiene autoridad aquí.

4:00 Los humanos juzgan los cambios a las suposiciones de confianza, directamente o a través de su política, y revisan las enmiendas después de cada campaña. El juicio experto sigue siendo responsable. El agente puede solicitar una asignación diferente. No puede ponerse una calificación aprobatoria.

### ¿Qué atrapa los objetivos cambiantes?

4:13 Aquí está la comprobación prometida. El comparador de Lean compara el teorema y cada definición de la que depende con esa copia aprobada protegida. También verifica los axiomas permitidos y reproduce la prueba en un nuevo kernel. Debilitar silenciosamente una definición auxiliar, por lo tanto, cambia lo que se está comparando. Una prueba aceptada debe establecer el objetivo aprobado. Esto todavía deja a los humanos responsables de elegir un objetivo sólido y suposiciones honestas. Para su propio flujo de trabajo de IA, mantenga los criterios de aceptación fuera de los

4:37 permisos de edición del trabajador y revise los cambios propuestos por separado. El resultado de Google concreta esa separación. El escritor de pruebas hace el trabajo; el límite de verificación decide si cuenta. Si prefiere leer esto en lugar de escucharme decirlo, el diff llega a su bandeja de entrada cada mañana, gratis en the daily diff dot dev, enlace a continuación. Así que el veredicto de hoy es SHIP IT.

### ¿Implementaría este flujo de trabajo de prueba?

4:54 Yo implementaría este flujo de trabajo de prueba verificada porque la afirmación aprobada se mantiene separada del agente que produce la respuesta. Mantendría el alcance y las suposiciones adjuntos a cada resultado. Suscríbase, haga clic en la campana y dígame en los comentarios si lo habría sellado de manera diferente. Y esa es la diferencia de hoy. Soy Niko de Axrisi. Fusionar responsablemente.

## Fuentes

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub