VERIFICACIÓN FORMAL DE CONTRATOS INTELIGENTES
Dr. Christian Reitwiessner
@ethchris
github.com/chriseth
IC3-Ethereum Crypto Boot Camp
2016-07-26
Problema:
¡Es difícil escribir código correctamente!
Objetivo clave: alinear el modelo mental con el modelo de la máquina
Fácil de probar el comportamiento deseado, difícil de verificar la ausencia de comportamientos no deseados
Razón: las pruebas solo capturan una cantidad finita de casos
Esto es importante para Ethereum.
Al igual que para un servicio web, el atacante puede estar en cualquier lugar
El código fuente a menudo está disponible (bueno y malo)
Ejemplo destacado: The DAO