Compile-time HOL Proof System

The Problem

Testing finds bugs. Code review catches some more. But testing can only cover the inputs you think to try, and review is limited by human attention. In safety-critical, financial, cryptographic, and defense systems, “probably correct” isn’t good enough.

One missed edge case in a medical device, a cryptographic library, or a trading engine can mean patient safety incidents, security breaches, or millions in losses. Traditional development tools leave a gap between “tested” and “proven.”

The Solution

The GDS Compile-time HOL Proof System closes that gap. It uses higher-order logic (HOL) to mathematically prove that your Rust code is correct at compile time. If the code compiles, it is correct — not by assertion, but by mathematical demonstration from foundational axioms. Zero runtime cost. The original code is emitted unchanged.

Who Benefits

Quick Start

Add pathways-prove to your Cargo.toml and annotate functions with #[proven]:

# Cargo.toml
[dependencies]
pathways-prove = "0.1"

use pathways_prove::proven;

#[proven(pre = "x: nat, y: nat", post = "result = x + y")]
fn add(x: u64, y: u64) -> u64 {
    x + y
}

The proof runs at compile time. If the code compiles, its correctness has been mathematically verified. Zero runtime cost — the original function is emitted unchanged.

Mathematical Foundations

The proof system is built on a minimal, auditable foundation: 4 axioms, 10 foundational concepts, and 10 primitive inference rules. Every theorem in the library — over 1,400 proofs spanning 77 mathematical domains — is derived from this foundation through legitimate inference alone. After bootstrap, the definition context is permanently sealed. No shortcuts. No unverified assumptions. No back doors.

The 4 Foundational Axioms

After these four axioms are admitted, the entire definition context is permanently sealed. No new axioms, constants, type constructors, or definitions can ever be introduced through any mechanism. There is no unlock. There is no back door. All subsequent mathematics must be derived through inference from these axioms and the 10 primitive rules alone.

The 10 Foundational Concepts

Everything in the proof system — from basic arithmetic to concurrency proofs to cryptographic verification — is constructed from these 10 concepts:

The 10 Primitive Inference Rules

Theorems are opaque values — constructable only through these 10 rules. Rust’s module privacy system enforces this boundary at the language level. There is no way to forge a theorem, no escape hatch, no unsafe bypass. If a Thm value exists, it was proven.

Architecture: Trust by Construction

The proof system enforces correctness through three architectural layers, each of which is load-bearing. Remove any one and the guarantees collapse.

Available Macros

What You Can Prove

• Functional Correctness: Functions produce the correct output for all possible inputs, proven by induction, case analysis, and structural reasoning.
• Memory Safety: No use-after-free, buffer overflows, null dereferences, or dangling pointers — mathematically proven, not just borrow-checked.
• Heap Verification: Allocation tracking for Box, Vec, and raw allocations. Proves freedom from use-after-free, double-free, and memory leaks across all exit paths.
• Resource Tracking: File descriptors, MMIO mappings, DMA buffers, and IRQ handlers tracked from acquisition to release. Proves no resource leaks, no use-after-release, and no double-release.
• Panic Freedom: Proves unreachable panics for unwrap(), expect(), split_at(), remove(), and all library calls with implicit panic conditions. Tracks guard facts and transitive panic risk through call chains.
• Obligation Tracking: 50 violation classes across 5 phases — arithmetic overflow, cast truncation, division by zero, shift bounds, pointer validity, aliasing, array bounds, lock ordering, information leaks, MIR divergence, and more. Every obligation must be discharged or the build fails.
• Concurrency Correctness: Freedom from data races, deadlocks, priority inversions, and livelock. Verified mutex semantics, lock-free progress, and memory ordering guarantees.
• Deadlock Detection: Lock ordering validation, ABBA cycle detection across function boundaries, guard scope enforcement, bare condvar wait detection, and mutex invariant tracking.
• Taint Analysis: Secret-tainted variable propagation through all operations. Detects secret-dependent branches (timing leaks), secret-dependent memory accesses (cache leaks), and secret-dependent variable-time instructions. Enforces declassification at public boundaries.
• Security Properties: Information flow non-interference, access control invariants, capability confinement, constant-time execution, and side-channel resistance.
• Cryptographic Correctness: Hash function collision resistance, signature unforgeability, encryption semantic security, key exchange safety, and protocol composition.
• Container Proofs: 10 verified container families (bitmap, buffer, deque, heap, list, map, pool, queue, set, tree) with 30+ concrete types, each with formally proven capacity invariants, ordering, and lock-free correctness.
• Real-time Bounds: Worst-case execution time bounds proven for safety-critical scheduling. Instruction-level cycle counting with architecture-specific latency models.
• Assembly Verification: Register state, flag transitions, clobber sets, stack balance, and memory effects verified for inline assembly across all supported architectures.
• Termination: Well-founded recursion and loop termination with formally verified ranking functions and decreasing measures.
• Ownership & Separation: Linear types, move semantics, heap separation (frame rule), and resource allocation/deallocation correctness.
• Tactic System: 10+ tactics (conj_tac, disch_tac, gen_tac, spec_tac, case_split_tac, induction_tac, arith_tac, subst_tac, rewrite_once_tac, mp_tac) plus 28 derived inference rules for building proofs compositionally.
• Term Normalization: Automatic canonicalization, constant folding, commutativity/associativity normalization, and proof-driven rewriting from the theorem library.

