Como o Kiro da AWS usa lógica formal para encontrar problemas nas especificações antes do código