Bounded-retry agent — the verified-termination poster child

soma.toml

[package]
name = "agents-corpus"
version = "0.1.0"
description = "Verified AI-agent example cells (training corpus)"

# Agent LLM config. `mock = "echo"` keeps every example in this directory
# hermetic: `soma test` / `soma run` need no network and no API key, and
# results are deterministic. For a live run, delete the `mock` line (or
# override with SOMA_LLM_MOCK) and provide the key via env.
[agent]
provider = "anthropic"
model    = "claude-opus-4-6"
key      = "${ANTHROPIC_API_KEY}"
mock     = "echo"

# Termination proof for verified_termination.cell's `workflow` machine:
# every path eventually reaches a terminal, no deadlocks.
# `cells` scopes these properties to Solver — the other agents in this
# directory have their own state names and must not inherit them.
[verify]
cells = ["Solver"]
deadlock_free = true
eventually    = ["done", "failed"]

[verify.after.understanding]
eventually = ["solving", "failed"]

[verify.after.solving]
eventually = ["verifying", "failed"]

[verify.after.verifying]
eventually = ["done", "failed"]

bounded_retry.cell

// Bounded-retry agent — the verified-termination poster child.
// A naive `failed -> working` retry arrow creates a livelock the model
// checker would reject. Here the retry COUNT lives in memory and the loop
// is bounded, so the machine always reaches succeeded or exhausted.
//
// Run:  SOMA_LLM_MOCK=echo soma run bounded_retry.cell --signal attempt "flaky-op" 2
// Test: SOMA_LLM_MOCK=echo soma test bounded_retry.cell

cell agent Retrier {
    face {
        signal attempt(name: String, fail_times: Int) -> Map
    }

    state run {
        initial: idle
        idle      -> working
        working   -> succeeded
        working   -> exhausted
        *         -> failed
    }

    // Simulates an operation that fails `fail_times`, then succeeds.
    // The loop is bounded by max_tries, so it cannot run forever.
    on attempt(name: String, fail_times: Int) {
        let id = to_string(next_id())
        transition(id, "working")

        let max_tries = 5
        let tries = 0
        let ok = false
        while tries < max_tries {
            tries = tries + 1
            if tries > fail_times {
                ok = true
                break
            }
        }

        if ok {
            transition(id, "succeeded")
            return map("status", "succeeded", "op", name, "tries", tries)
        }
        transition(id, "exhausted")
        map("status", "exhausted", "op", name, "tries", tries)
    }
}

cell test RetryTests {
    rules {
        // Fails twice then succeeds on the 3rd try.
        assert attempt("op", 2).status == "succeeded"
        assert attempt("op", 2).tries == 3
        // Fails more than the bound → exhausted, but still terminates.
        assert attempt("op", 9).status == "exhausted"
        assert attempt("op", 9).tries == 5
        // Succeeds immediately.
        assert attempt("op", 0).tries == 1
    }
}