Obligation Tracking: 50 Violation Classes

Every #[proven] function generates proof obligations that must be discharged or the build fails. The system tracks 50 distinct violation classes across 5 phases, from arithmetic overflow to MIR divergence. Obligations are classified by severity: hard-reject (build fails), heuristic discharge (auto-provable), and informational (logged for audit).

Verified Container Library: 10 Families, 30+ Types

The pwos-containers crate provides 10 container families with 30+ concrete types, each with formally proven capacity invariants, ordering properties, and lock-free correctness. All container operations are modeled as HOL terms for compositional reasoning via #[proven].

Heap Verification

The heap verifier tracks every allocation from creation to deallocation across all exit paths, proving freedom from the three critical heap safety violations:

Resource Tracking

Beyond heap memory, the system tracks four categories of system resources from acquisition through release, proving that every resource is properly cleaned up on all exit paths:

Deadlock Detection

The verifier performs static deadlock analysis by tracking lock acquisition ordering within and across function boundaries:

Tactic System & Derived Rules

Beyond the 10 primitive inference rules, the proof system provides 10+ high-level tactics and 28 derived inference rules for building proofs compositionally:

Tactics

Derived Inference Rules (28 Beyond the 10 Primitives)

Hardware Verification Support

The asm_proven! macro verifies inline assembly across 4 architectures with full register models, flag tracking, cycle counting, memory ordering, and peripheral device state machines. Every instruction effect is modeled as a HOL term.

Architectures & Register Models

Peripheral Device State Machines

Hardware peripherals are modeled as state machines with typed MMIO registers, port I/O, and DMA effects. Every device interaction generates HOL terms for verification:

Virtualization (Intel VT-x / VMX)

Instruction Cycle Cost Accounting

Per-instruction latency and throughput models for WCET (worst-case execution time) analysis. Conditional branches split the context; both paths are tracked independently with min/max cycle bounds merged at join points:

Theorem Library: 1,400+ Theorems Across 77 Domains

Over 1,400 pre-verified theorems organized across 77 mathematical domains, all derived from the 4 foundational axioms through legitimate inference. Every theorem has tracked dependencies and has passed mandatory quality gates (unconditional, non-tautological). All theorems are loaded via stack-safe queue dispatch during the sealed bootstrap phase.

Feature Breakdown by Target

Every capability across Rust code, inline assembly for all supported architectures, and WebAssembly:

How We Compare

No other tool combines compile-time theorem proving, native Rust integration, assembly verification, and a pre-built proof library. Here is how the Pathways HOL Proof System compares to the leading formal verification tools:

✓ = Full support    ~ = Partial / limited    ✗ = Not supported    Verus uses a verus! macro extending Rust syntax; Creusot uses Pearlite; Prusti uses proc-macro attributes with custom operators. Dafny is a standalone verified language (not Rust) with integrated verification. F* assembly support is via the Vale DSL (x86-64 and AArch64). Coq/Rocq assembly and crypto via CompCert, Bedrock, and FIAT-Crypto (deployed in BoringSSL, Go, Firefox). SPARK certification support covers DO-178C (Level A), Common Criteria (EAL 5+), EN 50128, ISO 26262, and IEC 61508.

Licensing & Pricing

The HOL proof system is distributed as a Rust crate via Cargo. License keys are cryptographically signed tokens validated at compile time. Each license is tied to a single user and can be activated on up to two unique machines.

* “Rust developers” includes anyone who writes, reviews, modifies, or interacts with Rust code in any capacity — including through AI-assisted development tools.

Support Contracts

Support is available as a separate annual contract for Business and Enterprise tiers: