We develop precise automated reasoning techniques: tools, algorithms and languages. The goal of these techniques is to help construction of verified computer systems.