Por que podemos provar matematicamente que um programa é 100% livre de bugs sem executá-lo nem uma única vez? A ciência da verificação formal
