# costwright: Static Budget Certificate Verification for LLM Agent Workflows

> costwright is a static analysis tool that can predict the worst-case budget upper limit of LLM agent workflows before code execution. It is based on the cost correctness theorem formally verified with Lean 4, supports frameworks like LangGraph, CrewAI, and OpenAI Agents SDK, and can identify budget risks without executing code.

- 板块: [Openclaw Llm](https://www.zingnex.cn/en/forum/board/openclaw-llm)
- 发布时间: 2026-06-13T19:46:11.000Z
- 最近活动: 2026-06-13T19:49:48.553Z
- 热度: 154.9
- 关键词: LLM, 智能体, 预算控制, 静态分析, 形式化验证, Lean 4, LangGraph, CrewAI, 成本管理, CI/CD
- 页面链接: https://www.zingnex.cn/en/forum/thread/costwright-llm
- Canonical: https://www.zingnex.cn/forum/thread/costwright-llm
- Markdown 来源: floors_fallback

---

## [Introduction] costwright: Static Budget Certificate Verification Tool for LLM Agent Workflows

costwright is a static analysis tool for LLM agent workflows that can predict the worst-case budget upper limit and verify budget certificates before code execution. It is based on the cost correctness theorem formally verified with Lean 4, supports frameworks like LangGraph, CrewAI, and OpenAI Agents SDK, and can identify budget risks without executing code. The original author/maintainer is hernaninverso, and the project is open-sourced on GitHub (link: https://github.com/hernaninverso/costwright). Release time: 2026-06-13T19:46:11Z.

## Background: Budget Risks in LLM Agent Workflows

With the application of LLMs in automated workflows, the risk of budget overruns is becoming increasingly prominent. Traditional runtime trackers can only count costs after the fact and cannot provide early warnings. Research shows: 88% of loop workflows rely on framework default limits or no limits; LangGraph's default recursion limit was only 25 before v1.0.6, and 1000 after; only 12% of LLM calls set explicit token limits. Core question: How to avoid infinite loops or high costs when agents make autonomous decisions?

## Core Design Philosophy: Static Verification and Formal Guarantees

As a static budget certificate verification tool, costwright differs from runtime trackers by analyzing the workflow graph structure before execution to predict the worst-case budget upper limit. Its core advantage lies in the machine-verified Lean4 cost correctness theorem, which guarantees "well-typed ⟹ expenditure ≤ declared budget". It analyzes code via pure AST, has zero execution dependencies, and does not run user code.

## Technical Implementation and Workflow

costwright supports frameworks like LangGraph, CrewAI, and OpenAI Agents SDK. Usage steps: After pip installation, execute `costwright check .`. Analysis report categories: certifiable, default_dependent, non_certifiable, runaway, parse_error. The conservative design ensures no false security guarantees are provided.

## Practical Application Scenarios and Value

costwright can be integrated into CI/CD pipelines (e.g., GitHub Action), with automated verification controlled via `--json` output and `--fail-on` policies. The `caps` command identifies LLM constructs without token limits and provides parameter recommendations (e.g., max_output_tokens for OpenAI, max_tokens for Anthropic, etc.). It can also generate diff patches (`--patch`) but does not directly modify user files, maintaining audit traceability.

## Limitations and Future Directions

costwright does not handle constructs like Send fan-out, interruptions/human-machine collaboration, CrewAI hierarchical mode, dynamic goto (marked as non_certifiable). The current boundary is the worst case (over-approximation), and tighter boundary optimization is on the roadmap. The experimental `fuse` feature bundles budget and risk certificates but does not provide compositional guarantees; non-interference theorems are future work.

## Summary and Insights

costwright is an important step for LLM agent engineering towards formal methods; verifying budget constraints in advance in complex systems has practical value. It translates theory into an engineering tool, improving agent reliability. For teams, adding CI checks without modifying the architecture can significantly enhance cost controllability, making it a low-cost, high-value budget risk assessment solution.