Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis system, Leon, which translates software into a functional language and uses SMT solvers to reason about paths in programs and specifications. Certain completeness results partly explain the effectiveness of verification and synthesis procedures implemented within Leon, in particular results on decidability of sufficiently surjective abstraction functions, and the framework of complete functional synthesis.