Issues

• Editor performance on large acquisition verdicts (dalek-lite field_u64.rs)

  enhancementvscode-extension
  ilyasergey/vermilion#58 · Filter by author ilyasergey opened on Aug 20, 2026

• Work alongside an enabled rust-analyzer

  featurevscode-extension
  ilyasergey/vermilion#57 · Filter by author ilyasergey opened on Aug 20, 2026

• Bit-vector assert obligations collide on their emitted declaration name

  bugvcgen
  ilyasergey/vermilion#56 · Filter by author ilyasergey opened on Aug 20, 2026

• Learn proof automation from the accumulated interactive twin proofs

  feature
  ilyasergey/vermilion#55 · Filter by author ilyasergey opened on Aug 20, 2026

• Share substituted values in the lowering instead of duplicating them

  bugvcgen
  ilyasergey/vermilion#53 · Filter by author ilyasergey opened on Aug 20, 2026

• Ladder rung for Seq extensionality (elementwise ⇒ whole equality)

  enhancement
  ilyasergey/vermilion#52 · Filter by author ilyasergey opened on Aug 20, 2026

• Vermilion as a standalone tool (reproduce proofs outside this repo)

  feature
  ilyasergey/vermilion#50 · Filter by author ilyasergey opened on Aug 20, 2026

• Carry decreases measures for cross-module recursive spec fns

  featurevcgenverus
  ilyasergey/vermilion#49 · Filter by author ilyasergey opened on Aug 20, 2026

• Bool-parameter conditionals emit unprovable Decidable evidence

  bugvcgen
  ilyasergey/vermilion#48 · Filter by author ilyasergey opened on Aug 20, 2026

• Per-function checking performance follow-ups

  enhancementvcgen
  ilyasergey/vermilion#42 · Filter by author ilyasergey opened on Aug 20, 2026

• Upgrade to Lean 4.32 and remove the Veil dependency

  enhancementfeature
  ilyasergey/vermilion#41 · Filter by author ilyasergey opened on Aug 20, 2026

• Use Aeneas as a certified solver backend for specific programs

  featurefoundations
  ilyasergey/vermilion#40 · Filter by author ilyasergey opened on Aug 20, 2026

• Share obligation contexts and name result values in emitted twins

  featurevcgen
  ilyasergey/vermilion#39 · Filter by author ilyasergey opened on Aug 20, 2026

• Support iterator for loops via ghost-iterator contracts

  featurevcgenverus
  ilyasergey/vermilion#38 · Filter by author ilyasergey opened on Aug 20, 2026

• Interactively-proven highlight shown even when the backend twin proof fails

  bugvscode-extension
  ilyasergey/vermilion#36 · Filter by author ilyasergey opened on Aug 20, 2026

• Bits bridge lemmas and a wrap-collapse rung for constant-time arithmetic

  feature
  ilyasergey/vermilion#35 · Filter by author ilyasergey opened on Aug 20, 2026

• Hoist canonical core datatype models into the Lean prelude

  featurevcgen
  ilyasergey/vermilion#33 · Filter by author ilyasergey opened on Aug 20, 2026

• Support the standard HashMap entry API

  featurevcgen
  ilyasergey/vermilion#30 · Filter by author ilyasergey opened on Aug 20, 2026

• Give statics and atomic ghost protocols a Lean semantics

  featurefoundationsvcgen
  ilyasergey/vermilion#27 · Filter by author ilyasergey opened on Aug 20, 2026

• Go to Lean shortcut fails for bounded_arithmetic.rs

  bugvscode-extension
  ilyasergey/vermilion#26 · Filter by author ilyasergey opened on Aug 20, 2026

• Verification shortcut should no-op without a verus macro

  bugvscode-extension
  ilyasergey/vermilion#24 · Filter by author ilyasergey opened on Aug 20, 2026

• Support std Ord min and max default-body contracts

  featurevcgen
  ilyasergey/vermilion#23 · Filter by author ilyasergey opened on Aug 20, 2026

• Support unary BitNot on machine integers

  featurevcgen
  ilyasergey/vermilion#21 · Filter by author ilyasergey opened on Aug 20, 2026

• Fast-fail Rust highlighting when the twin proof fails to type-check

  bugvscode-extension
  ilyasergey/vermilion#15 · Filter by author ilyasergey opened on Aug 20, 2026

• Per-case-study test and runnable harness with output

  enhancement
  ilyasergey/vermilion#12 · Filter by author ilyasergey opened on Aug 20, 2026