# Transformer VM

A deterministic transformer-shaped virtual machine that compiles a small assembly language into a runtime, executes it with no randomness, and proves the resulting computation with a transparent STARK proof system.

Transformer VM compiles a compact assembly language into a transformer-style runtime, executes it deterministically so the same program always produces the same output, records the execution trace, and proves the claimed computation with an in-repository STARK prover. The same program can also run through separate native, Burn and ONNX execution paths, and the project can fail immediately on the first point where these paths disagree, catching semantic drift before a proof is generated.

The project defines several proof surfaces at different levels of completeness: a stable surface that proves native instruction-set execution together with checks that the transformer and native paths agree, an experimental backend covering a narrower set of fixtures and lookup demos, and two artifact-only surfaces that compare the transformer path against ONNX or across all engines without yet making a full proof claim; the repository states plainly that it does not yet prove full standard-softmax transformer inference on its experimental backend.

It is written in Rust and builds on earlier published research asking whether large language models can be proven computers.

Website: https://github.com/AbdelStark/llm-provable-computer