Enum Commands 

pub enum Commands {
    Explain {
        contract: PathBuf,
        format: String,
        binding: Option<PathBuf>,
    },
    Validate {
        contract: PathBuf,
    },
    CheckParity {
        contract: PathBuf,
    },
    Scaffold {
        contract: PathBuf,
        trait: bool,
        output: Option<PathBuf>,
    },
    ExtractPytorch {
        target: String,
        output: Option<PathBuf>,
    },
    Codegen {
        contract_dir: PathBuf,
        output: Option<PathBuf>,
    },
    Kani {
        contract: PathBuf,
    },
    Probar {
        contract: PathBuf,
        binding: Option<PathBuf>,
    },
    Status {
        contract: PathBuf,
    },
    Audit {
        contract: PathBuf,
        binding: Option<PathBuf>,
        coq: bool,
        flux: bool,
    },
    Diff {
        old: PathBuf,
        new: PathBuf,
    },
    Coverage {
        contract_dir: PathBuf,
        binding: Option<PathBuf>,
        fuzz: bool,
        reverse: Option<PathBuf>,
        enforcement: Option<PathBuf>,
    },
    Generate {
        contract: PathBuf,
        output: PathBuf,
        binding: Option<PathBuf>,
        readme: bool,
        ci: bool,
    },
    Graph {
        contract_dir: PathBuf,
        format: String,
    },
    Equations {
        contract: PathBuf,
        format: String,
    },
    Lean {
        contract: PathBuf,
        output_dir: Option<PathBuf>,
    },
    LeanStatus {
        path: PathBuf,
    },
    ProofStatus {
        path: PathBuf,
        binding: Option<PathBuf>,
        verify_bindings: Option<PathBuf>,
        format: String,
        table: bool,
        kind: Option<String>,
    },
    Lint {

        contract_dir: PathBuf,
        min_score: f64,
        binding: Option<PathBuf>,
        format: Option<String>,
        severity: Option<String>,
        strict: bool,
        suppress: Option<String>,
        suppress_rule: Option<String>,
        suppress_file: Option<String>,
        rule: Vec<String>,
        config: Option<PathBuf>,
        diff_ref: Option<String>,
        trend: bool,
        show_trend: bool,
        no_cache: bool,
        cache_stats: bool,
        suggest: bool,
        baseline: Option<PathBuf>,
        fix: bool,
        watch: bool,
        coverage: bool,
        min_coverage: Option<f64>,
        crate_dir: Option<PathBuf>,
        min_level: Option<String>,
        explain: Option<String>,
        strict_test_binding: bool,
    
},
    Score {
        path: PathBuf,
        binding: Option<PathBuf>,
        format: String,
        min_score: Option<f64>,
        summary: bool,
        top_gaps: usize,
        weights: Option<String>,
        exit_code: bool,
        pvscore: bool,
    },
    Query(QueryArgs),
    Invariants {
        contract: PathBuf,
    },
    Coq {
        contract: PathBuf,
    },
    Fuzz {
        contract: PathBuf,
    },
    Mirai {
        contract: PathBuf,
    },
    Flux {
        contract: PathBuf,
    },
    Tla {
        contract_dir: PathBuf,
    },
    Book {
        contract_dir: PathBuf,
        output: PathBuf,
        update_summary: bool,
        summary_path: Option<PathBuf>,
    },
    Infer {
        crate_dir: PathBuf,
        binding: PathBuf,
        contract_dir: PathBuf,
        top: usize,
    },
    Unlock {
        contract: PathBuf,
        reason: String,
    },
    Roofline {
        contract_dir: PathBuf,
        params: u64,
        bits: u32,
        hardware: String,
        format: String,
    },
    Pipeline {
        pipeline: PathBuf,
        format: String,
    },
    Kaizen {
        contract_dir: PathBuf,
        src_root: Option<PathBuf>,
        repo: Option<String>,
        dry_run: bool,
        codegen: bool,
        fix: bool,
        json: bool,
        min_score: Option<f64>,
    },
    Certify {
        contract_dir: PathBuf,
        config: Option<PathBuf>,
        output: Option<PathBuf>,
    },
    VerifyStructure {
        contract_dir: PathBuf,
        config: Option<PathBuf>,
        model: Option<PathBuf>,
    },
    VerifyPipeline {
        contract_dir: PathBuf,
        format: String,
    },
    VerifyBindings {
        binding: PathBuf,
        output: Option<PathBuf>,
        crate_name: Option<String>,
    },
    Migrate {
        contract_dir: PathBuf,
        dry_run: bool,
    },
}

Available subcommands for the pv CLI

Variants

Explain

Explain a contract in detail

Fields

contract: PathBuf

format: String

binding: Option<PathBuf>

Validate

Validate a YAML kernel contract

Fields

