As Markus said, Thomas' repo and mine are written in TLA+, but if you have specific questions we'd be happy to answer.
We had a quick Zoom meeting the other day and it was fun to talk and compare our solutions.
About your module:
First, I'd advise you reconsider the x \in Input bit. As Input is a sequence and not a set, it can't work.
Second, using a while ... end while; around your with blocks will translate into a much more readable TLA+, which you
can inspect to get more insight on what it is you are actually writing.
Third, here you are trying to find the pair of integers x and y such that x + y = Sum, but your assertion is written in a way
which will halt TLC for any other pair. It will fail on the first state it explores right after the initial state. Unless it stumbles
upon that pair on the first attempt, it's never going to get to the solution.
In Advent Of Code, you're playing TLC as a problem solver rather than a checker: try to write invariants opposite of what
you'd want in a real specification.
Lastly, I'd avoid assert, because if you actually find the solution, you will not see which x and y make the solution, just
an assertion failure message.
I got bored when I saw the problem statements of days 4 and 5 and all the parsing involved. The recursive operators I
originally wrote for parsing day 2 and 3 inputs didn't satisfy me at all.
So I got sidetracked and implemented custom modules for parsing which I've just got working  (caution, it's Clojure code).
With that it's possible that I'll find motivation for the other exercises.
Thomas went further if you're interested in solutions for days 4+.