The verification work at Cornell and Bell Labs is grounded in significant practice. Moreover, the tools we use have been constantly evolving toward more open architectures. The tools we now use for Ensemble are formally based. We have interoperable representations between type theory and ML.
Our research over the years has been characterized by improving our tools, especially to more open systems, more flexible logical frameworks and richer type theories. We know how to attack the technical problems based on our fifteen years of experience in the area. We have assembled a research team that can make significant progress.