Issues

• [CN_Rocq] [CN_Lean] Function definition translations incompatible with VIP resource algebra

  rems-project/cn#669 · Filter by author yinamy opened on Sep 25, 2026

• [CN-Rocq] Rocq version of CN_Lib is behind Lean version

  rems-project/cn#668 · Filter by author yinamy opened on Sep 25, 2026

• [CN-Rocq] [CN-Lean] Broken tests

  rems-project/cn#667 · Filter by author yinamy opened on Sep 25, 2026

• [Fulminate] Pointer dereference in an apply argument generates invalid C

  rems-project/cn#655 · Filter by author moratorium08 opened on Sep 21, 2026
  1

  

• [Fulminate] Make lemma failures clearer

  Fulminate
  rems-project/cn#654 · Filter by author rbanerjee20 opened on Sep 15, 2026

• [Fulminate] Single-statement loops - injection-induced syntax error

  Fulminate
  Bug

  rems-project/cn#652 · Filter by author rbanerjee20 opened on Sep 14, 2026

• [CN-Rocq] Structs with fields of the same name are translated incorrectly to Rocq

  rems-project/cn#644 · Filter by author moratorium08 opened on Aug 30, 2026
  3

• [CN-Testing] Add CLI flags fixing paper settings

  BennetDarcy
  Feature

  rems-project/cn#546 · Filter by author ZippeyKeys12 opened on May 19, 2026
  1

  

• [Bennet-AD] Port over changes

  Bennet
  Task

  rems-project/cn#545 · Filter by author ZippeyKeys12 opened on May 19, 2026
  

• [CN-Testing] Support all types of ghost arguments in input generators

  BennetCN spec testingDarcyenhancement
  Feature

  rems-project/cn#531 · Filter by author ZippeyKeys12 opened on Apr 11, 2026
  

• [CN-Testing] Support C-typed ghost arguments in input generators

  BennetCN spec testingDarcyenhancement
  Feature

  rems-project/cn#530 · Filter by author ZippeyKeys12 opened on Apr 11, 2026
  

• [Fulminate] Fix (or delete) --without-ownership-checking mode

  rems-project/cn#512 · Filter by author rbanerjee20 opened on Mar 22, 2026

• README for Bennet

  rems-project/cn#501 · Filter by author prasitaGit opened on Mar 11, 2026
  

• [Fulminate] Stop filtering out legitimate assert(true)s

  rems-project/cn#500 · Filter by author rbanerjee20 opened on Mar 6, 2026

• cn test fails with a mysterious error

  rems-project/cn#492 · Filter by author podhrmic opened on Jan 29, 2026
  1

  

• [Seq-Test] Make Fulminate usage consistent with new API

  CN sequence testing
  rems-project/cn#470 · Filter by author ZippeyKeys12 opened on Dec 3, 2025

• [Testing] Gradual Rustification of runtime libraries

  BennetCN spec testingDarcy
  Task

  rems-project/cn#462 · Filter by author ZippeyKeys12 opened on Nov 21, 2025
  

• [Fulminate] Clarify Fulminate API

  rems-project/cn#461 · Filter by author ZippeyKeys12 opened on Nov 21, 2025
  1

• [Testing] Separate test runner

  CN spec testing
  Task

  rems-project/cn#459 · Filter by author ZippeyKeys12 opened on Nov 21, 2025
  

• [Bennet] Support CN value generation

  BennetCN spec testing
  Feature

  rems-project/cn#457 · Filter by author ZippeyKeys12 opened on Nov 21, 2025
  

• [Fulminate] Generate functions for spec-checking

  Fulminate
  Task

  rems-project/cn#454 · Filter by author rbanerjee20 opened on Nov 19, 2025
  

• [CN-exec] Provenance issue: function prologues have to be inserted before CN_LOAD

  bugFulminate
  Bug

  rems-project/cn#453 · Filter by author moratorium08 opened on Nov 19, 2025
  1

  

• Fix div, mod, pointer-diff in bitvector mode

  rems-project/cn#438 · Filter by author cp526 opened on Nov 9, 2025

• [Testing] Better handling of globals

  CN spec testing
  rems-project/cn#420 · Filter by author ZippeyKeys12 opened on Nov 4, 2025
  1

  

• [CN-Exec] Incorrect instrumentation for the use of return values

  rems-project/cn#392 · Filter by author moratorium08 opened on Oct 28, 2025
  3