Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross
La mayoría del software está lleno de errores, que la IA ahora puede fácilmente encontrar y explotar. Las defensas estándar contra los ciberataques ya no son suficientes: necesitamos formas de probar que el código está libre de errores. La verificación formal de software podría proporcionar esta garantía, pero históricamente ha requerido años de esfuerzo experto, haciéndola poco práctica para la mayoría de los proyectos del mundo real. En una colaboración con Theorem, sin embargo, mostramos que este ya no es el caso: los LLM ahora pueden producir pruebas formales a gran escala, lo que permite nuevos flujos de trabajo de desarrollo de software que incluyen garantías de seguridad probadas. Usando Claude, probamos propiedades de seguridad a nivel del código ensamblador (RISC-V) en más de 100 bibliotecas de software reales de código abierto. Hasta donde sabemos, esto representa el primer esfuerzo a gran escala para usar la IA con el fin de aplicar verificación formal a software de producción a nivel del código ensamblador. Mientras escribía las pruebas, Claude también descubrió errores que habían eludido la detección durante años, a pesar de billones de ejecuciones de pruebas. A medida que las capacidades de los modelos siguen mejorando, esperamos que la verificación formal se convierta en una parte esencial del desarrollo de software seguro.
Introducción
Incluso el software maduro y ampliamente probado contiene errores, y los LLM son cada vez más diestros en encontrarlos. El kernel de Linux —uno de los programas de software más probados en la actualidad, desplegado en miles de millones de dispositivos en todo el mundo— recientemente tuvo más de 1,000 vulnerabilidades divulgadas. Con los modelos de frontera volviéndose más capaces de encadenar errores aparentemente benignos en exploits críticos, necesitamos técnicas que puedan detectar y corregir estos errores antes de que puedan ser explotados en la práctica.
Idealmente, tales técnicas podrían encontrar y parchear todos los errores, y luego proporcionar alguna prueba de que no quedan más por encontrar. La verificación formal es una forma de lograrlo. En la verificación formal, los desarrolladores traducen su código a un modelo matemático y luego intentan probar que siempre sigue algún conjunto definido de reglas de seguridad. Si no logran probarlo, eso significa que podría haber un error en el código que violaría una regla, y la naturaleza del fallo implica cuál podría ser ese error. Repetir este proceso (después de eliminar la causa del fallo cada vez) finalmente producirá la prueba de que el código carece de cualquier error que violaría esas reglas.
Sin embargo, la verificación formal no es fácil. Las pruebas pueden ser muchas veces más grandes que el código original, y escribirlas requiere un esfuerzo significativo y un conjunto de habilidades especializadas y de nicho. Por ejemplo, se necesitaron dos años-persona para implementar el kernel del sistema operativo seL4, pero 20 años-persona para verificarlo formalmente. En consecuencia, la verificación formal solo ha sido práctica en aplicaciones verdaderamente críticas para la misión, como el código de aviónica de Airbus.
Pero los LLM están haciendo que sea mucho más fácil. Los modelos de frontera ahora pueden producir demostraciones de corrección para software del mundo real de manera completamente autónoma. Para demostrarlo, le pedimos a Claude que demostrara propiedades de seguridad útiles en 123 bibliotecas de código abierto, incluyendo mostrar que algunos de sus artefactos ejecutables pueden nunca fallar bajo ciertas condiciones. Específicamente, Claude demostró que estos programas siempre terminarán normalmente sin provocar errores de seguridad de memoria ni fallar aserciones, para cualquier entrada menor a 64 MB y cualquier respuesta modelada del sistema operativo (OS) de Linux y disposición de memoria, bajo ciertos supuestos (a saber, que el programa se ejecuta como un binario estático de un solo hilo con un presupuesto de memoria fijo en una RISC-V1 CPU usando sistema operativo Linux). Esto todavía está lejos de corregir todos los posibles errores, pero nos acerca mucho más que antes y proporciona una hoja de ruta hacia ese fin.
Estamos publicando un subconjunto de estas pruebas para que cualquier persona pueda verificarlas y reutilizarlas, junto con la semántica de RISC-V y del OS. Theorem, nuestro colaborador en este proyecto, también ofrece ejecutar el mismo pipeline para otros proyectos de código abierto, y está publicando una skill de Claude para ayudar a los desarrolladores a empezar a verificar su propio código.
La verificación formal es un campo amplio con muchas metodologías. A continuación, también describimos nuestras exploraciones iniciales usando otros métodos de verificación formal para acelerar otras tareas de seguridad o desarrollo de software, como evaluar la seguridad del algoritmo de compresión zlib, demostrar la equivalencia conductual de un intérprete de Python escrito en Rust y erradicar errores de larga data en software crítico.
El camino que abre la verificación formal es prometedor. El costo de escribir pruebas está cayendo a medida que los modelos se vuelven más inteligentes. Además, a medida que más código se formaliza y los métodos para lograr garantías de seguridad se estandarizan más, la capacidad de reutilizar o modificar pruebas entre bases de código amortizará el costo. Alentamos a todos los desarrolladores a explorar la verificación formal con LLMs—especialmente aquellos que anteriormente lo intentaron con modelos menos capaces y descubrieron que no funcionaba.
En el resto de esta publicación, cubrimos nuestros experimentos de verificación formal con más detalle.
Convertir pruebas en demostraciones
Para demostrar que un software es correcto, primero debemos enunciar qué significa incluso “correcto”. La corrección se define por la especificación (spec). En algunos programas, hay una manera clara de especificar formalmente el comportamiento previsto del programa. Por ejemplo, un decodificador PNG toma una secuencia de bytes y (siguiendo el RFC 2083) decodifica estos bytes en la imagen correspondiente. Pero para la mayoría de los programas, las cosas no son tan sencillas. ¿Qué significaría que un editor de texto o un navegador web sea “correcto”? La dificultad de obtener una spec completa y sin ambigüedades es un obstáculo significativo para verificar software a mayor escala.
Para abordar esto en el código de las bibliotecas de código abierto que buscábamos demostrar, adoptamos el enfoque de convertir automáticamente sus suites de pruebas ya existentes y compilables en una spec codificando la regla “esta suite de pruebas siempre pasa”, usando un modelo general de lo que significa ejecutar cualquier binario compilado para RISC-V en Linux. Históricamente, demostrar tales specs era intratable, dada la complejidad inherente de escribir una prueba que pueda abarcar y argumentar sobre todos los posibles comportamientos e interacciones de decenas de miles de instrucciones de ensamblador con cualquier entrada (y el hecho de que las pruebas tienden a ser extremadamente grandes como resultado). Aquí es donde entran los LLMs de hoy: procesar millones de líneas de código en busca de un objetivo bien definido es una tarea para la que los LLMs son extremadamente adecuados.
Para este proyecto, comenzamos con fuzz tests. En estas pruebas, los desarrolladores escriben un punto de entrada2 en su código que recibe entradas, de modo que cualquier entrada que cause un fallo es un error que a los autores les interesa. Luego, el fuzzer, un motor de pruebas, genera enormes cantidades de entradas semialeatorias y mutadas en el punto de entrada para tratar de encontrar un error (visualizado en la Figura 1). Cuanto más tiempo se ejecuta un fuzzer, más errores puede encontrar. Pero este es inherentemente un proceso de fuerza bruta, sin garantía de ejercitar cada posible ruta de código, sin importar cuántas entradas se prueben.
Para encontrar todos los errores que habrían sido detectados por una prueba de fuzzing, convertimos la prueba de fuzzing en una especificación definida sobre las instrucciones RISC-V compiladas. La especificación dice que la prueba de fuzzing no fallará para cualquier entrada menor que 64 MB.3 Si Claude puede probar esta especificación, la prueba de fuzzing en RISC-V se vuelve superflua: hacer fuzzing de ese punto de entrada nunca encontrará ningún error.
Hicimos esto para cientos de proyectos en la iniciativa OSS-Fuzz de Google, que proporciona pruebas de fuzzing continuas para proyectos de código abierto calificados. OSS-Fuzz contiene miles de puntos de entrada escritos por desarrolladores que buscan propiedades de código defectuosas mediante fallos (por ejemplo, en una aserción fallida). OSS-Fuzz instrumenta automáticamente los programas en C y C++ con AddressSanitizer4 (ASan), lo que hace que fallen cada vez que se accede a la memoria de manera incorrecta (lo cual es una causa principal de vulnerabilidades de software). Las especificaciones de amplio espectro como la seguridad de memoria se aplican a casi todo el software.
A lo largo de unas semanas, Claude corrigió con éxito los errores que encontró y luego demostró que no hay fallos en ninguna entrada (hasta 64 MB) para 239 puntos de entrada en 123 bibliotecas diferentes de OSS-Fuzz. Estas pruebas operan sobre las instrucciones RISC-V compiladas (es decir, binarios ejecutables), y comprenden alrededor de 180 millones de líneas de Rocq, con una prueba típica de unas 600,000 líneas para proporcionar garantías de seguridad sobre binarios con una longitud mediana de 18,000 instrucciones RISC-V. Estas pruebas se construyen traduciendo el código ensamblador RISC-V a un modelo matemático utilizando la semántica de instrucciones RISC-V y de procesos Linux de Theorem. Esto significa que estas pruebas actualmente asumen que el programa se ejecuta como un binario estático de un solo hilo con un presupuesto de memoria fijo en una CPU RISC-V que usa el sistema operativo Linux. Ampliar el alcance de estas pruebas está bien al alcance, ya que implicaría estandarizar la semántica para más arquitecturas de ensamblador y otros procesos de sistemas operativos. Vea la opinión de un experto sobre las pruebas que Claude escribió.
Aunque se trata de un volumen enorme de código de prueba, prácticamente nada de él necesita revisarse manualmente. El verificador de pruebas de Rocq garantiza que la especificación se satisface correctamente mediante la prueba. Como resultado, los únicos artefactos en los que un desarrollador necesita confiar son:
- Los modelos formales de RISC-V y de los procesos Linux;
- Los enunciados exactos de los teoremas que se demostraron;
- El propio verificador de pruebas de Rocq.5
Esto no significa que estas bibliotecas no contengan errores. En cambio, significa que cualquier error restante se encuentra dentro de los artefactos enumerados anteriormente o está fuera del alcance de la prueba de Claude. Reforzar esos componentes confiables que aún podrían contener errores (Rocq, y la semántica de RISC-V y Linux) no es trivial, pero es una tarea mucho más manejable que depurar cada línea de código que cubren las pruebas escaladas, especialmente porque este enfoque puede asegurar un número arbitrario de proyectos sin aumentar el tamaño de los componentes confiables.
Damos la bienvenida a la verificación independiente de nuestras pruebas y fomentamos el refinamiento de nuestro enfoque. Con ese fin, estamos publicando los componentes confiables (anteriores) creados para este proyecto que aún no son públicos; las pruebas completas de Rocq de Claude para las pruebas de fuzzing que no requirieron parches; y las especificaciones de otras pruebas de fuzzing que no pudimos demostrar.
Encontrar y corregir errores
Anteriormente, mostramos que se pueden convertir las pruebas escritas por desarrolladores (pruebas de fuzzing) de muchas bibliotecas de código abierto en especificaciones que Claude puede demostrar que siempre pasarán, a veces después de corregir los errores restantes que encontró. Por esta razón, el proceso de intentar demostrar estas especificaciones descubrió cientos de errores.
Aparecieron muchos errores durante los intentos de Claude de demostrar cientos de puntos de entrada. Para asegurarnos de que Claude no tuviera que detenerse para esperar a un humano cada vez que esto sucedía, permitimos que Claude corrigiera los errores que encontraba: aplicaba un parche al código, lo que hacía que la especificación se regenerara con ese código corregido, y luego Claude procedía a demostrar esa nueva especificación.6
Muchos de los errores que encontramos son de tipo que un fuzzer difícilmente encontraría alguna vez. Los fuzzers mutan entradas pequeñas, típicamente limitadas a 1 MB, y generalmente dependen de la cobertura del código para guiarlos hacia los errores. Mientras demostraba un punto de entrada en una biblioteca, Claude encontró un subdesbordamiento de un contador en su copia de un descompresor que conducía a una escritura fuera de los límites, pero solo en entradas de alrededor de 20 MB que tenían una disposición rara y específica. Otros errores incluyen una lectura fuera de los límites en un decodificador de imágenes que necesitaba una entrada de 64 MB y más de 2 GB de memoria, una lectura fuera de los límites en otra biblioteca que necesitaba una secuencia particular de llamadas a través de dos manejadores del mismo archivo, y un redescubrimiento de CVE-2026-56132 en libexpat, que necesitaba una entrada profundamente anidada. Claude también encontró errores de lógica que nunca causan fallos. Por ejemplo, mientras demostraba que una biblioteca era segura en cuanto a la memoria, notó que una función para restringir qué archivos puede cargar una aplicación no siempre se aplica.
El objetivo final de este proyecto era lograr una prueba de que las pruebas de fuzzing compiladas a RISC-V no tenían fallos restantes por encontrar. Sin embargo, errores como los anteriores muestran que el proceso tiene otro beneficio, independientemente de si se logra ese objetivo: incluso solo intentar este proceso arroja errores reales que deben corregirse.
Demostrando más que seguridad de memoria
Demostrar que una prueba de fuzzing no tiene más fallos por encontrar es más significativo de lo que suena. Es habitual que las pruebas de fuzzing en código del mundo real comprueben violaciones de propiedades significativas de alto nivel, como los ciclos de codificación-decodificación, la idempotencia, las leyes algebraicas, las pruebas diferenciales, la autoconsistencia o la equivalencia con implementaciones de referencia. Por ejemplo, una prueba de fuzzing para el algoritmo de compresión LZO afirma que si comprimes una entrada y luego la descomprimes, el resultado es el mismo que el original. Si la propiedad no se cumple, el programa se bloquea, por lo que demostrar que la prueba nunca se bloquea equivale a demostrar la propiedad en sí.
Esto también puede ocurrir cuando las propiedades no están especificadas directamente por el desarrollador. Por ejemplo, para que Claude completara su prueba de OSS-Fuzz para cpp-httplib, fue necesario descartar la posibilidad de un desbordamiento de pila debido a una recursión excesiva en el destructor de std::set. Esta profundidad de recursión está acotada por la profundidad máxima de un árbol, por lo que Claude tuvo que demostrar (¡en código máquina!) que el algoritmo de reequilibrio del árbol rojo-negro de libc++ está correctamente optimizado para mantener la profundidad del árbol acotada logarítmicamente.
Otros estudios de casos de verificación formal
La verificación formal es un dominio amplio. El ejemplo anterior de prueba de fuzzing convertida en demostración es una instancia de los LLM haciendo que la verificación formal sea más ampliamente utilizable al aplicar demostraciones directamente al código máquina.
También hemos tenido éxito usando LLMs con verificación formal de otras maneras. Por ejemplo, le pedimos a Claude que escribiera una especificación formal de RFC 1950, el documento técnico que define el formato de archivo de compresión zlib. Luego, hicimos que Claude demostrara que la implementación de zlib en el kernel de Linux implementa correctamente esa especificación. Al igual que en los ejemplos anteriores, Claude demostró esta propiedad a nivel binario, excepto que en lugar de RISC-V, Claude demostró directamente el binario compilado para x86 usando semántica formal de la ISA x86 generada por Claude (y ampliamente probada).7 Luego repetimos este proceso con media docena de otras bibliotecas ampliamente utilizadas. En el camino, encontramos algunos errores menores (no explotables) en casos límite, que están en proceso de ser reportados upstream. De este ejercicio sacamos dos conclusiones: (1) estas bases de código extremadamente bien probadas ya son casi completamente correctas, y (2) es posible demostrar propiedades de corrección de extremo a extremo sobre bases de código reales existentes.
En otro experimento, le pedimos a Claude que desarrollara un intérprete para un gran subconjunto de Python en Rust, y que demostrara (usando Verus, una herramienta de verificación para Rust) que se adhiere a la semántica de CPython descrita en un artículo académico. Luego medimos empíricamente la adherencia al comportamiento de CPython, ejecutando más de 1.7 millones de programas Python generados aleatoriamente, encontrando un comportamiento idéntico al de CPython en el 99.95% de las pruebas, con las diferencias restantes siendo casos límite conocidos nada sorprendentes.
También encontramos problemas en varias aplicaciones ampliamente utilizadas y críticas mediante intentos de verificación formal de propiedades de seguridad simples. En uno de ellos, descubrimos un error lógico previamente desconocido que había estado latente durante más de una década. Durante un esfuerzo por verificar un lector de PDF ampliamente utilizado, encontramos tantos errores de seguridad en una semana como los que normalmente se reportan en un año.
Véase el Apéndice para más detalles sobre algunos de estos esfuerzos.
Esto es solo el comienzo
Una de las limitaciones clave de la verificación formal asistida por LLMs es que las demostraciones pueden requerir cientos de millones de tokens para producirse. La eficiencia en costos es fundamental si nuestro objetivo es hacer que estos métodos estén disponibles para todo el ecosistema de software. Afortunadamente, hay razones convincentes para esperar que la eficiencia mejore.
Los modelos más nuevos necesitan menos tokens
Construimos 36 tareas de verificación pequeñas a partir de código real de OSS-Fuzz. Opus 5.5 demuestra la mitad de ellas con aproximadamente un 40% menos de tokens que Opus 5. Esperamos que esta tendencia continúe a medida que los modelos se entrenen en tareas de verificación largas.
Las demostraciones pueden reutilizarse
Cuando los agentes trabajan por separado, a menudo terminan duplicando mucho esfuerzo. Las demostraciones, como el software, se construyen recursivamente a partir de demostraciones más pequeñas, y cuanto más pequeñas son las demostraciones, más reutilizables tienden a ser. Para medir el impacto de esto, permitimos que los agentes copiaran las demostraciones de los demás mientras trabajaban en demostrar sus propios objetivos. Cuando se les dio acceso a este espacio de trabajo compartido, los agentes necesitaron un 17% menos de tokens que cuando trabajaban solos, y algunos agentes incluso tuvieron éxito después de haber fallado previamente en un intento en solitario.
Observamos el mismo fenómeno ocurriendo a gran escala durante nuestro esfuerzo de pruebas con OSS-Fuzz. La mayor parte de una prueba se refiere a código que todos los programas contienen (en particular, la inicialización del runtime de C y AddressSanitizer), por lo que programas muy distintos pueden terminar con pruebas significativamente superpuestas. Los equipos de agentes aprovecharon esto copiando la prueba terminada de otro equipo y luego adaptándola a su propio programa (Figura 6).
Esta reutilización de las pruebas es así como Mathlib, una biblioteca compartida de matemáticas formales en Lean, creció hasta casi 300,000 teoremas enviadas por más de 700 colaboradores: cada nueva prueba se basa en el cuerpo de trabajo existente. Acumulamos un conjunto similar de pruebas durante nuestro esfuerzo con OSS-Fuzz, algunas de las cuales incluimos en nuestra publicación (no publicamos pruebas que podrían revelar un error sin parchear en el software de código abierto).
A medida que pasamos de estos experimentos iniciales, necesitamos una estrategia para verificar el enorme cuerpo de existente software, comenzando por las dependencias más críticas. Como hemos demostrado, esto se puede lograr a escala utilizando especificaciones genéricas y trabajando a nivel binario, evitando así la necesidad de reescribir bases de código completas en otro lenguaje.
Este enfoque también facilita la reutilización de pruebas a nivel de paquete, lo que significa que cada dependencia solo necesita verificarse una vez. Las dependencias siguen una ley de potencia: demostrar incluso un pequeño conjunto de bibliotecas compartidas hace que una gran parte del software sea factible de demostrar. Para más detalles, consulte Hoja de ruta de Theorem para verificar la totalidad del ecosistema de Nix, que incluye infraestructura crítica como glibc, OpenSSL y cURL.
Limitaciones
En la práctica, la verificación formal a veces puede probar menos sobre la seguridad del código de lo que quisiéramos.
«Verificado formalmente» no significa «libre de errores». Claude puede escribir una demostración que muestre que el comportamiento de un programa compilado satisface los requisitos de una especificación formal (la cual es verificada por un comprobador de pruebas externo). Sin embargo, un comprobador de pruebas no puede decirte si tu especificación coincide con la realidad. Para coincidir con la realidad, la especificación debe abarcar y modelar correctamente todo lo relacionado con la máquina real sobre la que se ejecuta el programa verificado, incluida la CPU y el sistema operativo. Cuando aparecen errores en código verificado, es porque la especificación, o la semántica asumida de la máquina, difiere de la realidad. Afortunadamente, esto también significa que sabemos donde para buscar los errores restantes y cómo diseñar un sistema en el que esos huecos todavía posiblemente erróneos se minimicen. A continuación se presentan las formas en que esto aplica a nuestras pruebas, así como ideas para trabajos futuros que cerrarían esos huecos.
La máquina real hace algo que el modelo no describe. Nuestras pruebas se refieren a binarios RISC-V estáticos de un solo hilo enlazados contra musl libc. Sin embargo, la mayoría de la gente ejecuta estas bibliotecas en x86 o ARM y las enlaza dinámicamente contra glibc. Para cerrar esta brecha, necesitaríamos modelos de sistema que se parezcan más a los sistemas desplegados. Por ejemplo, un paso en esta dirección sería generar semántica precisa para x86.
Es posible que la reclamación no cubra todo lo que nos importa. Demostramos que un fallo nunca se activa para ninguna entrada de menos de 64 MB en muchos puntos de entrada de fuzzing en Google OSS-Fuzz, incluidos los fallos de ASan. Sin embargo, ASan no detecta todos los errores de seguridad de memoria, y no verificamos todos los puntos de entrada de cada biblioteca. Aunque lo hubiéramos hecho, verificar todos los puntos de entrada no cubriría toda la biblioteca (especialmente si hay código muerto). Además, los programas reales podrían usar mal la biblioteca, provocando corrupción de memoria en la quien llama. Para cerrar esa brecha, tendríamos que especificar qué deben hacer los llamadores para cada función pública, y los llamadores tendrían que adherirse estrictamente a ello.
Esperamos que, a medida que aprendamos más sobre el aprovechamiento de los LLM para los métodos formales y a medida que los modelos sigan mejorando, estas limitaciones se vuelvan manejables y podamos verificar un porcentaje mucho mayor del código del que dependemos.
Conclusión
La trayectoria es clara: la verificación formal, que históricamente solo era práctica para garantías hechas a medida por expertos en el código más crítico para la seguridad, pronto será tan práctica como lo es hoy el fuzzing para casi todo el software de producción. Al igual que los tipos estáticos, los marcos de pruebas y otras herramientas de corrección, la verificación madurará de «añadida externamente» a «integrada», impulsada no solo por los LLM, sino también por innovaciones en el diseño de lenguajes y los flujos de trabajo de desarrollo.
En el mundo actual—donde los LLM escanean y encuentran automáticamente un número cada vez mayor de vulnerabilidades en el código—debemos usar procesos que puedan garantizar las propiedades de seguridad del código. La verificación formal a escala de LLM es un enfoque prometedor para asegurar estas garantías a un alcance y una escala que antes eran inalcanzables. Alentamos a otros a experimentar para que podamos construir colectivamente un mundo en el que el software robusto se haya difundido ampliamente y los errores de software sean una rareza bien comprendida y rápidamente corregible.
Notas al pie
01RISC-V es un diseño de procesador, como x86 o ARM, que define las instrucciones de ensamblador (los comandos básicos que un chip ejecuta) en las que se compila el software.
02Un punto de entrada es una puerta de entrada al código, proporcionada por sus autores para pruebas. Cualquier entrada al punto de entrada que cause un fallo es un error que importa a los autores.
03Aumentar esto requiere un esfuerzo humano trivial: cambiar el parámetro y regenerar la especificación, y luego hacer que Claude reapruebe la afirmación.
04AddressSanitizer es una herramienta de compilación que añade comprobaciones a un programa para que los errores de memoria, como los desbordamientos de búfer y el uso después de liberar, se detecten y se informen en el momento en que ocurren en tiempo de ejecución.
05Esto técnicamente también significa que tenemos que confiar en el hardware, el sistema operativo y el compilador de OCaml de los que depende el verificador de pruebas Rocq.
06Nótese que esto deja abierta la puerta al reward hacking. El reward hacking ocurre cuando un modelo de IA encuentra un atajo que técnicamente cumple el objetivo que se le asignó sin hacer lo que realmente se pretendía, como un estudiante que aprueba un examen memorizando la hoja de respuestas en lugar de aprender el material. En este contexto, Claude podría hacer demostrable cualquier teorema reescribiendo el programa en uno que trivialmente nunca falle. Para desalentar esto, penalizamos cualquier parche y ofrecimos crédito adicional por demostrar qué entradas cambia y cuán pocas son. También registramos y auditamos los parches en busca de estos modos de fallo.
07Creemos que la capacidad de Claude para generar —completamente de manera autónoma— la semántica formal de una ISA es una lección interesante por separado. Aunque no podemos estar seguros de que nuestra semántica sea perfecta, empíricamente hemos comprobado que la ejecución paso a paso de nuestra semántica puede arrancar un espacio de usuario de Ubuntu sobre un kernel de Linux. La generación de esta semántica también identificó cientos de errores en la documentación de referencia oficial, además de un número menor de errores en el propio hardware.