# Pi² Labs — Complete Information

> Pi² is building Fast, a new payment system for the agentic economy.

## Company Overview

### Who We Are
Pi² Labs (Pi Squared Labs) is a technology company developing verifiable computing infrastructure. Rooted in over 25 years of academic research in formal verification and programming language semantics, Pi² Labs commercializes the K framework and matching logic into practical infrastructure for blockchain, financial markets, and AI verification.

### Mission
To build Fast, a new payment system for the agentic economy — enabling trust through mathematical proofs rather than assumptions.

### History
Pi² Labs was founded by Grigore Rosu, the creator of the K framework at the University of Illinois at Urbana-Champaign, and Sriram Vishwanath, an IEEE Fellow and professor at Georgia Tech. Grigore previously founded Runtime Verification, which pioneered formal verification in distributed financial markets and secured billions in assets. Pi² Labs represents the next evolution — applying formal methods to settlement infrastructure and AI verification.

## Products

### Fast
Fast is a real-time, verifiable settlement system designed for efficient markets. Built on the FastSet protocol, it combines the parallelism of the actor model with the decentralization of blockchains to enable massively scalable, verifiable claim settlement without requiring global consensus.

### Fast Terminal
Fast Terminal is the user-facing interface for interacting with the Fast network, providing tools for participants in the settlement ecosystem.

## Core Technology

### K Framework
The K framework is an executable semantic framework that uses configurations, computations, and rules to define programming languages and calculi. It allows language designers to write a single formal definition of a language and automatically generate parsers, interpreters, compilers, model checkers, and verification tools. Languages formally defined in K include C, Java, JavaScript, Python, x86-64 assembly, and the Ethereum Virtual Machine (EVM).

### Matching Logic
Matching logic is a first-order logic variant for specifying and reasoning about structure through patterns and pattern matching. It serves as the logical foundation for the K framework and enables mathematical reasoning about program behavior.

### Matching μ-Logic
An extension of matching logic with least fixpoints that captures modal μ-logic, temporal logics, and reachability logic as instances. This enables reasoning about complex program properties including termination, liveness, and safety.

### Proof of Proof
A verifiable computing framework that produces succinct cryptographic proofs for checking matching logic proofs. This bridges formal verification with blockchain consensus — rather than re-executing computations, validators can verify compact cryptographic proofs that the computation was correct.

### Verifiability Stack
A three-tiered architecture comprising:
- **Verifiable Settlement Layer (VSL)** — Handles settlement finality
- **Verifiable Language Machine (VLM)** — Executes computations with proof generation
- **Verifiable Consensus Protocol (VCP)** — Coordinates distributed agreement

## Leadership Team

### Grigore Rosu — Co-Founder & Chief Executive Officer
Grigore Rosu has spent his career transforming industries through technology, and now he's developing Fast, a new payment system for agents at Pi² Labs. After earning his Ph.D. in computer science from UCSD, he worked at NASA on critical spacecraft software. Later, as a professor at UIUC, he created the K Framework, a tool for formally verifying programming languages. He previously founded Runtime Verification, pioneering formal verification in distributed financial markets and securing billions in assets. Pi² Labs represents the next step in his journey, leveraging over 25 years of expertise to build a secure global payment system for agents.

### Sriram Vishwanath — Co-Founder
Sriram Vishwanath is the co-founder of Pi² Labs and a prominent researcher in AI/ML and distributed systems, focusing on enabling agents to transact autonomously and securely. An IEEE Fellow and Technical Fellow at MITRE Labs, Sriram holds the Byers Chair for Computer Engineering at Georgia Tech and previously taught CS at UT Austin. He has over 300 publications and 19,000+ citations. He's also a serial entrepreneur with three successful exits and advises startups valued at over $1 billion.

### Xiaohong Chen — Chief Technology Officer
Xiaohong Chen is a formal verification expert whose PhD thesis on matching μ-logic established key theoretical foundations for the company's technology. He leads the technical development of Pi² Labs' verification infrastructure.

### Lindsay Casale — Chief Marketing Officer
Lindsay leads marketing initiatives and brand strategy for Pi² Labs.

### Musab Alturki — Chief Operating Officer
Musab manages operations and organizational execution.

### Jeet Raut — Head of Strategy
Jeet leads strategic planning and business development.

### Ilja Zakharov — Head of Engineering
Ilja oversees the engineering teams and technical delivery.

### Ovidiu Damian — Head of Product
Ovidiu leads product development and roadmap.

### Yi Zhang — Chief Architect
Yi leads the system architecture and technical design.

### Jin Xing Lim — Technical Product Lead
Jin manages technical product delivery and coordination.

### Nicholas Harness — Ecosystem Lead
Nicholas develops and manages the partner ecosystem.

## Research Publications

Pi² Labs maintains an extensive body of academic research across three categories:

### Whitepapers (4)
1. **Semantics-Based Execution and the LLVM Backend of the K Framework** — Overview of the K framework, the core of Pi² Labs's technology
2. **Proof of Proof: A Verifiable Computing Framework** — Pi²'s approach to verifiable computing using succinct cryptographic proofs
3. **Pi²'s Verifiability Stack** — The three-tiered VSL/VLM/VCP architecture for verifiable settlement
4. **Actors and Blockchains, Together** — The FastSet protocol blending actor model parallelism with blockchain decentralization

