Crate oxiz_proof 

oxiz-proof

Proof generation and checking for the OxiZ SMT solver.

This crate provides machine-checkable proof output in various formats, enabling verification of solver results by external proof checkers.

Beyond Z3

While Z3 supports generic proofs, OxiZ aims to generate machine-checkable proofs (Alethe, LFSC) by default, making it more suitable for certified verification workflows.

Supported Formats

• DRAT: For SAT core proofs
• Alethe: SMT-LIB proof format
• Carcara: Proof checker compatibility for Alethe format
• LFSC: Logical Framework with Side Conditions
• Coq: Export to Coq proof assistant
• Lean: Export to Lean theorem prover (Lean 3 & 4)
• Isabelle: Export to Isabelle/HOL
• Theory: Theory-specific proof steps
• Checker: Proof validation infrastructure
• PCC: Proof-carrying code generation
• Merge: Proof merging and slicing utilities
• Diff: Proof comparison and similarity metrics
• Normalize: Proof normalization for canonical representation

Re-exports

pub use alethe::AletheProof;

pub use alethe::AletheProofProducer;

pub use alethe::AletheRule;

pub use alethe::AletheStep;

pub use carcara::CarcaraProof;

pub use carcara::to_carcara_format;

pub use carcara::validate_for_carcara;

pub use checker::CheckError;

pub use checker::CheckResult;

pub use checker::Checkable;

pub use checker::CheckerConfig;

pub use checker::ErrorSeverity;

pub use checker::ProofChecker;

pub use compress::CompressionConfig;

pub use compress::CompressionResult;

pub use compress::ProofCompressor;

pub use compress::get_dependency_cone;

pub use compress::trim_to_conclusion;

pub use conversion::ConversionError;

pub use conversion::ConversionResult;

pub use conversion::FormatConverter;

pub use coq::CoqExporter;

pub use coq::export_theory_to_coq;

pub use coq::export_to_coq;

pub use coq_enhanced::CoqProofTerm;

pub use coq_enhanced::CoqType;

pub use coq_enhanced::EnhancedCoqExporter;

pub use coq_enhanced::export_to_coq_enhanced;

pub use diff::ProofDiff;

pub use diff::ProofSimilarity;

pub use diff::compute_similarity;

pub use diff::diff_proofs;

pub use drat::DratProof;

pub use drat::DratProofProducer;

pub use drat::DratStep;

pub use explanation::ExplainedStep;

pub use explanation::ProofComplexity;

pub use explanation::ProofExplainer;

pub use explanation::Verbosity;

pub use fingerprint::FingerprintDatabase;

pub use fingerprint::FingerprintGenerator;

pub use fingerprint::ProofFingerprint;

pub use fingerprint::SizeFeatures;

pub use format::ProofFormat;

pub use heuristic::HeuristicType;

pub use heuristic::ProofHeuristic;

pub use heuristic::StrategyLearner;

pub use incremental::IncrementalProofBuilder;

pub use incremental::IncrementalStats;

pub use incremental::ProofRecorder;

pub use interpolant::Color;

pub use interpolant::Interpolant;

pub use interpolant::InterpolantExtractor;

pub use interpolant::Partition;

pub use isabelle::IsabelleExporter;

pub use isabelle::export_theory_to_isabelle;

pub use isabelle::export_to_isabelle;

pub use isabelle_enhanced::EnhancedIsabelleExporter;

pub use isabelle_enhanced::IsabelleMethod;

pub use isabelle_enhanced::IsabelleProof;

pub use isabelle_enhanced::IsabelleType;

pub use isabelle_enhanced::IsarProofBody;

pub use isabelle_enhanced::export_to_isabelle_apply_style;

pub use isabelle_enhanced::export_to_isabelle_enhanced;

pub use lazy::LazyDependencyResolver;

pub use lazy::LazyNode;

pub use lazy::LazyProof;

pub use lazy::LazyStats;

pub use lean::LeanExporter;

pub use lean::export_theory_to_lean;

pub use lean::export_to_lean;

pub use lean::export_to_lean3;

pub use lean_enhanced::EnhancedLeanExporter;

pub use lean_enhanced::LeanProofTerm;

pub use lean_enhanced::LeanTactic;

pub use lean_enhanced::LeanType;

pub use lean_enhanced::export_to_lean_enhanced;

pub use lean_enhanced::export_to_lean_term_mode;

pub use lfsc::LfscDecl;

pub use lfsc::LfscProof;

pub use lfsc::LfscProofProducer;

pub use lfsc::LfscSort;

pub use lfsc::LfscTerm;

pub use merge::merge_proofs;

pub use merge::slice_proof;

pub use merge::slice_proof_multi;

pub use metadata::Difficulty;

pub use metadata::Priority;

pub use metadata::ProofMetadata;

pub use metadata::Strategy;

pub use mmap::MmapConfig;

pub use mmap::MmapProof;

pub use mmap::MmapProofStorage;

pub use normalize::canonicalize_conclusions;

pub use normalize::normalize_proof;

