Thermite

Thermite is a new programming language designed specifically for AI agents to write code in, not humans. The core idea is that software written by AI agents is hard to trust, because there is no easy way to verify that the code actually does what the agent claims. Thermite tries to solve this by making verification a mandatory part of the language itself, not an optional add-on.

Every function in Thermite must come with a formal contract: what the function requires to be true before it runs, what it promises to be true after it runs, and what side effects it is allowed to have (such as reading files or making network calls). A separate toolchain called Forge checks these contracts using mathematical proof techniques borrowed from formal verification research. Code that passes is issued a certificate proving what was verified and how strong the proof is. Code that cannot be verified at the highest level is still allowed, but must be explicitly marked with a loud tag so auditors can find it immediately.

The verification system has multiple levels. At the strongest level, a mathematical solver proves the code correct for all possible inputs. If that times out, it falls back to checking the code up to a bounded set of inputs. If that also fails, contracts are enforced at runtime. The language is deliberately designed to be uncomfortable for humans to write, since the intended author is an AI agent that can afford to spend compute and tokens on annotation work that a human would find tedious.

The language compiles to Rust under the hood, so the final output is a native binary. The declared side effects of each function are also enforced at runtime using a Linux kernel security feature that kills any code that tries to do something it did not declare permission for.

The project describes itself as reaching a point where the full toolchain runs end-to-end, including recursive data types, effects, strings, and composable verification. The toolchain's own core logic is itself verified using the same proof tools. The license is not mentioned in the README.