Issues

• Bug: fatal runtime error: stack overflow, aborting during charon cargo --preset=aeneas

  C-bugE-needs-minimization
  AeneasVerif/charon#1519 · Filter by author LebedevRI opened on Oct 13, 2026
  1

• Remove the "ULLBC" terminology

  AeneasVerif/charon#1517 · Filter by author Nadrieril opened on Oct 12, 2026

• Bug: floats aren't bit-precise

  C-bugS-representation
  AeneasVerif/charon#1507 · Filter by author N1ark opened on Oct 7, 2026
  1

• Feature request: Export the crate root in the LLBC output

  AeneasVerif/charon#1505 · Filter by author mpenciak opened on Oct 5, 2026
  1

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

  C-bug
  AeneasVerif/charon#1504 · Filter by author oliver-butterley opened on Oct 5, 2026
  4

• Clarify Asserts

  S-representation
  AeneasVerif/charon#1496 · Filter by author Nadrieril opened on Oct 1, 2026

• Add assumptions on region binders

  S-representation
  AeneasVerif/charon#1494 · Filter by author Nadrieril opened on Sep 30, 2026

• Turn the hax subcrate into a general-purpose one

  A-internal
  AeneasVerif/charon#1483 · Filter by author Nadrieril opened on Sep 25, 2026

• Clarify the pretty-printing flags

  A-build-system
  AeneasVerif/charon#1482 · Filter by author Nadrieril opened on Sep 25, 2026

• Build the full-MIR sysroots ourselves

  A-build-system
  AeneasVerif/charon#1475 · Filter by author Nadrieril opened on Sep 22, 2026
  3

  

• Panic on #![no_core] crates

  C-bugneeded-for-soteria
  AeneasVerif/charon#1396 · Filter by author N1ark opened on Aug 31, 2026

• Bug: associated type of a for<'a> bound becomes type_error

  C-bugneeded-for-aeneas
  AeneasVerif/charon#1362 · Filter by author MantasBaksys opened on Aug 21, 2026
  1

• Feature request: include global magic functions

  needed-for-soteria
  AeneasVerif/charon#1344 · Filter by author N1ark opened on Aug 3, 2026
  3

• Closure sub-items cannot be targeted by --opaque/--exclude name patterns — contradicts the documented "item and all subitems" opacity

  A-name-matcher
  AeneasVerif/charon#1339 · Filter by author PlanetMacro opened on Jul 31, 2026
  1

• Document charon_lib

  AeneasVerif/charon#1299 · Filter by author Nadrieril opened on Jun 25, 2026
  1

• [charon-ml] LLBC loader uses both result and exception

  AeneasVerif/charon#1287 · Filter by author niooss-ledger opened on Jun 13, 2026
  4

• Feature request: dynamically-linked plugin system

  AeneasVerif/charon#1286 · Filter by author Nadrieril opened on Jun 12, 2026
  1

• Bug: weirdly typed ProjectionElem::PtrMetadata

  C-bugneeded-for-soteria
  AeneasVerif/charon#1281 · Filter by author N1ark opened on Jun 11, 2026

• Add a lot of examples in docs

  AeneasVerif/charon#1277 · Filter by author Nadrieril opened on Jun 8, 2026

• Split up AggregateKind::Adt

  S-representation
  AeneasVerif/charon#1276 · Filter by author Nadrieril opened on Jun 8, 2026

• Clarify the CLI flags

  AeneasVerif/charon#1252 · Filter by author Nadrieril opened on Jun 3, 2026

• Make the AST structs and enums non-exhaustive

  S-representation
  AeneasVerif/charon#1250 · Filter by author Nadrieril opened on Jun 2, 2026

• Precisely track late-bound lifetimes

  needed-for-aeneasS-representation
  AeneasVerif/charon#1237 · Filter by author Nadrieril opened on Jun 1, 2026

• Feature request: start from #[test] functions

  needed-for-soteria
  AeneasVerif/charon#1235 · Filter by author N1ark opened on Jun 1, 2026
  1

• Feature request: represent allocations accurately

  needed-for-soteria
  AeneasVerif/charon#1225 · Filter by author Nadrieril opened on Jun 1, 2026