14 noticias
El model checking de estados finitos —la verificación de sistemas mediante la exploración exhaustiva de todos sus estados posibles— ha sido técnicamente superado desde mediados de los años noventa por el model checking simbólico, capaz de manejar tamaños de modelo muy superiores. Sin embargo, sigue
TigerBeetle, una base de datos distribuida que emplea el protocolo de replicación Viewstamped Replication (VSR), ha incorporado a su metodología de pruebas un simulador determinista con conciencia de protocolo (protocol-aware DST). Esta aproximación permite verificar invariantes de seguridad y vivac
El artículo repasa los argumentos del clásico paper de 1979 'Social Processes and Proofs of Theorems and Programs', que sostenía que la verificación formal de programas estaba abocada al fracaso, y los contrasta con la situación actual. En 1979, los autores defendían que las demostraciones matemátic
Un ingeniero de Antithesis, Carl, relata cómo localizó y verificó el conocido bug de WAL-Reset de SQLite —un error de condición de carrera en el sistema de registro anticipado de escritura que llevaba oculto desde 2010— usando las skills de Claude para Antithesis. Tras la publicación de SQLite 3.51.
Marionette es una biblioteca de simulación determinista (DST) para el lenguaje Zig que permite probar sistemas distribuidos y de almacenamiento reproduciendo fallos difíciles de capturar en producción: escrituras truncadas por caídas, corrupciones de sectores, particiones de red o carreras entre tem
John Murray, ingeniero de Antithesis, presenta en la conferencia Software Should Work 2026 una charla titulada "Derivations to Deployments: Practical Nix in Production". En ella expone cómo la compañía adoptó Nix de forma intensiva en toda su pila tecnológica y en sus procesos de despliegue, movida
La plataforma de pruebas Antithesis ha identificado errores en todas las implementaciones del protocolo de consenso Raft que ha analizado, entre ellas HashiCorp Raft, Aeron Cluster, OpenRaft y MicroRaft. Los fallos detectados violan la principal invariante del algoritmo, conocida como seguridad de l
Andrew Kelley, creador del lenguaje de programación Zig, pronunció la charla «Don't Take the Black Pill» en el evento Software Should Work (SSW) 2026, un encuentro dedicado a reflexionar sobre el papel del software en la sociedad. La intervención, de 35 minutos, parte de la sensación generalizada de
En la P99 CONF 2025, Alex Pshenichkin, ingeniero de Antithesis, presentó una charla centrada en uno de los mayores obstáculos para llevar la prueba de sistemas distribuidos al siguiente nivel: la velocidad de simulación determinista. La prueba determinista (DST, por sus siglas en inglés) exige que c
Un ingeniero de Antithesis relata cómo la empresa consiguió finalmente «vencer» al Tetris de la NES, un objetivo que persigue desde 2021 y que quedó estancado en el nivel 160 cuando los jugadores adolescentes llevaron el rendimiento humano más allá de lo que su plataforma de pruebas había explorado.
Antithesis ha lanzado Hegel, una nueva familia de bibliotecas de pruebas basadas en propiedades, disponibles inicialmente para Rust y con planes de expansión a Go, C++, OCaml y TypeScript. Hegel busca replicar la calidad de las pruebas basadas en propiedades de Hypothesis en múltiples lenguajes, int
Antithesis ha lanzado 'Bombadil', una nueva herramienta experimental para automatizar las pruebas basadas en propiedades de interfaces de usuario web. La herramienta, disponible desde ahora, explora y valida automáticamente la corrección de las propiedades de la UI, con el objetivo de detectar error
Investigadores han demostrado con éxito la prueba autónoma del juego Super Mario Bros., utilizando un enfoque innovador inspirado en el artículo de Antithesis sobre 'State-Driven Talk'. El sistema, cuyo código fuente está disponible en GitHub, explora el amplio espacio de estados del juego sin inter
Antítesis, una empresa especializada en pruebas de software, ha desarrollado una técnica innovadora para integrar código C++ de un solo hilo con código Rust de múltiples hilos y asíncrono. Esta integración es crucial para su fuzzer, una herramienta que busca vulnerabilidades en software mediante la