All issues

Search results

Enable constrained types to work with polymorphism

Laurel

Status: Open.

#1456 In strata-org/Strata;

· keyboardDrummer opened on Jul 30, 2026

Support shadowing of variables

Laurel

Status: Open.

#1455 In strata-org/Strata;

· keyboardDrummer opened on Jul 30, 2026

Support checking the wellformedness of loop invariants

Laurel

Status: Open.

#1454 In strata-org/Strata;

· keyboardDrummer opened on Jul 30, 2026

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

Status: Open.

#1451 In strata-org/Strata;

· repowazdogz-droid opened on Jul 24, 2026

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

Status: Open.

#1450 In strata-org/Strata;

· repowazdogz-droid opened on Jul 24, 2026

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

Status: Open.

#1449 In strata-org/Strata;

· repowazdogz-droid opened on Jul 24, 2026

gen_smt_vcs reduction proofs break in Lean 4.31

Status: Open.

#1442 In strata-org/Strata;

· joehendrix opened on Jul 20, 2026

PrecondElim swaps de Bruijn indices in WF obligations under nested quantifiers

Status: Open.

#1434 In strata-org/Strata;

· joscoh opened on Jul 1, 2026

Typechecker rejects unannotated quantifier binder instead of unifying to bool

Status: Open.

#1433 In strata-org/Strata;

· joscoh opened on Jul 1, 2026

ContractPass desugaring makes well-formed partial-op postconditions unprovable

bugSomething isn't workingSomething isn't working

Laurel

Status: Open.

#1418 In strata-org/Strata;

· fabiomadge opened on Jun 26, 2026

Remove the Core type from Laurel

Status: Open.

#1411 In strata-org/Strata;

· keyboardDrummer opened on Jun 24, 2026

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

bugSomething isn't workingSomething isn't working

Core

Status: Open.

#1410 In strata-org/Strata;

· joscoh opened on Jun 24, 2026