Issues

• Suggestion: add release tags to Strata

  strata-org/Strata#1486 · Filter by author evertonfraga opened on Oct 9, 2026

• Core evaluator does not reduce concrete bitvector/integer casts

  strata-org/Strata#1484 · Filter by author aditink opened on Oct 2, 2026

• Sequence.select and Sequence.select! are unrelated in the SMT encoding

  strata-org/Strata#1482 · Filter by author kondylidou opened on Oct 1, 2026

• Define Sequence in Laurel: RawSequence datatype (length + partial Map) refined by a constrained type

  Laurel
  strata-org/Strata#1475 · Filter by author keyboardDrummer opened on Sep 16, 2026

• Laurel cannot prove two sequences equal; extensionality needs its own trigger (Sequence.equal)

  Laurel
  strata-org/Strata#1474 · Filter by author keyboardDrummer opened on Sep 16, 2026

• SMT→Lean bridge: queries mentioning datatype sorts cannot be translated

  strata-org/Strata#1472 · Filter by author kondylidou opened on Sep 6, 2026
  2

• Import conflict between Strata and Batteries over List.Forall₂ declarations

  strata-org/Strata#1462 · Filter by author chrissuu opened on Aug 8, 2026

• Enable constrained types to work with polymorphism

  Laurel
  strata-org/Strata#1456 · Filter by author keyboardDrummer opened on Jul 30, 2026

• Support shadowing of variables

  Laurel
  strata-org/Strata#1455 · Filter by author keyboardDrummer opened on Jul 30, 2026

• Support checking the wellformedness of loop invariants

  Laurel
  strata-org/Strata#1454 · Filter by author keyboardDrummer opened on Jul 30, 2026

• --vc-directory files use (get-value ...) without setting :produce-models, so cvc5 cannot replay them

  strata-org/Strata#1451 · Filter by author repowazdogz-droid opened on Jul 24, 2026

• README says counterexamples report models, but models only appear in SARIF output

  strata-org/Strata#1450 · Filter by author repowazdogz-droid opened on Jul 24, 2026

• README links docs/PythonFrontend.md, which does not exist on main

  strata-org/Strata#1449 · Filter by author repowazdogz-droid opened on Jul 24, 2026

• PrecondElim swaps de Bruijn indices in WF obligations under nested quantifiers

  strata-org/Strata#1434 · Filter by author joscoh opened on Jul 1, 2026

• Typechecker rejects unannotated quantifier binder instead of unifying to bool

  strata-org/Strata#1433 · Filter by author joscoh opened on Jul 1, 2026

• ContractPass desugaring makes well-formed partial-op postconditions unprovable

  bugLaurel
  strata-org/Strata#1418 · Filter by author fabiomadge opened on Jun 26, 2026

• Remove the Core type from Laurel

  strata-org/Strata#1411 · Filter by author keyboardDrummer opened on Jun 24, 2026
  

• Type soundness: if/loop guards silently refine an enclosing procedure's rigid type variable

  bugCore
  strata-org/Strata#1410 · Filter by author joscoh opened on Jun 24, 2026

• Enable Laurel to check for ghostness violations

  bugLaurel
  strata-org/Strata#1407 · Filter by author keyboardDrummer opened on Jun 24, 2026

• Support field-granular modifies clauses in Laurel (modifies o.f)

  enhancementLaurel
  strata-org/Strata#1402 · Filter by author julesmt opened on Jun 23, 2026
  1

  

• Type soundness: nested funcDecl generalizes over a type variable free in the ambient context

  bugCore
  strata-org/Strata#1399 · Filter by author joscoh opened on Jun 19, 2026
  

• Type soundness: call statement silently refines an enclosing procedure's rigid type variable

  bugCore
  strata-org/Strata#1397 · Filter by author joscoh opened on Jun 19, 2026
  

• Unsound: nested funcDecl specializes a procedure's type variable

  bugCore
  Bug

  strata-org/Strata#1395 · Filter by author joscoh opened on Jun 19, 2026
  

• typeDecl/funcDecl leak out of blocks and across ite branches in typeCheckAux

  bugCore
  Bug

  strata-org/Strata#1392 · Filter by author joscoh opened on Jun 18, 2026
  

• Core: path-conditions leak across procedures via structured exit — unsound (vacuous pass)

  bugCore
  strata-org/Strata#1390 · Filter by author fabiomadge opened on Jun 18, 2026