pub use parallel::ParallelCheckResult;

pub use parallel::ParallelConfig;

pub use parallel::ParallelProcessor;

pub use parallel::ParallelStatsComputer;

pub use pattern::LemmaPattern;

pub use pattern::PatternExtractor;

pub use pattern::PatternStructure;

pub use pcc::CodeLocation;

pub use pcc::PccBuilder;

pub use pcc::ProofCarryingCode;

pub use pcc::SafetyProperty;

pub use pcc::VerificationCondition;

pub use proof::Proof;

pub use proof::ProofNode;

pub use proof::ProofNodeId;

pub use proof::ProofStats;

pub use proof::ProofStep;

pub use rules::Clause;

pub use rules::CnfValidator;

pub use rules::Literal;

pub use rules::ResolutionValidator;

pub use rules::RuleValidation;

pub use rules::TheoryLemmaValidator;

pub use rules::UnitPropagationValidator;

pub use simplify::ProofSimplifier;

pub use simplify::SimplificationConfig;

pub use simplify::SimplificationStats;

pub use simplify::simplify_proof;

pub use stats::DetailedProofStats;

pub use stats::ProofQuality;

pub use stats::TheoryProofStats;

pub use streaming::ProofChunk;

pub use streaming::ProofChunkIterator;

pub use streaming::ProofStreamer;

pub use streaming::StreamConfig;

pub use streaming::StreamingProofBuilder;

pub use template::ProofTemplate;

pub use template::TemplateIdentifier;

pub use template::TemplateStep;

pub use theory::ArithProofRecorder;

pub use theory::ArrayProofRecorder;

pub use theory::EufProofRecorder;

pub use theory::ProofTerm;

pub use theory::TheoryProof;

pub use theory::TheoryProofProducer;

pub use theory::TheoryRule;

pub use theory::TheoryStep;

pub use theory::TheoryStepId;

pub use unsat_core::UnsatCore;

pub use unsat_core::extract_minimal_unsat_core;

pub use unsat_core::extract_unsat_core;

pub use unsat_core::get_core_labels;

pub use validation::FormatValidator;

pub use validation::ValidationError;

pub use validation::ValidationResult;

pub use visualization::ProofVisualizer;

pub use visualization::VisualizationFormat;

pub use craig::ArrayInterpolator;

pub use craig::CraigInterpolator;

pub use craig::EufInterpolator;

pub use craig::InterpolantColor;

pub use craig::InterpolantPartition;

pub use craig::InterpolantTerm;

pub use craig::InterpolationAlgorithm;

pub use craig::InterpolationConfig;

pub use craig::InterpolationError;

pub use craig::InterpolationStats;

pub use craig::LiaInterpolator;

pub use craig::SequenceInterpolator;

pub use craig::Symbol;

pub use craig::TheoryInterpolator;

pub use craig::TreeInterpolator;

pub use craig::TreeNode;

Modules

alethe

Alethe proof format for SMT proofs.

carcara

Carcara proof format compatibility.

checker

Proof checking infrastructure.

compress

Proof compression and optimization.

conversion

Format conversion utilities.

coq

Coq proof export

coq_enhanced

Enhanced Coq Proof Export with Complete Proof Terms.

craig

Craig Interpolation for SMT solving

diff

Proof diffing utilities for comparing two proofs.

drat

DRAT proof format for SAT proofs.

explanation

Natural language proof explanations and analysis.

fingerprint

Proof fingerprinting for fast similarity detection.

format

Unified proof format conversion API.

heuristic

Strategy heuristics learned from successful proofs.

incremental

Incremental proof construction.

interpolant

Interpolant extraction from proofs.

isabelle

Isabelle proof export

isabelle_enhanced

Enhanced Isabelle/HOL Proof Export with Complete Proof Terms.

lazy

Lazy proof evaluation for efficient proof processing.

lean

Lean proof export

lean_enhanced

Enhanced Lean 4 Proof Export with Complete Proof Terms.

lfsc

LFSC proof format (Logical Framework with Side Conditions).

logging

Proof step logging to persistent binary log files.

merge

Proof merging and slicing utilities.

metadata

Proof node metadata and annotations.

mmap

Memory-mapped proof storage for large proofs.

normalize

Proof normalization utilities for canonical representation.

parallel

Parallel proof checking and processing.

pattern

Lemma pattern extraction from proofs.

pcc

Proof-Carrying Code (PCC) generation

proof

Core proof representation.

replay

Proof log replay and offline verification.

rules

Proof rule definitions and validators.

sat_integration

Integration with oxiz-sat for DRAT proof generation

simplify

Proof simplification through logical rewriting.

stats

Advanced proof statistics and analysis.

streaming

Proof streaming for processing large proofs efficiently.

template

Proof template identification and reuse.

theory

Theory proof generation for SMT solvers.

traversal

Proof traversal and transformation utilities.

unsat_core

Unsat core extraction from proofs.

validation

Format validation utilities for proof formats.

visualization

Proof visualization utilities.