Issues

• Modular analysis never checks the subtype checks of ghost variables and constants in the contract of an imported node

  comp:coreimpact:soundnesslang:contractlang:refinement-typestatus:triage
  Bug

  kind2-mc/kind2#1878 · Filter by author daniel-larraz opened on Oct 30, 2026
  

• Charge the counterexample checks of a round by fixed costs rather than wall-clock time

  comp:corecomp:smtimpact:incompletelang:rec-functionneeds:designstatus:triage
  Task

  kind2-mc/kind2#1869 · Filter by author daniel-larraz opened on Oct 29, 2026

• A recursive call under a quantifier in the contract of an opaque function makes the solvers fail with an unknown constant

  comp:frontendimpact:crashlang:contractlang:quantifierlang:rec-functionstatus:triage
  Bug

  kind2-mc/kind2#1863 · Filter by author daniel-larraz opened on Oct 28, 2026

• A restart that mentions a pattern variable bound by matching a quantified variable makes the solvers fail with an unknown constant

  comp:frontendimpact:incompletelang:datatypelang:matchlang:quantifierstatus:triage
  Bug

  kind2-mc/kind2#1857 · Filter by author daniel-larraz opened on Oct 28, 2026

• Match arm bound by a top-level variable pattern is left unbound when the scrutinee type is not inferred: a type ascription in it is wrongly rejected or fails an assertion

  comp:frontendimpact:crashimpact:rejects-validlang:datatypelang:matchlang:refinement-typestatus:triage
  Bug

  kind2-mc/kind2#1839 · Filter by author daniel-larraz opened on Oct 24, 2026

• Accept a match block on a node call inside a restart block

  comp:frontendimpact:rejects-validlang:clocklang:matchstatus:triage
  Bug

  kind2-mc/kind2#1834 · Filter by author lorchrob opened on Oct 23, 2026

• Datatype field with a quantified refinement type fails an assertion in lustreAstNormalizer

  comp:frontendimpact:crashlang:datatypelang:quantifierlang:refinement-typestatus:triage
  Bug

  kind2-mc/kind2#1833 · Filter by author lorchrob opened on Oct 23, 2026

• Generated nodes re-derive input refinement types: node calls in them are re-instantiated or desugared twice

  comp:frontendimpact:rejects-validimpact:spurious-cexlang:clocklang:refinement-typestatus:triage
  Bug

  kind2-mc/kind2#1832 · Filter by author lorchrob opened on Oct 23, 2026
  1

  

• Contract ghost constant passed to a function call crashes with Not_found

  comp:frontendimpact:crashlang:contractstatus:triage
  Bug

  kind2-mc/kind2#1829 · Filter by author lorchrob opened on Oct 22, 2026

• With --ivc, a program containing a recursive function spins until the timeout computing the minimal IVC

  comp:ivc-mcsimpact:hanglang:rec-functionstatus:triage
  Bug

  kind2-mc/kind2#1828 · Filter by author lorchrob opened on Oct 22, 2026

• A contract declaration may share a name with a datatype constructor, where a node or function may not

  comp:frontendlang:contractlang:datatypestatus:triage
  Task

  kind2-mc/kind2#1825 · Filter by author lorchrob opened on Oct 22, 2026

• A binder clashing with a constructor reports a type error instead of the clash when an ascription in its scope mentions it

  comp:frontendimpact:wrong-resultlang:arraylang:datatypelang:matchlang:quantifierlang:refinement-typestatus:triage
  Bug

  kind2-mc/kind2#1824 · Filter by author lorchrob opened on Oct 22, 2026
  

• Inlined call whose arguments mix a multi-output call with other arguments crashes with Invalid_argument("List.map2")

  comp:frontendimpact:crashlang:quantifierstatus:triage
  Bug

  kind2-mc/kind2#1823 · Filter by author daniel-larraz opened on Oct 22, 2026

• Reachability and fairness conditions in moxi output

  comp:certificationcomp:outputkmoxineeds:designstatus:triage
  Task

  kind2-mc/kind2#1814 · Filter by author lorchrob opened on Oct 19, 2026

• Alpha-rename binders in one pass, and keep a map back to the names the user wrote

  comp:certificationcomp:frontendcomp:outputlang:contractlang:datatypelang:matchlang:quantifierlang:refinement-typestatus:blocked
  Task

  kind2-mc/kind2#1810 · Filter by author lorchrob opened on Oct 16, 2026
  1

• A polymorphic node importing a contract with two type arguments fails an assertion in lustreInstantiatePolyNodes

  comp:frontendimpact:crashlang:contractlang:polymorphismstatus:triage
  Bug

  kind2-mc/kind2#1808 · Filter by author lorchrob opened on Oct 16, 2026

• Check the memory of the analysis on macOS and Windows

  comp:coreos:macosos:windowsstatus:triage
  Feature

  kind2-mc/kind2#1799 · Filter by author daniel-larraz opened on Oct 14, 2026

• Array literal built from a pre in an arrow right operand fails an assertion in lustreExpr

  comp:frontendimpact:crashlang:arraystatus:triage
  Bug

  kind2-mc/kind2#1773 · Filter by author lorchrob opened on Oct 13, 2026

• Contract ghost variable nesting the same polymorphic datatype twice fails an assertion in lustreAstNormalizer (or is wrongly rejected)

  comp:frontendimpact:crashimpact:rejects-validlang:contractlang:datatypelang:polymorphismlang:setstatus:triage
  Bug

  kind2-mc/kind2#1768 · Filter by author daniel-larraz opened on Oct 12, 2026

• Nested instantiation of a polymorphic datatype is compared by name only: Opt<Opt<bool>> accepted as Opt<Opt<int>>

  comp:frontendimpact:accepts-invalidimpact:crashimpact:soundnesslang:datatypelang:polymorphismstatus:triage
  Bug

  kind2-mc/kind2#1767 · Filter by author daniel-larraz opened on Oct 12, 2026
  1

  

• Temporal operator inside a contract-import type argument escapes the function-contract and stateful-import checks

  comp:frontendimpact:accepts-invalidlang:contractlang:polymorphismlang:refinement-typestatus:triage
  Bug

  kind2-mc/kind2#1766 · Filter by author lorchrob opened on Oct 12, 2026

• Datatype and node sharing a name with different type-parameter counts: Invalid_argument("List.combine")

  comp:frontendimpact:crashlang:datatypelang:polymorphismstatus:triage
  Bug

  kind2-mc/kind2#1764 · Filter by author lorchrob opened on Oct 12, 2026

• The index variable of a comprehension named after a global constant reads the constant

  comp:frontendimpact:spurious-cexlang:arraystatus:triage
  Bug

  kind2-mc/kind2#1754 · Filter by author daniel-larraz opened on Oct 11, 2026
  1

  

• Quantifier inside a stateful restart fails in lustreAstDependencies

  comp:frontendimpact:crashlang:quantifierstatus:triage
  Bug

  kind2-mc/kind2#1741 · Filter by author daniel-larraz opened on Oct 10, 2026
  1

• Generated locals collide with user variables named '<name>_<n>' (crash or silent merge)

  comp:frontendimpact:crashstatus:triage
  Bug

  kind2-mc/kind2#1734 · Filter by author daniel-larraz opened on Oct 10, 2026