We present the edge-Street/ edge-Rabin environment for doing verification using language containment. This environment has a number of desirable properties compared with the L-process/L-automaton environment ([Kur87b]), which is a practical language-containment-based formal verification environment: * It contains the L-environment as a subset. * It can be exponentially more compact than the L-environment. * We present BDD-based algorithms for main verification functions in this environment, and argue that they are efficient. Furthermore, if the specifications come from the L-environment, our algorithms reduce to the algorithms of [HTKB92] and [HBK93] for the L-environment. * It is in some sense maximal, i.e. language containment check for the next natural extension to our environment is NP-complete (as opposed to polynomial.) We have implemented our algorithms in our verification tool, and will present a flexible user interface to this environment.