In this problem session, I will introduce an effectful modal calculus and its formalization with small-step environment-based semantics.