TLA-Finance

An agentic finance system can produce output that appears plausible while conflicting with the financial state or constraints it was given. The challenge is to determine whether an output is actually suspicious and explain why.

• A workflow for turning a suspicious Finance Agent output and its relevant context into a reproducible verification case.
• Formal constraints that describe what an acceptable output must preserve.
• Trace-based analysis that connects a violated constraint back to the output and relevant state.

• Case-driven evaluations centered on suspicious Finance Agent outputs.
• A Choices construct for expressing and checking alternative Finance Agent decisions within the same verification case.
• Model-checking results that show which modeled constraints hold or fail for each example.
• An interactive walkthrough that explains a flagged output through its verification trace.