since generation is not deterministic, how do they verify the lock file?

Generation of the lock file is deterministic.

See here for information about determinism https://github.github.com/gh-aw/reference/faq/#determinism

The generation of the workflow file from the input markdown file is deterministic. It's what the agent does when running the workflow that is non-deterministic.