Issues

• #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

• task: add Nodup assumption to Veil.Enumeration

  good first issue
  Task

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

• feature: display non-deterministic choices made in the action in trace display

  enhancement
  Feature

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

• feature: incremental verification and caching

  enhancement
  Feature

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

• feature: model checker should enumerate all theories

  bugenhancement
  Feature

  verse-lab/veil#38 · Filter by author dranov opened on Jan 14, 2026
  1

• feature: interactive state space exploration

  enhancement
  Feature

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

• bug: unnecessary enumeration of fields in executing transitions

  Bug

  verse-lab/veil#58 · Filter by author zqy1018 opened on Jan 8, 2026
  1

• feature: allow hooking custom visualisations into Veil

  enhancement
  Feature

  verse-lab/veil#39 · Filter by author dranov opened on Dec 18, 2025
  1

• Automatic discovery of efficient execution patterns for non-determinism

  verse-lab/veil#54 · Filter by author dranov opened on Dec 18, 2025