Limitations of Czech

Doesn't understand program flow
only looks top down
has basic understanding of input, handling

Doesn't examine all possible states

Doesn't (yet) do size, return comparisons

Several outstanding bugs