with one click
certify
// Generate and verify Mumei proof certificates with mumei verify --proof-cert and mumei verify-cert.
// Generate and verify Mumei proof certificates with mumei verify --proof-cert and mumei verify-cert.
[HINT] Download the complete skill directory including SKILL.md and all related files
| name | certify |
| description | Generate and verify Mumei proof certificates with mumei verify --proof-cert and mumei verify-cert. |
Given .mm source whose verification succeeds, produce a proof certificate and re-check it against the current source.
Action:
Run mumei verify --proof-cert, optionally with an explicit output path.
Expectation:
Verification succeeds and writes a .proof.json certificate containing atom proof metadata.
Result: If certificate generation succeeds, proceed to Step 2. If verification fails, run diagnose.
mumei verify input.mm --proof-cert --output input.proof.json
With cargo from the compiler checkout:
LLVM_SYS_170_PREFIX=/usr/lib/llvm-17 cargo run -- verify input.mm --proof-cert --output input.proof.json
Action:
Parse the generated .proof.json and confirm it includes module metadata, atom entries, content/proof hashes, dependencies/effects, and Z3 result fields.
Expectation: The certificate is valid JSON and every atom entry reflects the just-verified source.
Result: If the structure is valid, proceed to Step 3.
python -m json.tool input.proof.json >/dev/null
Action:
Run mumei verify-cert against the certificate and source file.
Expectation: The command reports that the certificate matches current source hashes and proof status.
Result: Report certificate validity. If atoms changed, regenerate the certificate.
mumei verify-cert input.proof.json input.mm
When accepting Lean-backed imported certificates:
mumei verify-cert input.proof.json input.mm --allow-lean-verified
| Parameter | Type | Required | Default | Description |
|---|---|---|---|---|
| source_file | path | yes | .mm source file | |
| cert_file | path | no | <source>.proof.json | Output/input certificate path |
| allow_lean_verified | flag | no | off | Accept z3_check_result = "lean_verified" |