- Graphical output
- Partial dups
- Better error messages
- More canonicalization
- Query optimizer
- Mark's "havoc" operator
- Minimal automata
- The Φ dup erasure operator
- Packet parsing / types
- Import / export routing tables
- Union find
- Grammars beyond regular expressions (Floyd grammars?)
- SMT
- Verified version in Lean