AeneasVerif

Các issue có thể đã có người làm được xếp cuối danh sách. Sắp xếp tất cả theo ngày

• Bug: `Unreachable` on `&mut` to an opaque type with a mutable region

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1473 · Mở ngày 22/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Uncaught `Invalid_argument "Can't get the list of fields of this adt"` when code builds a variant of an opaque enum

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 55/100

  AeneasVerif/aeneas#1463 · Mở ngày 16/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: `There should be no bottoms in the value` on `if true { panic!() }`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 42/100

  AeneasVerif/aeneas#1462 · Mở ngày 16/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Internal error in `simplify_loop_output_conts` when code after a loop reads one field of a tuple loop variable

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 22/100

  AeneasVerif/aeneas#1459 · Mở ngày 16/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Lean backend: references to crate-level items lose the crate prefix and can resolve to a same-named definition in a module

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1458 · Mở ngày 16/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Missing backwards function in Lean backend with iterators

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 22/100

  AeneasVerif/aeneas#1437 · Mở ngày 14/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Uncaught exception: `CFailure`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1435 · 1 bình luận · Mở ngày 13/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Model for `core::num::NonZero`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 18/100

  AeneasVerif/aeneas#1418 · Mở ngày 12/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Lean backend emits namespace references captured by structure fields and local binders

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1411 · 1 bình luận · Mở ngày 9/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: user `Drop` impls never run, so a destructor's effect is silently lost

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 15/100

  AeneasVerif/aeneas#1410 · Mở ngày 9/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: `<[T]>::contains` model calls `eq(needle, element)`, but core calls `eq(element, needle)`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 72/100

  AeneasVerif/aeneas#1409 · Mở ngày 9/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: elabDoMatch: duplicate binder

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1406 · Mở ngày 8/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Support typed copies

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  enhancement

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 12/100

  AeneasVerif/aeneas#1405 · 1 bình luận · Mở ngày 8/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Internal error in `InterpMatchCtxs` when joining loop contexts over non-opaque wrapper holding borrow

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 22/100

  AeneasVerif/aeneas#1399 · Mở ngày 5/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: `[CONST; N]` repeat of a non-`Copy` type

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1450 · 5 bình luận · Mở ngày 5/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: fieldless enum variant written into an array is translated as `()` when a later loop borrows the array

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1395 · Mở ngày 3/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Feature request: Translate inline asm using Kraken

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1396 · 3 bình luận · Mở ngày 3/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Isabelle/HOL backend: contribution proposal

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 8/100

  AeneasVerif/aeneas#1389 · Mở ngày 1/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Formulate specs for unsigned integers in terms of `Int` instead of `Nat`?

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 18/100

  AeneasVerif/aeneas#1387 · Mở ngày 1/10/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: uncaught `CFailure` in `PrePasses.update_array_default` when an impl's trait is removed by Charon's `--exclude`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1375 · Mở ngày 27/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: `vec![x]` requires an unused external type `core::mem::maybe_uninit::MaybeUninit`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1370 · Mở ngày 26/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: internal error at `InterpReduceCollapse.ml:1137` on `if let Some(x) = slice.get(i)` inside a loop

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1369 · Mở ngày 26/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: internal error at `InterpMatchCtxs.ml:230` when joining contexts that hold a struct of borrowed slices

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1368 · Mở ngày 26/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: no `partial_fixpoint` monotonicity lemma for `loop`, so recursion through a loop does not elaborate

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 1-2 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1367 · Mở ngày 26/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: `@[discriminant]` instances are declared in the root namespace and clash across extractions

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 3/5 Nửa ngày Mức phù hợp với người mới 62/100

  AeneasVerif/aeneas#1366 · 1 bình luận · Mở ngày 26/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: error when matching contexts

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 15/100

  AeneasVerif/aeneas#1349 · Mở ngày 16/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Lean backend: type-decl holding a `Box<dyn Iterator>` field is refused with "Dynamic trait types are not supported yet" — minimal repro (charon translates it fine)

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1343 · Mở ngày 10/9/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Docs: Documentation still recommends deprecated `#setup_aeneas_simps`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 78/100

  AeneasVerif/aeneas#1324 · Mở ngày 30/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Nested items within anonymous const items (const `_`) generate invalid Lean identifiers

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1323 · 1 reaction · Mở ngày 30/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Internal error (Interp.ml:609) on `<[T]>::get` inside a loop

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 34/100

  AeneasVerif/aeneas#1319 · Mở ngày 28/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Improve documentation (discoverability?) for beginners

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 35/100

  AeneasVerif/aeneas#1295 · 5 reaction · Mở ngày 24/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Could not match the contexts` on a loop

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 18/100

  AeneasVerif/aeneas#1282 · Mở ngày 21/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: A generic struct whose field mentions one instantiation of itself produces an invalid `mutual inductive`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1281 · Mở ngày 21/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Comparisons are emitted as Prop

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1279 · Mở ngày 21/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: `IScalar.rem` is falsely modeled as non-panicking for MIN % (-1)

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 55/100

  AeneasVerif/aeneas#1275 · Mở ngày 20/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Closure returning reference argument fails with non-endable abstraction

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 18/100

  AeneasVerif/aeneas#1266 · Mở ngày 15/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Feature request: `async`

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  enhancement

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 12/100

  AeneasVerif/aeneas#1265 · Mở ngày 15/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Feature request: Add support for mutually recursive functions and trait implementations

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  enhancement

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 15/100

  AeneasVerif/aeneas#1264 · 1 bình luận · Mở ngày 15/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Matching an indexed `enum` value fails during expansion

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1253 · 1 bình luận · Mở ngày 11/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Distinct lifetimes in `Option<&T>::as_ref()` trigger internal error

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 22/100

  AeneasVerif/aeneas#1252 · Mở ngày 11/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: ` u8 as char` fails to translate

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 3/5 Nửa ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1251 · Mở ngày 10/8/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Lean backend emits a `sorry`-named structure with error-hole fields for the dyn-compatible trait `digest::DynDigest` instead of failing cleanly

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 42/100

  AeneasVerif/aeneas#1243 · Mở ngày 31/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Items depending on a failed-to-translate derived impl are still emitted, producing ill-typed Lean with dangling identifiers and inline `sorry /- ERROR: ... -/` bodies

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 30/100

  AeneasVerif/aeneas#1242 · 1 bình luận · Mở ngày 31/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Uncaught `Not_found` in `extract_function_call` (Extract.ml) when a called trait method's declaration is missing — partially written output files are left on disk

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 40/100

  AeneasVerif/aeneas#1241 · 1 bình luận · Mở ngày 31/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Uncaught `Not_found` in `ty_has_mut_borrow_for_region_in_pred` (TypesUtils.ml) when translating functions generic over a large trait-clause web with outlives predicates (arkworks `Pairing`)

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 32/100

  AeneasVerif/aeneas#1239 · 1 bình luận · Mở ngày 31/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: Nested borrows: selecting a `&'static [u8]` constant by match, and the single-variant case silently folds

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 12/100

  AeneasVerif/aeneas#1234 · Mở ngày 27/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• scalar_tac does not see through the *.rMax / *.rMin constants (no scalar_tac_simps equations)

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100

  AeneasVerif/aeneas#1233 · Mở ngày 27/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Bug: A Rust struct field named `mk` collides with the generated Lean constructor and breaks the whole file

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  bug

  Độ khó 3/5 1-2 ngày Mức phù hợp với người mới 45/100

  AeneasVerif/aeneas#1231 · Mở ngày 25/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Feature request: Full support for Higher ranked trait bounds

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy
  enhancement translation

  Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 15/100

  AeneasVerif/aeneas#1227 · 2 bình luận · Mở ngày 23/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày

• Merge the `Error` variants

  Đang mở

  ⋯Báo cáo vấn đề với issue này

  • Có gì không ổn?

  • Đã có người nhận
  • Không phù hợp cho người mới
  • Đã cũ hoặc không hợp lệ
  • Vấn đề khác…
  • Gửi Hủy

  Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 25/100

  AeneasVerif/aeneas#1225 · 18 bình luận · 1 reaction · Mở ngày 20/7/2026

  Maintainer thường phản hồi trong vòng 1 ngày