contract: PathBuf

CheckParity

Execute cross_check_command per row of a parity-matrix contract (SEMANTIC gate)

Fields

contract: PathBuf

Scaffold

Generate Rust trait + test scaffolding from a contract

Fields

contract: PathBuf

trait: bool

output: Option<PathBuf>

ExtractPytorch

Extract kernel equations from PyTorch source into YAML

Fields

target: String

output: Option<PathBuf>

Codegen

Generate Rust debug_assert!() from YAML contracts

Fields

contract_dir: PathBuf

output: Option<PathBuf>

Output Rust file path

Kani

Generate Kani proof harnesses from a contract

Fields

contract: PathBuf

Probar

Generate probar property tests from a contract

Fields

contract: PathBuf

binding: Option<PathBuf>

Path to binding registry YAML (generates wired tests)

Status

Show contract status (equations, obligations, coverage)

Fields

contract: PathBuf

Path to the contract YAML file

Audit

Run traceability audit on a contract

Fields

contract: PathBuf

Path to the contract YAML file

binding: Option<PathBuf>

Path to binding registry YAML (adds binding audit)

coq: bool

Show Coq proof tier per obligation

flux: bool

Show Flux shape coverage per obligation

Diff

Diff two contract versions and suggest semver bump

Fields

old: PathBuf

Path to the old contract YAML file

new: PathBuf

Path to the new contract YAML file

Coverage

Show cross-contract obligation coverage report

Fields

contract_dir: PathBuf

Directory containing contract YAML files

binding: Option<PathBuf>

Path to binding registry YAML (adds binding coverage)

fuzz: bool

Include fuzz coverage data

reverse: Option<PathBuf>

Reverse coverage: scan crate dir for unbound pub fns

enforcement: Option<PathBuf>

Enforcement quality: scan crate source for contract call sites and classify E0/E1/E2

Generate

Generate all artifacts (scaffold, kani, probar) to disk

Fields

contract: PathBuf

Path to the contract YAML file

output: PathBuf

Output directory for generated files

binding: Option<PathBuf>

Path to binding registry YAML (generates wired tests)

readme: bool

Generate CONTRACT-README.md (requires –binding)

ci: bool

Generate .github/workflows/contracts.yml

Graph

Show contract dependency graph

Fields

contract_dir: PathBuf

Directory containing contract YAML files

format: String

Output format: text (default), dot, json, or mermaid

Equations

Display equations from a contract

Fields

contract: PathBuf

format: String

Lean

Generate Lean 4 definitions and theorem stubs

Fields

contract: PathBuf

output_dir: Option<PathBuf>

LeanStatus

Report Lean 4 proof status across contracts

Fields

path: PathBuf

Path to a contract YAML file or directory of contracts

ProofStatus

Report hierarchical proof levels (L1–L5) across contracts

Fields

path: PathBuf

Path to a contract YAML file or directory of contracts

binding: Option<PathBuf>

Path to binding registry YAML (adds binding coverage)

verify_bindings: Option<PathBuf>

L5 gate: before counting a binding as implemented, verify its function actually exists in source (scanned from the given root, default .). Phantom “implemented” bindings are downgraded, so L5 means “verified as implemented”, not self-declared.

format: String

Output format: text (default) or json

table: bool

Show per-obligation verification table

kind: Option<String>

Filter: kernel|registry|model-family|pattern|schema

Lint

Run all contract quality gates (validate + audit + score)

Fields

contract_dir: PathBuf

Directory containing contract YAML files

min_score: f64

Minimum composite score threshold (default: 0.0 = no score gate)

binding: Option<PathBuf>

Path to binding registry YAML

format: Option<String>

Output format: text (default), json, sarif, github

severity: Option<String>

Minimum severity to report: error, warning, info

strict: bool

Promote warnings to errors

suppress: Option<String>

Suppress specific finding IDs (comma-separated)

suppress_rule: Option<String>

Suppress all findings for a rule (comma-separated)

suppress_file: Option<String>

Suppress all findings matching a file path (comma-separated)

rule: Vec<String>

Override rule severity (e.g. PV-AUD-001=info)

config: Option<PathBuf>

Path to .pv.toml config file

diff_ref: Option<String>

Only lint contracts changed since base ref (e.g. main, HEAD~5)

trend: bool

Record quality trend snapshot

show_trend: bool

Show quality trend history

no_cache: bool

Bypass lint cache

cache_stats: bool

Show cache hit/miss statistics

suggest: bool

Show auto-fix suggestions (dry run)

baseline: Option<PathBuf>

Suppress findings in baseline SARIF file

fix: bool

Apply deterministic auto-fixes

watch: bool

Re-lint on file change (polling)

coverage: bool

Show aggregate contract coverage metric

min_coverage: Option<f64>

