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…