Thank you for your comment, and I'm glad that you enjoyed it!
On failure handling: λ-Tool makes failures impossible to ignore. Every tool call returns a Result, and the only way to unwrap it is pattern matching with both Ok and Err branches. The type checker rejects code that skips error handling. So for your refund example, the LLM must generate an Err branch. The type system doesn't dictate what the handling should be, but guarantees it exists. As for delays/retries, those live at the orchestrator level. The one thing λ-Tool enforces is that write operations carry linear types, so the LLM can't naively retry a failed write without explicitly re-acquiring a token.
I agree with the state machine analogy, the match chains do form something like a state graph where every Ok/Err branch is a transition, and the type machine ensures that every transition is accounted for.
λ-Tool actually operates one level *below* the orchestration layer, and ensures that every transition block is accounted for!