Jason Gross

Jason Gross
Occupation	Founder of Theorem
Known for	Program verification, Fiat Cryptography, contributions to the Rocq (Coq) proof assistant

Jason Gross is a computer scientist and entrepreneur who is the founder of Theorem (also known as Theorem Labs), a company developing artificial intelligence tools for program verification. Gross holds a Ph.D. in Electrical Engineering and Computer Science from the Massachusetts Institute of Technology (MIT), where his research focused on improving the performance of proof assistants.

Career

Academic research

Gross earned his Ph.D. from MIT, with his dissertation addressing the problem of making proof assistants faster when applied to real-world problems. During his academic career, he developed Fiat Cryptography, a project housed at MIT's Programming Languages and Verification group (PLV). According to Gross, Fiat Cryptography enables "tens of trillions of secure connections to the internet every day," underpinning the cryptographic prime number computations behind HTTPS connections.

Gross became a significant contributor to the Rocq proof assistant (formerly known as Coq), reporting what he describes as the plurality of all-time bugs in the software. He subsequently joined the Rocq core development team to help address those issues.

Theorem

Gross founded Theorem (accessible at theorem.dev and theoremlabs.com) to address what he describes as "the oversight problem in massively scaling up software deployment." The company's core product applies AI to program verification, aiming to make verification capabilities comparable in accessibility to writing code in languages like Python. The company's tagline describes its mission as enabling "even your systems engineers" to use formal verification techniques — a domain traditionally requiring specialized expertise in proof assistants and formal methods.

Theorem builds on Gross's extensive background in formal verification and proof assistants, translating academic research in these areas into practical tools for broader software engineering use.

Residence

Gross resides in the Bay Area, California.