Show HN: Untyped – check recorded agent runs against a TLA+ spec

Category: devtools

Tags: tla-plus, model-checking, agent-systems, durable-execution, trace-validation

Score: 7.0/10 (Innovation: 8, Technical: 8, Documentation: 8, Utility: 4)

Untyped provides a TLA+ specification of the protocol between an agent harness and a side-effecting tool on a durable-execution runtime, and uses model checking plus trace validation to check whether harness designs and recorded runs uphold invariants like at-most-once effects, approval before destructive actions, and budget limits. It is interesting because it formalizes a subtle, practical problem in agent systems and offers a concrete, executable methodology for finding bugs in retry and idempotency logic.

Target audience: backend developers, distributed systems engineers, agent framework builders

Repository: https://github.com/untyped-ai/untyped · TLA · MIT · 3 stars

View on Hacker News