Skip to main content
ThunderLang

Architecture

How Thunder works.

Thunder is built the way Java is: a language, a compiler, a portable model, and an engine that runs it. ThunderLang is the language; the Thunder Compiler turns it into the Intent Graph; the Thunder Engine executes and proves it, deterministically and offline. OpenThunder is the platform that keeps the proof honest over time.

The shape of it

ThunderLang is to the Thunder Engine what Java is to the JVM.

If you know the Java stack, you already know this one.

In the Java worldIn ThunderWhat it is
Java (the language)ThunderLangthe language you write, in .thunder files
javac (the compiler)Thunder Compilersource to the Intent Graph and to target code
bytecodeIntent Graphthe canonical compiled model everything binds to
the JVMThunder Engineruns and proves intent deterministically, no AI
OpenThunderthe platform that proves it stays true over time

The short name is Thunder; the language is ThunderLang; the CLI is thunder.

From intent to proof

One pipeline, every stage inspectable.

01
ThunderLang
goals, guarantees, prohibitions, decisions, tests
02
Thunder Compiler
parse, type, and compile
03
Intent Graph
the canonical model (intent-graph-v1)
04
Thunder Engine
run · test · prove (deterministic)
05
Targets + Proof
TypeScript, Python, … and an intent-proof-v1 artifact

The compiler and engine are deterministic. AI can help you author intent, but it never decides whether something is proven, that is the engine's job, and every stage is inspectable by the engineer who owns it.

The parts

Five names, one system.

ThunderLang

the language

What you write. A mission states its goal, typed inputs and outputs, the guarantees that must always hold, the behaviors that are prohibited, and how each is verified. Files use the .thunder extension (.tl is an accepted shorthand).

Thunder Compiler

javac's analog

Turns ThunderLang source into the canonical Intent Graph, and from there into target code, docs, schemas, and a test plan. Deterministic: the same source always compiles to the same graph.

Intent Graph

the bytecode

The stable, versioned model (intent-graph-v1) that every tool binds to, editors, the engine, generators, and OpenThunder. It is what makes intent portable across languages and tools.

Thunder Engine

the JVM's analog

The deterministic runtime. It executes intent, runs decisions, simulates lifecycles, evaluates contracts, runs tests (example, contract, property, scenario, mutation), and emits proofs. No AI, no account, no network.

OpenThunder

the platform above

Consumes the proof artifact and the Intent Graph, then adds what only an independent observer can: the Change Ledger, proof freshness at scale, verification against the real repo and runtime, and policy gates. ThunderLang defines and proves locally; OpenThunder proves it stays true.

The thunder CLI

Powerful on its own. No account, no network, no AI.

The Thunder Engine ships as one binary, thunder. Define, build, test, and prove entirely on your machine. OpenThunder is a layer you add, not a dependency you need.

checkruntestproveverifybuildgraphatlasliftdiff
# scaffold, then work by mission name , no paths
$ thunder new CreateInvoice
$ thunder mission CreateInvoice test
$ thunder mission CreateInvoice prove
# or point a verb straight at a file
$ thunder run eligibility.thunder --inputs '{"age":20}'
CanEnroll: Eligible [rule: adult]
# prove it, honestly
$ thunder test invoice.thunder --contracts --strict
UNVERIFIED never INV-N-004: invoice an unapproved order

Files

Write it in .thunder.

The canonical extension is .thunder. The compiler also accepts the .tl shorthand, and reads legacy .intent sources.

CreateInvoice.thunder
1mission CreateInvoice
2
3goal
4 Generate an invoice from approved orders
5
6guarantee duplicate invoices are not created
7 id INV-G-001
8 verify by evidence
9 database contains AuditRecord
10
11never invoice an unapproved order
12 id INV-N-004
13
14target
15 TypeScript
16 Python