Minimum coverage percentage (exit 1 if below)

crate_dir: Option<PathBuf>

Path to crate directory for reverse coverage gate

min_level: Option<String>

Minimum enforcement level: basic, standard, strict, proven

explain: Option<String>

Explain a lint rule in detail (e.g. PV-ENF-001)

strict_test_binding: bool

Enable strict test-binding gate (PV-VER-002): cross-checks every falsification_tests[].test cargo invocation against #[test] fns in the source tree. Catches drift classes that PV-VER-001 misses (suffix drift, module-path drift, convention drift, “or equivalent” placeholders). Default emits Warning; combine with --strict to promote to Error and fail CI. Issue #1510.

Score

Score contracts or a codebase directory

Fields

path: PathBuf

Path to a contract YAML file or directory of contracts

binding: Option<PathBuf>

Path to binding registry YAML

format: String

Output format: text (default) or json

min_score: Option<f64>

Minimum score threshold (exit 1 if below)

summary: bool

Show aggregate summary only (no per-contract detail)

top_gaps: usize

Show top N gaps by impact (default: 5)

weights: Option<String>

Custom weights as JSON

exit_code: bool

Exit with status 1 if any contract below –min-score

pvscore: bool

Show 10-dimension PVScore (geometric mean)

Query(QueryArgs)

Search contracts by intent, regex, or literal match

Invariants

Generate type invariant trait + Kani preservation harnesses

Fields

contract: PathBuf

Coq

Generate Coq theorem stubs from a contract

Fields

contract: PathBuf

Fuzz

Generate libfuzzer fuzz targets from a contract

Fields

contract: PathBuf

Mirai

Generate MIRAI annotations from a contract

Fields

contract: PathBuf

Flux

Generate Flux refinement types from a contract

Fields

contract: PathBuf

Tla

Generate TLA+ specification from contract dependency DAG

Fields

contract_dir: PathBuf

Directory containing contract YAML files

Book

Generate mdBook pages for contracts

Fields

contract_dir: PathBuf

Directory containing contract YAML files

output: PathBuf

Output directory for generated pages

update_summary: bool

Also update book/src/SUMMARY.md with contract links

summary_path: Option<PathBuf>

Path to SUMMARY.md (default: book/src/SUMMARY.md)

Infer

Infer contracts and bindings for unbound functions in a crate

Fields

crate_dir: PathBuf

Path to the crate directory to scan

binding: PathBuf

Path to binding registry YAML

contract_dir: PathBuf

Directory containing contract YAML files

top: usize

Maximum number of suggestions to show

Unlock

Remove enforcement level lock from a contract (requires –reason)

Fields

contract: PathBuf

Path to the contract YAML file

reason: String

Mandatory reason for unlocking (audit trail)

Roofline

Compute roofline ceilings from contract equations

Fields

contract_dir: PathBuf

params: u64

Total model parameters (e.g. 7000000000 for 7B)

bits: u32

Bits per weight (2, 4, 8, 16, 32)

hardware: String

Hardware profile: apple-m, a100

format: String

Output format: text (default) or json

Pipeline

Validate a pipeline contract (cross-repo verification)

Fields

pipeline: PathBuf

Path to the pipeline YAML file

format: String

Output format: text (default) or json

Kaizen

Fleet-wide contract enforcement (kaizen loop)

Fields

contract_dir: PathBuf

src_root: Option<PathBuf>

repo: Option<String>

dry_run: bool

codegen: bool

fix: bool

json: bool

min_score: Option<f64>

Certify

Produce whole-model proof certificate (runs verify-pipeline + verify-structure)

Fields

contract_dir: PathBuf

config: Option<PathBuf>

output: Option<PathBuf>

VerifyStructure

Verify model architecture structure matches contracts

Fields

contract_dir: PathBuf

config: Option<PathBuf>

model: Option<PathBuf>

VerifyPipeline

Verify compositional shape flow across contract dependency graph

Fields

contract_dir: PathBuf

format: String

VerifyBindings

Generate a Rust test that verifies all bound functions exist

Fields

binding: PathBuf

Path to binding.yaml

output: Option<PathBuf>

Output file path (default: stdout)

crate_name: Option<String>

Crate name for test label

Migrate

Migrate old-format contract YAMLs to current schema (GH-67)

Fields

contract_dir: PathBuf

dry_run: bool

Trait Implementations

impl Clone for Commands

fn clone(&self) -> Commands

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Commands

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl FromArgMatches for Commands

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut<'b>( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl Subcommand for Commands

fn augment_subcommands<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate Self via FromArgMatches::from_arg_matches_mut

fn augment_subcommands_for_update<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate self via FromArgMatches::update_from_arg_matches_mut

fn has_subcommand(__clap_name: &str) -> bool

Test whether Self can parse a specific subcommand