Como a AWS está usando lógica formal para evitar bugs nas especificações antes do código