Yes that's right, they're checked at runtime (with the option to disable the checks if the performance cost is a concern) and failed checks simply throw exceptions.
The hints aren't used for other purposes at compile time yet, but they could enable some warnings.
It looks like Koto only checks types at run-time. That means its type annotations are essentially shorthand for something like Python's `if not isinstance(...): raise TypeError`.