Crate provable_contracts 

provable-contracts

Papers to Math to Contracts in Code.

A Rust library for converting peer-reviewed research papers into mathematically provable kernel implementations via YAML contract intermediaries with Kani bounded model checking verification.

Modules

• schema — Parse and validate YAML kernel contracts
• scaffold — Generate Rust trait stubs + failing tests from contracts
• [kani] — Generate #[kani::proof] harnesses from contracts
• [probar] — Generate probar property-based tests from contracts
• audit — Trace paper→equation→contract→test→proof chain
• binding — Map contract equations to implementation functions
• diff — Detect drift between contract versions
• coverage — Cross-contract obligation coverage report
• generate — End-to-end codegen to disk
• graph — Contract dependency graph and cycle detection
• latex — LaTeX conversion for contract math notation
• book_gen — mdBook page generation for contracts
• lean_gen — Lean 4 definition and theorem stub generation
• lint — Contract quality gate: validate + audit + score in one pass
• kernels — Scalar, AVX2, and PTX kernel implementations

Modules

audit

Audit trail generator — traceability chain.

binding

Binding registry — maps contract equations to implementations.

book_gen

mdBook page generation for contracts.

build_helper

Build script helper for consuming crates.

codegen

Code generation from YAML contracts → Rust debug_assert!() checks.

coq_gen

Coq theorem stub generation from YAML contracts.

coverage

Cross-contract obligation coverage report.

diff

Contract diff — detect drift between contract versions.

error

explain

Contract explanation — chain-of-thought narrative for any contract.

extract

PyTorch kernel extraction — reads Python source, extracts equations.

flux_gen

Flux refinement type annotation generation.

fuzz_gen

Coverage-guided fuzz target generation.

generate

End-to-end codegen — generates all artifacts to disk.

graph

Contract dependency graph — composition via depends_on.

infer

Contract inference engine.

invariant_gen

Type invariant code generation.

kani_gen

Kani harness generator — Phase 6 of the pipeline.

kernels

Kernel implementations: scalar reference, AVX2 SIMD, and CUDA PTX.

latex

LaTeX conversion utilities for contract math notation.

lean_gen

Lean 4 code generator — Phase 7 of the pipeline.

lint

Contract quality gate: validate + audit + score in one pass.

mirai_gen

MIRAI abstract interpretation annotation generation.

obligation_matrix

Per-obligation verification matrix.

pipeline

Pipeline contract support — cross-repo compositional verification.

probar_gen

Probar property-test generator — Phase 5 of the pipeline.

proof_status

Proof status report — cross-contract proof level assessment.

query

Contract query engine with BM25 semantic search.

readme_gen

Deterministic README.md and CI workflow generation for consumer projects.

reverse_coverage

Reverse coverage: detect public functions without contract bindings.

roofline

Runtime roofline model derived from contract YAML.

scaffold

Scaffold generator — Phase 3 of the pipeline.

schema

scoring

Contract and codebase scoring.

tla_gen

TLA+ system-level model checking specification generation.

traits

Auto-generated contract traits for compiler-enforced binding verification.