Issues

• #gen_spec reports procedure assertions as errors as soon as an invariant exists, before any verification command

  verse-lab/veil#124 · Filter by author ilyasergey opened on Oct 15, 2026

• sat trace with any 4 actions exceeds simp's step limit on a moderate model

  verse-lab/veil#123 · Filter by author ilyasergey opened on Oct 15, 2026

• #time #model_check reports only the synchronous part of the command

  verse-lab/veil#122 · Filter by author ilyasergey opened on Oct 15, 2026

• instantiate of a non-public class in a module file: misleading 'Unknown identifier' error

  verse-lab/veil#121 · Filter by author ilyasergey opened on Oct 15, 2026

• immutable function / param of type Nat → Nat: #check_invariants refutes a preserved invariant with an empty counterexample

  verse-lab/veil#120 · Filter by author ilyasergey opened on Oct 15, 2026

• Nat-quantified assumptions cannot be model-checked (no Decidable instance), even with assumptions_hold_by

  verse-lab/veil#119 · Filter by author ilyasergey opened on Oct 15, 2026

• max on Nat in an action breaks symbolic traces and the SMT encoding

  verse-lab/veil#118 · Filter by author ilyasergey opened on Oct 15, 2026

• set_option … in #model_check does not parse after a sat/unsat trace

  verse-lab/veil#117 · Filter by author ilyasergey opened on Oct 15, 2026

• #model_check handsoff mode can stall between compilation finishing and the compiled binary starting

  bug
  Bug

  verse-lab/veil#64 · Filter by author zqy1018 opened on Sep 13, 2026

• Liveness Proofs in Veil

  verse-lab/veil#30 · Filter by author agostbiro opened on Sep 6, 2026
  2

• With veil.smt.trust false, a transition's obligation errors (failed to synthesize Nonempty node) and the #check_invariants text output still prints ✅ for it

  verse-lab/veil#26 · Filter by author Deicyde opened on Sep 2, 2026

• veil_let x := v; y := x mis-parses — doReassign consumes veil_let x := v; y as an assignment LHS, the exact input DoNotation.lean's NOTE guards against

  verse-lab/veil#23 · Filter by author Deicyde opened on Aug 29, 2026
  2

• A bare import Veil reserves 12 identifiers globally (assert, require, sat, …) — scoped keyword declarations are defeated by unscoped rules that reference them

  verse-lab/veil#24 · Filter by author Deicyde opened on Aug 29, 2026
  1

• transition weakening theorem fails when a module's state is only Boolean individuals — fixed tactic script assumes convert h leaves a goal

  verse-lab/veil#22 · Filter by author Deicyde opened on Aug 29, 2026
  1

• VCManager HashMap nonlinearity

  verse-lab/veil#7 · Filter by author hargoniX opened on Apr 23, 2026
  2

• feature: add support for symbolic simulation

  enhancement
  Feature

  verse-lab/veil#46 · Filter by author dranov opened on Apr 16, 2026

• feature: use the explicit state model checker to find CTIs on finite instances

  enhancement
  Feature

  verse-lab/veil#47 · Filter by author dranov opened on Mar 20, 2026

• bug: inference of Decidable is very syntactic, so it sometimes fails

  bug
  Bug

  verse-lab/veil#48 · Filter by author dranov opened on Mar 19, 2026
  1

• feature: integrate with querysmt

  enhancement
  Feature

  verse-lab/veil#49 · Filter by author dranov opened on Feb 25, 2026

• feature: show nicer InfoView when cursor is inside definitions

  Feature

  verse-lab/veil#50 · Filter by author dranov opened on Feb 23, 2026
  1

• task: investigate integrating with definitions in CSLib

  Task

  verse-lab/veil#57 · Filter by author dranov opened on Feb 23, 2026

• task: allow require/assume to introduce hypothesis into local context

  Task

  verse-lab/veil#51 · Filter by author zqy1018 opened on Feb 14, 2026
  

• feature: sat trace queries for concrete state model checker

  enhancement
  Feature

  verse-lab/veil#52 · Filter by author dranov opened on Feb 2, 2026
  2

• feature: add representation for state

  Feature

  verse-lab/veil#53 · Filter by author zqy1018 opened on Feb 1, 2026
  1

• task: optimise allValues definitions in Veil.Enumeration instances

  Task

  verse-lab/veil#55 · Filter by author dranov opened on Jan 28, 2026