Usage

python3 -m lambda_pmc [options] INPUT

If INPUT is omitted, VMT, MCMT and IC3PO input is read from standard input. The result is one of safe, unsafe or unknown; python3 -m lambda_pmc --help lists all options.

Choosing a mode

`--algo`	What it does	Use it when
`bounded-induction` (default)	Generalizes the proofs of finite instances into quantified lemmas, and checks them with Z3 or MathSAT	a good first choice for general models
`parameter-abstraction`	Same loop; the check for all sizes is done by ic3ia on a quantifier-free abstraction	the model is in the supported fragment (universal init, property and axioms, `∃∀` transitions)
`updria`	Universal PDR with implicit predicate abstraction (requires Z3)	you want invariants built by a property-directed search
`bmc`	Bounded counterexample search	debugging a model, looking for bugs

Main options

Options that are on by default are disabled with their --no- form, for example --no-use-symmetries.

Option	Default	Effect
`-l, --input-language`	`vmt`	`vmt`, `mcmt`, `mypyvy` or `ic3po`
`--show-witness`	off	print the counterexample, or the invariant of a successful proof
`--verbosity {0,1,2}`	1	0: only the verdict; 1: compact progress; 2: solver activity and the parsed options
`--stats`	off	print run statistics: a progress line while the algorithm runs and a summary at the end
`--qfinvmin`	on	minimize the generalized invariant before the inductiveness check
`--use-symmetries`	on	exploit the index symmetry of the ground instances
`--houdini`	on	keep the largest inductive subset of a non-inductive candidate (Z3 only)
`--qa-invariants`	off	also infer lemmas with quantifier alternation from the finite proofs
`--repair`	off	requantify lemmas falsified by a larger instance, possibly with existential quantifiers
`--solver mathsat`	`z3`	check inductiveness with a quantifier-instantiation procedure over MathSAT
`--initial-concretization [N]`	off	UPDRIA: seed the search with lemmas generalized from a finite instance
`--starting-card SORT=N`	heuristic	first cardinality of a sort explored by the finite search
`--card SORT=N`, `--verify-concretization`		model check only the finite instance with the given cardinalities

Z3 parameters are passed with --z3-<name> (for example --z3-mbqi), and selected ic3ia settings with --ic3ia-<name> (for example --ic3ia-inv-reduce).

Input formats

VMT is the canonical format; the Input language page describes the profile Lambda reads. MCMT is read natively. mypyvy models are read through a fork with a VMT printer (set MYPYVY_DIR), and Ivy protocols through Ivy's convert_to_mypyvy followed by that printer. The standalone converters ivy2vmt, mypyvy2vmt, ic3po2vmt and vmt2veil are in lambda_pmc/translators/, together with mypyvy2ic3po and ivy2duoai, which produce inputs for IC3PO and DuoAI.

Certificates

python3 -m lambda_pmc --algo bounded-induction -l vmt \
  --dump-proof-check proof --dump-veil proof.lean model.vmt

--dump-proof-check PREFIX writes SMT-LIB obligations: the negations of Init ⇒ Inv, Inv ∧ T ⇒ Inv′ and Inv ⇒ P. Every check-sat must return unsat. Layouts: single (default), three, or split (one file per obligation). For cvc5, use cvc5 --incremental FILE.smt2.
--dump-veil FILE writes a Veil module to be checked in Lean. With --veil-proofs trust (default) Veil trusts cvc5; with --veil-proofs reconstruct the proofs are checked by the Lean kernel. Systems with real-valued symbols are not supported by this exporter; use SMT-LIB for those.

The modules target Veil v4.28.0 (Lean 4.28.0). Build Veil with lake exe cache get and lake build +Veil, then check a module from the Veil directory with lake lean FILE.lean (not lake env lean). A module is verified when the output has one ✅ per obligation and no ❌; do not rely on the exit code. The README.md of the distribution has the details.