Gypsy includeva specifiche e affermazioni nella lingua stessa. Parte del sistema di programmazione e della metodologia Gypsy era la generazione di condizioni di verifica (teoremi da dimostrare) che provavano la correttezza del codice.
Il programma Gypsy ha dimostrato , tra le altre cose, che, contrariamente alla credenza popolare, è IS possibile fornire codice completamente privo di bug. Il Message Flow Modulator era un piccolo programma, che si trovava su una linea seriale e passava attraverso i messaggi filtrati. L'MFM è stato sviluppato presso l'UT Austin. La suite di test di accettazione è stata sviluppata in modo indipendente da una squadra sulla costa occidentale. La MFM ha visto per la prima volta la suite di test di accettazione al test di accettazione del cliente presso PAX River, e ha superato, al primo tentativo, nessuna deviazione, nessuna rinuncia, niente yeabuts, niente NULLA. È passato. (Don Good, il principale investigatore del progetto, mi disse che era passato molto tempo prima che il suo telefono smettesse di squillare dopo che quella notizia era uscita.)