Seven soundness bugs hide in ZK DSL toolchains, and Liezz finds them by splicing witnesses from different runs.

Verifpal 1.3 adds peer scenarios for differing counterparty assumptions across runs, plus result envelopes and solver tweaks.