Leadership Team

Clark Barrett is Co-Founder and Co-CEO of &Truth, where he co-leads the company's technical work. He is the Corbel Professor (Research) of Computer Science in the School of Engineering at Stanford University. Before coming to Stanford in 2016, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University.

His expertise is in automated reasoning and its applications. He was an early pioneer in satisfiability modulo theories, formal hardware verification, and neural network verification. More recently, he has also pioneered efforts on AI-assisted formal verification.

He has worked with a variety of industry teams, including as a visiting scientist at Google, a consultant at Apple and Meta, and an Amazon scholar at AWS. He is the director of the Stanford Center for Automated Reasoning (Centaur), co-director of the Stanford Center for AI Safety, and a member of the CSLib steering committee.

He is an ACM Fellow and a two-time winner of the Computer Aided Verification (CAV) award (2021, 2024).

Ilya Sergey is Co-Founder and Chief Science Officer of &Truth, where he co-leads the company's technical work. He is also an Associate Professor at the School of Computing of the National University of Singapore (NUS), where he leads the Verified Systems Engineering (VERSE) lab.

Together with his students, he co-created the open-source multimodal Lean-based verifiers Veil and Velvet, both of which have seen industrial adoption. He received his PhD from KU Leuven. Before joining NUS, he was a faculty member at University College London. He has worked with several industry teams, including as a research scientist at Meta and as a consultant at Zilliqa and Mysten Labs. Ilya's research spans programming language design, software verification, and distributed systems.

He is Review Committee Co-Chair for OOPSLA 2027, was General Chair of ICFP 2025, and organized the ICFP Programming Contest in 2019. He is the recipient of multiple distinguished paper awards, the 2019 Dahl–Nygaard Junior Prize, and research awards from Google, Meta, and Amazon.

Christopher Hsu is the Co-Founder, Co-CEO, and Executive Chairman of &Truth. He also serves on the Strategic Advisory Board of the Lean Focused Research Organization (FRO), a nonprofit organization supporting the development of the Lean proof assistant and its ecosystem.

Chris is President of Infinitude Foundation, dedicating philanthropy to AI safety, consciousness studies, and philosophy of mind. He is a seasoned executive and investor with over 20 years of experience spanning AI, strategic M&A, and early-stage, growth, and frontier technologies.

Previously, Chris was the Founding Partner & CEO of Kilometre Capital, Chief Investment Officer of Rocketeer Management, Managing Director at Citadel Investment Group, and Senior Advisor to EQT BPEA Private Equity.

Chris holds a B.S. in Management Science & Engineering from Stanford University. He ran his first marathon at age 11, held Ironman All World Athlete Silver status, and remains an active endurance athlete. His core interests span AI safety, consciousness studies, and perennial philosophy.

Linus Lee is Founding Executive and Chief of Strategy & Operations, overseeing operations, strategy implementation, and talent acquisition. As Managing Partner at Kilometre Capital, he has worked alongside Chris for more than 17 years, leading and executing over $20 billion in M&A transactions across software, internet, hardware, and enterprise technology.

Earlier in his career, Linus was a software developer at Athenahealth during its early and growth stages and provided strategic technology advisory services in Asian markets through Pauling Advisors. He earned a B.A. in English Literature from Harvard University, graduating magna cum laude and receiving the Thomas H. Hoopes Prize for outstanding scholarly work.

Gregory Malecha is Technical Lead and Member of Technical Staff, bringing deep expertise in modern C++ verification, systems software, and proof automation. As Director of Formal Methods at BlueRock Security, formerly BedRock Systems, he built and led the formal-methods team over roughly six years, serving as both technical architect and manager.

He developed BRiCk, a framework for verifying concurrent modern C++ in the Rocq (Coq) proof assistant, and led verification of the BedRock/BlueRock Hypervisor, applying machine-checked mathematical proofs to thousands of lines of industrial C++. His work spans low-level systems verification, extensible proof automation, and the intersection of formal methods and AI. Gregory earned his Ph.D. and M.S. in Computer Science from Harvard University and his B.S. in Computer Science from Rice University.

Sebastian Ullrich is Chief Lean Officer, bringing deep expertise in theorem proving, programming languages, and engineering leadership. As Co-Founder and Head of Engineering of the Lean Focused Research Organization, he co-leads its technical program alongside Leonardo de Moura, overseeing compiler engineering and user experience. A core architect of Lean 4, Sebastian developed foundational capabilities in incremental and parallel elaboration and the module system, advancing the theorem prover's scalability.

He co-authored “The Lean 4 Theorem Prover and Programming Language” and shared the 2025 ACM SIGPLAN Programming Languages Software Award for Lean. His research spans formal verification, metaprogramming, and compilers. Sebastian earned his Ph.D. in Computer Science from Karlsruhe Institute of Technology, graduating summa cum laude.

As Chief Business Officer, Drew Harman leads &Truth's commercialization strategy and execution, bringing extensive product, strategy, finance, and GTM experience across AI and enterprise software. Over the past decade, Drew has been an Operating Partner with Insight Partners, Saints Capital, Shasta Ventures, and Interwest Partners, serving as a board member and strategic advisor to portfolio companies. He has sat on more than twenty boards, ranging from early-stage ventures searching for product-market fit to growth-stage businesses with more than $100M in ARR.

Earlier in his career, he was a startup strategy, product, and marketing executive, including roles at Ariba as VP of Product Management and VP of Corporate Strategy. He also served on the board of the nonprofit Foundation for Prader-Willi Research. Drew holds an MBA from INSEAD and a BA from Harvard.

Curtis Spencer is Founding Advisor, bringing deep engineering and investment experience across developer ecosystems, AI, and cybersecurity. As Co-Founder and General Partner of Electric Capital, he helps lead an engineering-led venture firm focused on early-stage investments, with a history of backing formal methods. He co-created Electric Capital's open-source Developer Report, an annual analysis of crypto developer activity across hundreds of ecosystems.

Previously, Curtis was an engineering lead at Meta, working on News Feed, Events, and Developer Experience after joining through its acquisition of Spool, where he was Co-Founder and CTO. He also co-founded Cruxlux, which was acquired by Kosmix, later part of WalmartLabs. Curtis earned his B.S. and M.S. in Computer Science from Stanford University.

Gordon Stewart is Secure Systems Lead and Member of Technical Staff, bringing deep expertise in formal methods across defense research, commercial systems, and academia. As Associate Director of Secure and Resilient Systems at Riverside Research, he led the formalized-security group, applying formal methods to programs for DARPA and other U.S. national-security customers. Previously, Gordon led concurrency verification at BedRock Systems, later BlueRock, overseeing verification of its highly concurrent C++ hypervisor using Coq-based concurrent separation logic.

Gordon previously served as an Assistant Professor at Ohio University, researching probabilistic programming languages and formally verified machine learning. He earned his A.B. in Classics from Harvard University and Ph.D. in Computer Science from Princeton University, where he worked on the Verified Software Toolchain project.