A counterexample is a failure, never a downgrade.
## What it looks like.
fn sum(xs: &[u32]) -> u64
req xs.len() <= 1_000_000
ens result == spec_sum(xs)
fx pure
{
let mut acc: u64 = 0;
let mut i: usize = 0;
while i < xs.len()
inv acc == spec_sum(&xs[..i])
dec xs.len() - i
{
acc = acc + xs[i] as u64;
i = i + 1;
}
acc
}
The contract, loop invariant, and termination measure are part of the source. result names the return value inside the postcondition.
## Distinctive moves.
- **Per-obligation assurance.** Forge records the engine and trust profile for
each clause. The project-level headline is the minimum over the functions in
scope, so one runtime-only boundary is not hidden behind a proof elsewhere.
- **Checked solver reconstruction.** Eligible nonlinear arithmetic,
fixed-width bit-vector, and finite first-order relation or array clauses take
specialised L4 routes, and the three differ in what Lean is asked to check.
Finite relation and array clauses get genuine certificate replay: an external
SAT run's LRAT proof is re-checked against a problem Lean recomputes for
itself. Bit-vector and linear-integer clauses are re-proved in Lean
independently, with the solver's own proof never consumed. The nonlinear
route transports a trusted solver answer from the reals to the integers
through a kernel-checked lemma. The ordinary all-input route through Verus is
not reconstructed, and the project's trust document enumerates what remains
trusted.
- **Contract-quality checks.** Mandatory contracts ensure that a specification
exists, but do not establish that it expresses the author's intent. Forge
probes for vacuous conditions and tests whether mutations survive the stated
contract. These checks reduce the space of weak specifications without
claiming to close the intent gap.
- **Effects cross the compilation boundary.** The `fx` row is checked for
subsumption up the call graph, then used to derive a seccomp allowlist for
hosted executables. Rust lowering also retains runtime contract checks,
keeping the L1 result active when stronger evidence is unavailable. The
allowlist is per effect verb rather than per resource — the
parenthesised path or domain is discarded — and an open project RFC
records that a declared `write` to a region the body never touches still
certifies. The row constrains syscalls rather than confining resources.
- **Holes are a supported workflow.** An agent can write the contract around a
typed hole, inspect the open goal with `forge goal`, apply a candidate with
`forge fill`, and check again. A remaining hole prevents the item from being
built or certified.
## Maturity.
Forge parses and checks Thermite, lowers certified programs to Rust, builds
native hosted executables, and can emit freestanding `no_std` libraries for
the kernel target. The repository ships conformance programs, proof-bearing
gates, translation-validation batteries, and an audit command that re-derives
the recorded trust chain.
The full stack is experimental and operationally substantial. Verus, Lean,
Mathlib, Z3, the reconstruction tools, and optional bounded-checking tooling
sit around the Rust compiler; the complete path is tested on x86-64 Linux.
That makes the proof-bearing setup heavier and less portable than the surface
syntax suggests. The larger limit is semantic rather than operational:
machine checks can establish that an implementation meets its formal
contract, while the correspondence between that contract and the intended
behaviour remains reviewable evidence rather than a closed theorem.
## Agent tooling.
`THERMITE.skill.md` is generated from the same registries and exhaustive
compiler matches that define Forge's accepted surface, with a token-budget
gate to keep the reference bounded. `forge skill` emits the canonical form or
a Claude Code variant and can check a committed copy for drift. The `goal`,
`fill`, and `edit` commands expose the contract-directed repair loop, while
JSON output gives agents structured obligation results, counterexamples,
engine attribution, and certificate data. Repository-local agent files and
the same audit gates used by maintainers document the development workflow,
but they are not required to compile a Thermite program.
## Design DNA
- **[Vera](https://agentlanguages.dev/languages/vera.md)** *(Verification)* — Both require contracts and effects on every function and expose machine-oriented diagnostics. Vera removes parameter names and targets WebAssembly; Thermite keeps a Rust-shaped surface, lowers through Rust, and records a separate assurance level and trust profile for each obligation.
- **[Aver](https://agentlanguages.dev/languages/aver.md)** *(Verification)* — Both keep verification artefacts beside the function and provide agent-facing language references. Aver uses prose intent and colocated verify blocks with Lean and Dafny export; Thermite uses preconditions, postconditions, and an assurance ladder whose checked-reconstruction routes terminate in Lean.
## Timeline
- **Jun 2026** — First public release of the parser, contract language, Forge checker, Rust lowering path, and assurance certificates.
- **Jul 2026** — Checked reconstruction expanded to fixed-width bit-vectors and finite relation and array clauses, alongside the existing nonlinear arithmetic route.
---
HTML version: https://agentlanguages.dev/languages/thermite/
Catalogue index: https://agentlanguages.dev/llms.txt
Catalogue homepage: https://agentlanguages.dev/index.md