rust

9 posts

model-checkingautoverusrustverification

AutoVerus convierte 40 horas de escritura de proofs en 3 llamadas a LLM. El truco es saber cuándo rendirse.

AutoVerus utiliza una red de agentes LLM para generar proofs de corrección de Verus para código Rust, automatizando más del 90% de las proof obligations mediante un bucle de generar-reparar-dischargar impulsado por el feedback del solver SMT.

La parte más difícil de la verificación formal nunca ha sido el verificador. Es escribir el proof. Dale a un ingeniero senior de Rust Verus, el verificador…
model-checkingllmrustformal-proofs

Los LLMs pueden generar código en Rust. Las pruebas formales son un problema completamente distinto.

Los grandes modelos de lenguaje escriben código en Rust sorprendentemente bueno, pero cuando les pides una prueba formal alucinan invariantes e inventan sintaxis que ningún verificador acepta. Esto es lo que realmente hacen bien, dónde fallan y cómo usarlos de todos modos.

Los LLMs pueden escribir Rust que compila e incluso pasa . Lo que no pueden hacer de forma confiable es escribir una prueba formal de que el código es correcto…
model-checkingrustverificationformal-methods

Puedes probar que tu código Rust es correcto sin escribir una sola prueba, pero el espacio de estados es la factura

Herramientas de model checking como Kani te permiten verificar propiedades de Rust con assertions en lugar de pruebas formales. El problema es lo que ocurre cuando tus bucles no tienen límites pequeños.

Puedes probar que tu código Rust es correcto sin escribir una sola prueba. La herramienta que lo hace se llama model checker, y para Rust el más práctico en…
capability-based-securityrustcap-stdsandboxing

Tus dependencias pueden leer cualquier archivo en disco. cap-std las obliga a pedir permiso.

La biblioteca estándar de Rust otorga autoridad de sistema de archivos ambiental a cada dependencia. cap-std la reemplaza con APIs basadas en capabilities que obligan al código a demostrar que tiene derecho a acceder a una ruta antes de abrirla.

Cualquier crate en tu árbol de dependencias puede abrir , escribir en tu directorio , o enumerar cada archivo en tu proyecto. La biblioteca estándar de Rust no…
type-level-correctnesserror-handlingtypescriptrust

Deja de Lanzar Errores que tu Type Checker No Puede Ver

Las excepciones lanzadas ocultan los caminos de fallo de tu sistema de tipos. Aquí te explicamos por qué los retornos de error explícitos hacen tu código más honesto, y cómo adoptarlos sin odiar tu vida.

La firma de tu función dice que devuelve un . No es así. Devuelve un o explota. El sistema de tipos simplemente no sabe nada de la segunda branch. Esta es la…
deep-divesmutation-testingrustcargo-mutantstest-quality

El mutation testing en Rust funciona, pero tus tiempos de compilación te lo harán pagar

cargo-mutants encuentra los tests que solo pretenden verificar tu código. Aquí te explicamos cómo funciona el mutation testing en Rust, qué detecta y si el coste en tiempo de compilación merece la pena.

Tienes un 100 % de cobertura de líneas. Cada branch se ejecuta. Cada función se llama. Entonces alguien cambia un por un en tu lógica de precios, ejecuta los…
deep-divesrustproperty-based-testingquickcheckproptest

Los Property-Based Tests en Rust Encuentran los Bugs que tus Unit Tests No Detectan

El example-based testing solo cubre los inputs que se te ocurrieron. El property-based testing genera datos aleatorios, verifica invariantes y reduce los fallos a contraejemplos mínimos mediante shrinking.

Escribiste una función . La probaste con y . Pasa. La envías a producción. Un usuario le pasa un slice de un solo elemento. Tu función lo descarta. Abren un…
deep-divesrustruntime-contractsperformance

Los Runtime Contracts de Rust Pueden Tener Costo Cero en Release Builds, pero el Compilador No Lo Hará por Ti

Rust elimina las debug assertions automáticamente, pero el verdadero design-by-contract necesita más que debug_assert!. Aquí te mostramos cómo construir runtime contracts de costo cero que desaparecen de tu release binary.

Rust puede hacer cumplir runtime contracts en desarrollo y borrarlos por completo de los release builds. La salvedad es que el lenguaje no trata los contracts…