We present a work-in-progress definition of an F* effect for writing, specifying, and verifying functional correctness for higher-order programs with input-output. We then extend this effect to support potentially non-terminating programs. Crucially we do not stop at partial correctness where the specification only concludes about terminating runs, but instead rely on infinite traces to also reason about infinite runs. We aim to use this to verify meaningful properties of infinite loops, such as the main loop of a web server. As F* does not natively support coinduction, we encode specifications about infinite traces using an impredicative encoding of an infinite loop at the level of specifications.