Logo
Background

Papers &
Research

Whitepapers

Semantics-Based Execution and the LLVM Backend of the K Framework

Semantics-Based Execution and the LLVM Backend of the K Framework

This paper gives an overview of the K framework, the core of Pi² Labs's technology.

Download
Proof of Proof: A Verifiable Computing Framework

Proof of Proof: A Verifiable Computing Framework

This paper gives an overview of Pi²'s Proof of Proof approach to verifiable computing.

Download
Pi²'s Verifiability Stack

Pi²'s Verifiability Stack

This paper introduces Pi²'s Verifiability Stack, a three-tiered architecture comprising the Verifiable Settlement Layer (VSL), the Verifiable Language Machine (VLM), and the Verifiable Consensus Protocol (VCP).

Download

Formal Foundations

Nominal Matching Logic with Fixpoints

Nominal Matching Logic with Fixpoints

Extends matching logic with names, abstraction, and the N quantifier to provide complementary approaches for specifying languages with binders.

Download
A Logical Treatment of Finite Automata

A Logical Treatment of Finite Automata

Presents a sound and complete axiomatization of finite words using matching logic, with shallow embeddings of regular expressions and automata.

Download
Matching Logic Proofs Meet Succinct Cryptographic Proofs

Matching Logic Proofs Meet Succinct Cryptographic Proofs

Presents the research problem of producing succinct cryptographic proofs for checking matching logic proofs, introducing the Proof of Proof concept.

Download
PhD Thesis: Matching µ-Logic

PhD Thesis: Matching µ-Logic

Presents matching μ-logic as a unifying logic for specifying and reasoning about programs, with formulas called patterns expressing structure and behavior.

Download
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

Proposes proof generation for language frameworks, producing proof objects as correctness certificates checked by a trustworthy proof checker.

Download
A General Approach to Define Binders Using Matching Logic

A General Approach to Define Binders Using Matching Logic

Proposes defining binders in matching logic where binding behavior is inherited from the built-in existential binder, applied to λ-calculus and System F.

Download
Matching μ-Logic

Matching μ-Logic

Proposes matching μ-logic extending matching logic with least fixpoints, capturing modal μ-logic, temporal logics, and reachability logic as instances.

Download
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

Presents a complete formal semantics of x86-64 user-level instructions, the most widely used instruction set architecture in desktop computing.

Download
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine

Provides the first complete formal semantics of the EVM, enabling verification of smart contracts and analysis of the Ethereum blockchain.

Download
Matching Logic

Matching Logic

Presents matching logic, a first-order logic variant for specifying and reasoning about structure through patterns and pattern matching.

Download
Defining the Undefinedness of C

Defining the Undefinedness of C

Presents a negative semantics of C11 that rejects undefined programs, detecting all 77 categories of core language undefinedness in the standard.

Download
KJS: A Complete Formal Semantics of JavaScript

KJS: A Complete Formal Semantics of JavaScript

Defines a complete formal semantics of JavaScript in K, systematically testing against the ECMAScript conformance test suite.

Download
K-Java: A Complete Semantics of Java

K-Java: A Complete Semantics of Java

Presents K-Java, systematically defining every feature in the official Java Language Specification using the K semantic framework.

Download
A Formal Semantics of Python 3.3

A Formal Semantics of Python 3.3

Demonstrates formalizing the operational semantics of Python 3.3 in the K Semantic Framework, providing an interpreter and analysis tools.

Download
An Overview of the K Semantic Framework

An Overview of the K Semantic Framework

Comprehensive overview of K, an executable semantic framework using configurations, computations, and rules to define programming languages and calculi.

Download

AI Agents

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

Presents ProofBridge, a unified framework for automatically translating natural language theorems and proofs into Lean 4 using joint NL/FL embeddings and retrieval-augmented fine-tuning.

Download
TensorCommitments: A Lightweight Verifiable Inference for Language Models

TensorCommitments: A Lightweight Verifiable Inference for Language Models

Proposes TensorCommitments, a tensor-native proof-of-inference scheme using multivariate polynomial commitments and Terkle trees for lightweight verifiable LLM inference.

Download
OpenDebateEvidence: A Massive-Scale Argument Mining and Summarization Dataset

OpenDebateEvidence: A Massive-Scale Argument Mining and Summarization Dataset

Introduces OpenDebateEvidence, a comprehensive dataset of 3.5 million documents for argument mining and summarization sourced from competitive debate communities.

Download
TexShape: Information Theoretic Sentence Embedding for Language Models

TexShape: Information Theoretic Sentence Embedding for Language Models

Presents TexShape, an information-theoretic framework for training sentence embeddings that simultaneously optimizes compression, privacy, and fairness using mutual information estimation.

Download
iDML: Incentivized Decentralized Machine Learning

iDML: Incentivized Decentralized Machine Learning

Proposes iDML, a blockchain-based incentive mechanism using smart contracts to robustly incentivize participation, ensure model provenance, and prevent attacks in decentralized opportunistic machine learning.

Download

Stay Informed

Sign up for updates and never miss important announcements.

Subscribe

Follow us

Learn about company and product updates, upcoming events, rewards, and more.

LinkedIn