-
Notifications
You must be signed in to change notification settings - Fork 27
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
An UNSAT premise set discharges every obligation vacuously and reports Tier 1 verified
bugSomething isn't workingSomething isn't workingStatus: Open.#1451 In aallan/vera;E618 rejects a verify-clean nested refinement chain at codegen, and is in no limitation table
bugSomething isn't workingSomething isn't workingStatus: Open.#1450 In aallan/vera;A true postcondition over an Array<Refined> element is refused with E500, not disclosed
bugSomething isn't workingSomething isn't workingStatus: Open.#1449 In aallan/vera;A refined handler-clause binder raises no obligation and is unguarded
bugSomething isn't workingSomething isn't workingStatus: Open.#1448 In aallan/vera;E623 reports once per contending module instead of once per contended name, so one slot conflict arrives as a cascade
bugSomething isn't workingSomething isn't workingStatus: Open.#1446 In aallan/vera;A handler-clause @Nat pattern binder over an Exn<Int> payload is disclosed but never guarded, so run -- -7 returns -7 through the @Nat slot
bugSomething isn't workingSomething isn't workingStatus: Open.#1445 In aallan/vera;apply_propose_edit replaces the server's document state even when the client declines the edit
bugSomething isn't workingSomething isn't workingStatus: Open.#1444 In aallan/vera;propose_edit applies an edit that turns a verified obligation into a timeout, without force
bugSomething isn't workingSomething isn't workingStatus: Open.#1443 In aallan/vera;validate_handler accepts a Bool -> Bool handle when both prelude layouts are present, and executing it crashes the host
bugSomething isn't workingSomething isn't workingStatus: Open.#1442 In aallan/vera;The warm VerificationSession replays a stale proof when a contract dependency two calls away changes
bugSomething isn't workingSomething isn't workingStatus: Open.#1441 In aallan/vera;The @Nat sign guard is missing at the array-element and Map-value stores
limitationKnown compilation limitationKnown compilation limitationStatus: Open.#1440 In aallan/vera;The refinement predicate at a State write boundary is obligated and unguarded
bugSomething isn't workingSomething isn't workingStatus: Open.#1439 In aallan/vera;