Steven Obua holds a Diplom in mathematics with a focus on computer science from the Technische Universität München (TUM), where he also spent time studying at the University of San Francisco. He earned his PhD in interactive theorem proving from TUM, and as a member of the Isabelle development team during his doctoral studies, he made significant contributions to the Flyspeck project, which successfully verified the proof of the Kepler conjecture. 

His postdoctoral research included work on the verification of Microsoft's hypervisor and a brief but influential period at École Polytechnique Fédérale de Lausanne exploring the design of a novel theorem proving system. At the University of Edinburgh, he was the researcher co-investigator for ProofPeer, an EPSRC-funded project pioneering collaborative theorem proving.

Dr. Obua's career spans both academia and industry, where he has worked in content management, insurance, mobile app development, hardware and software formal verification, gaming and computer-aided design. He is currently developing Practal, a new system that aims to empower vision through precision, based on abstraction logic.