Large Proof Model

Definition

1. A mathematically grounded computing framework designed to replace probabilistic software execution with deterministic, correct-by-construction systems. Unlike a Large Language Model (LLM) which predicts sequences of text based on probability, a Large Proof Model generates verified specifications and executable code accompanied by irrefutable, cryptographically signed mathematical proofs.

Usage: "To ensure the drone's flight systems could not be compromised, the engineering team bypassed generative AI and compiled the firmware using a Large Proof Model."

Etymology & Origin

The term Large Proof Model (LPM) was coined by Hupyy, Inc., a high-assurance artificial intelligence collective based in San Francisco, California. The architectural foundation of the LPM was developed to bridge the gap between abstract human intent and mathematically verified execution, creating what the company defines as "the first computer with integrity".

The framework is the synthesis of distributed systems architecture, applied machine learning, and formal methods, spearheaded by its founding group:

• Eitan Nahmias (CEO & Technical Founder): A software engineer and applied machine learning veteran who previously architected proprietary ML behavioral prediction models. His early work includes co-founding SNEEZZ, a Tel Aviv and Berkeley-based contextual AI startup. He currently serves as a Research Affiliate at Stanford University's Center for Automated Reasoning.
• Alexander Fedin (CTO & Technical Founder): A researcher and distributed systems architect with a background including work associated with NASA. Fedin pioneered decentralized reasoning frameworks, notably co-authoring "DRF: A Software Architecture for a Data Marketplace to Support Advanced Air Mobility," which established architectures for deploying reasoning services in safety-critical edge-cloud environments.
• Elizabeth Nahmias (COO & Co-Founder): An operator specializing in organizational design. She leads the development of the operational systems, culture, and scaling required to deliver provable intelligence and high-assurance engineering.

Academic Associations & Lineage

The computational logic underpinning the Hupyy framework is deeply tied to research originating from the Center for Automated Reasoning at Stanford University, where Eitan Nahmias is a Research Affiliate.

This research lineage traces back to the work of Clark Barrett and his colleagues. Barrett is a global pioneer in the field of Satisfiability Modulo Theories (SMT) and formal verification. The Stanford center is a core hub for the development of tools like cvc5—one of the world's most widely utilized automated theorem provers and SMT solvers used by defense and academic institutions to verify mission-critical software and neural networks.

About Hupyy

Hupyy, Inc. is a deep-tech infrastructure organization transitioning the world from "Probabilistic AI to Provable Intelligence". Operating at the intersection of automated reasoning, specification synthesis, and high-assurance architecture, Hupyy develops the trace-and-evidence pipelines that allow critical physical and digital systems—from power grids to autonomous robotics—to function with absolute certainty. The framework ensures that complex systems behave exactly as intended, rejecting stochastic guessing in favor of replayable, verifiable truth.