- Author
- dollspace-gay and maxinelevesque (language authors); catalogue maintained by Alasdair Allan
- Published
- First seen June 2026; catalogue page last updated 9 November 2026
- Kind
- Catalogue entry describing a verification-oriented programming language
- Original
- agentlanguages.dev/languages/thermite/
- Subject
- Programming languages and types
What it is
The agentlanguages.dev catalogue lists languages made for coding agents. This entry covers Thermite, written in Rust and Lean 4. It names design relatives and a short timeline.
What it says
- Thermite requires every function to carry req, ens and fx clauses.
- Its checker Forge rates each obligation on an assurance ladder from L0 to L4.
- A counterexample counts as a failure, never as a downgrade.
- The project-level assurance is the minimum across functions, so a runtime-only boundary shows.
- Forge checks that declared effects hold up the call graph and derives a seccomp allowlist.
- Agents can write a contract around a typed hole, then fill it with forge commands.
What evidence it gives
The entry is descriptive. It names tools, commands and repository contents, such as conformance programs and an audit command. It shows one short code example. It gives no benchmarks.
Interests and limits
The entry summarizes the project's own claims, and the language is experimental. The entry says the complete path is tested on x86-64 Linux. It says the effect allowlist limits syscalls, not resources. It also says a machine check cannot prove that a contract matches intent. Nothing was run.