### Research Publications (15)
5. **Nominal Matching Logic with Fixpoints** — Extends matching logic with names, abstraction, and the N quantifier
6. **A Logical Treatment of Finite Automata** — Sound and complete axiomatization of finite words using matching logic
7. **Matching Logic Proofs Meet Succinct Cryptographic Proofs** — The research problem behind Proof of Proof
8. **PhD Thesis: Matching µ-Logic** — Unifying logic for specifying and reasoning about programs
9. **Towards a Trustworthy Semantics-Based Language Framework via Proof Generation** — Proof generation for language frameworks
10. **A General Approach to Define Binders Using Matching Logic** — Defining binders in matching logic
11. **Matching μ-Logic** — Extends matching logic with least fixpoints
12. **A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture** — Complete formal semantics of x86-64
13. **KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine** — First complete formal semantics of the EVM
14. **Matching Logic** — First-order logic variant for pattern matching and structure reasoning
15. **Defining the Undefinedness of C** — Negative semantics of C11 detecting all 77 categories of undefinedness
16. **KJS: A Complete Formal Semantics of JavaScript** — Complete formal JavaScript semantics in K
17. **K-Java: A Complete Semantics of Java** — Complete Java semantics using K
18. **A Formal Semantics of Python 3.3** — Python 3.3 operational semantics in K
19. **An Overview of the K Semantic Framework** — Comprehensive K framework overview

### AI Publications (3)
20. **ProofBridge: Auto-Formalization of Natural Language Proofs in Lean** — Translating natural language proofs into Lean 4
21. **TensorCommitments: A Lightweight Verifiable Inference for Language Models** — Tensor-native proof-of-inference for verifiable LLM inference
22. **OpenDebateEvidence: A Massive-Scale Argument Mining and Summarization Dataset** — 3.5 million document dataset for argument mining (NeurIPS 2024)

## Website Structure

### Main Sections

**Homepage** (/)
- Hero section with company mission
- Product overview (Fast, Fast Terminal)
- Our solution and technology overview
- Research call-to-action
- Contact section

**Research Papers** (/papers)
- Papers hero and overview
- Whitepapers section (4 papers)
- Research publications section (15 papers)
- AI publications section (3 papers)
- Individual paper detail pages with summaries (/papers/[slug])

**About Us** (/about-us)
- Team overview with founder spotlights
- Company culture and values
- Open positions and careers (/about-us/[slug])
- Benefits overview

**Media Kit** (/media-kit)
- Brand guidelines and logos
- Press resources
- Company boilerplate

## Technical Information

### Website Technology
- Built with Next.js (App Router)
- TypeScript
- Tailwind CSS
- Local font loading (General Sans, GT Super Display)
- Optimized for search engines and AI discovery

### SEO and Discoverability
- Structured data markup (JSON-LD) for Organization, ScholarlyArticle, JobPosting
- Optimized for traditional search engines (Google, Bing)
- Optimized for AI search engines (ChatGPT, Perplexity, Claude)
- Dynamic sitemap with all pages and paper slugs
- AI-specific files (llms.txt, llms-full.txt)

## Contact and Social Media

- Twitter/X: [@pi2_labs](https://x.com/PiSquared)
- LinkedIn: [Pi² Labs](https://www.linkedin.com/company/fast-xyz)
- GitHub: [pi2-labs](https://github.com/pi2-labs)

## Frequently Asked Questions

### What does Pi² Labs do?
Pi² Labs builds verifiable computing infrastructure, combining formal verification research (the K framework, matching logic) with blockchain settlement technology (FastSet protocol) to create trustworthy systems for efficient markets.

### What is Fast?
Fast is a real-time, verifiable settlement system that uses the FastSet protocol to achieve massively scalable claim settlement without global consensus. It combines the actor model's parallelism with blockchain decentralization.

### What is the K Framework?
The K framework is an executable semantic framework for formally defining programming languages. A single definition automatically generates parsers, interpreters, compilers, model checkers, and verification tools. It was created by Grigore Rosu at the University of Illinois.

### What is Proof of Proof?
Proof of Proof is Pi² Labs' approach to verifiable computing that produces succinct cryptographic proofs for matching logic proofs, enabling blockchain validators to verify computations without re-execution.

### What programming languages has Pi² Labs formally verified?
Through the K framework, Pi² Labs' research has produced complete formal semantics for C, Java, JavaScript, Python, x86-64 assembly, and the Ethereum Virtual Machine (EVM).

### Who founded Pi² Labs?
Pi² Labs was co-founded by Grigore Rosu (creator of the K framework, UIUC professor, NASA veteran, Runtime Verification founder) and Sriram Vishwanath (IEEE Fellow, Georgia Tech professor, serial entrepreneur).

### Is Pi² Labs hiring?
Yes, Pi² Labs has open positions. Visit the About Us page for current openings.

---

Last updated: 2025
For the most current information, please visit https://pi2labs.org