zkmc — zero-knowledge model checking

Monorepo for the zkmc toolchain: proving termination of guarded-command programs and exporting the obligations as zero-knowledge proofs.

• encoder/ — Python toolkit (zkterm, zkrank, zkverify, zkfarkas, zkexplicit, zkltl, zksynth, zkits). Encodes guarded commands and ranking functions into matrix/vector form, discharges termination obligations via Farkas' lemma + Z3, and exports JSON consumable by the prover. Programs can be written as .gc guarded commands or imported from KoAT .koat integer transition systems (zkits); properties written directly as a Büchi automaton or in LTL (spec:, via Spot); ranking functions written by hand or synthesized automatically (zksynth / zkverify --synthesize). See encoder/README.md and encoder/LANGUAGE.md.
• zkmc-explicit/ — Rust implementation of explicit-case ZKP specified in ZKMC paper. Takes JSON as input, benchmarks time to setup, prove, and verify - see zkmc-explicit/README.md for installation and usage instructions.
• zkmc-symbolic/ — Rust implementation of symbolic-case ZKP specified in ZKMC paper. Takes JSON as input, benchmarks time to setup, prove, and verify - see zkmc-symbolic/README.md for installation and usage instructions.

Academic implementation, not production ready.

MIT