Module certificate 

Self-Certifying Proof Certificates

Generate proof certificates that can be independently verified without trusting LogicAffeine’s implementation.

Each certificate binds its proof steps to the claim via a cryptographic-style digest chain. Tampering with the claim, conclusion, or formulas is detected by verify_certificate().

Structs

ProofCertificate

A self-certifying proof certificate.

ProofStep

A single step in the proof.

Enums

VerifyClaim

What is being proven.

Functions

digest_formula

Compute a deterministic digest of a VerifyExpr for tamper detection.

generate_equivalence_certificate

Generate a proof certificate for an equivalence result.

generate_safety_certificate

Generate a proof certificate for a safety result.

verify_certificate

Verify a proof certificate (check that steps are internally consistent).