All issues

touchTask should return `Option (Task × Promise)`: a task without a promise is not a representable state

#10

· dtornow opened

on Aug 11, 2026

Promise/task coupling should be a declared invariant, not a rule

#9

· dtornow opened

on Aug 9, 2026

Backport the internal rule names from the Verus model: every rule processes something; absorb R2 taskFulfillment into the coupled write

#8

· dtornow opened

on Aug 9, 2026

Make the read/write discipline a type, not a convention: `H := ReaderT ServerState (Writer (List Effect))`

#7

· dtornow opened

on Aug 2, 2026