LOGOS reads as structured English and compiles to Rust. It's the single executable specification that appears at every level of the stack: the interpreter runs it, the register virtual machine runs it, and the dataflow tiles are placed from it.
The compiler, the interpreter and the language server below are the real ones, compiled to WebAssembly and running in this tab. Nothing is sent anywhere, and nothing loads until you ask. The bundle is a browser build, about 1.2 MB over the wire and 3.8 MB unpacked, rather than the full 11.6 MB engine above, and it's fetched on your first interaction rather than with the page.
Press Run, edit anything, hover a name to see what the language server knows about it, or press Control and Space for suggestions. It's the same server that backs the editor plugins, so what it offers here is what it offers in an IDE.
Source: The compiler, the language server, and the WebAssembly bindings, on GitHub(opens in a new tab)
A board, a function that scans the eight winning lines, and a move the program asserts is legal. The game arrives unfinished on purpose. Click a square: the move is written into the program above, the whole program runs again, and the board is its output
Runs and analyzes here. The Rust is emitted by the native compiler; the Rust it emits is shown above.
Compiler loads on first use, about 1.2 MB
Run the program, or click a square, to draw the board.
A click appends the square to the move list in the program above and runs it again. What you see here is the program's own output, parsed back into nine squares.
Syntax
The language, as far as this build implements it. Every form was compiled and run before it was written down. Click one to insert it at the caret.
The colors come from the language server's semantic tokens rather than a list of keywords matched by a regular expression. Gold is the language, emerald is a literal you wrote, plain text is a name you chose, and grey is punctuation. Where the coloring looks wrong, that is a real disagreement about the parse rather than a highlighting bug.
## To is a Markdown header. The file renders as documentation and compiles as source, so there is no separate doc comment syntax because there is no need for one.
Types are declared and checked. (n: Int) -> Int is not decoration.
Sentences end in a period, including Return 1. The block structure is Markdown's, not a brace convention wearing English clothes.
02-functions.lg
## To factorial (n: Int) -> Int:
If n is at most 1:
Return 1.
Return n * factorial(n - 1).largo emit rust
fn factorial(mut n: i64) -> i64 {
let mut __acc: i64 = 1;
loop {
if (n <= 1) {
return __acc * 1;
}
{
let __acc_expr = n;
__acc = __acc * __acc_expr;
let __tce_0 = logos_sub_i64(n, 1);
n = __tce_0;
continue;
}
}
}A LOGOS file is parsed once, and what comes out is two trees rather than one. The imperative tree is what the program does. The logical tree is what the program claims. The assert bridge is where the second becomes an obligation on the first, which is the reason a claim can sit beside the code it concerns rather than in a separate proof file.
Below the bridge there is one program again. The register bytecode is what the interpreter walks, what the virtual machine executes, and what the JIT stitches into native x86-64 once a loop has run long enough to earn it. Most of the ahead of time backends lower from that same bytecode, which is why the program you run in the playground and the program that reaches a chip are the same program rather than two that have to be kept in agreement.
Tree-walk interpreter
Runs the tree as parsed, for instant feedback while you are writing.
Register virtual machine
Runs the register bytecode, and is the reference every other target is compared against.
Copy and patch JIT
Stitches native x86-64 out of pre-compiled fragments once a loop earns it.
Most of the ahead of time backends lower from this same bytecode.
Where the specification, the reference implementation, and the compiled artifact are three separate things, agreement between them is something you test for. Where they are one artifact viewed at different levels, agreement is something you prove. That is the whole reason the toolchain has a language of its own rather than a pass over someone else's.
There are two halves to this, and being exact about which half does what is the whole answer. At the surface the language is about memory without a collector. Every value is Owned until something happens to it: Give x moves it, Show x lends it, and copy of x says you meant a copy. The checker follows each name through Owned, Moved and Borrowed, merges those states back together where branches rejoin, and answers a mistake with "Cannot use x after giving it away" before any Rust is generated.
What a program is allowed to say about its own values stays deliberately small. A refinement is a comparison over the name being declared, x > 0 or n < 100, and anything richer belongs in Assert that, which hands the claim to the proof engine rather than to the type checker. That line sits where it does on purpose: a type system rich enough to express every claim is a type system a reader has to study before writing a line.
The other half sits underneath. The kernel is a Calculus of Constructions checker with inductive types, cumulative universes over an impredicative Prop, positivity and termination checks, and proof terms it re-derives rather than trusts. That strength is the kernel's. A program reaches it by making a claim, not by writing the proof language itself.
Ownership is checked before the Rust compiler ever sees the program, by a lightweight data flow analysis that runs at check time in milliseconds and catches the 90% of ownership mistakes people actually make. Refinements are comparisons over the declared name, and anything richer is an Assert the proof engine discharges.
Eight conflict free replicated types are keywords here rather than a library you import. A record declared Shared names what each field converges as, and the compiler emits the merge for the whole record. Merge, Converge, Increase, Append and Resolve are statements in the language rather than methods on an object you remembered to reach for.
Underneath are the eight standard structures: GCounter and PNCounter for counters, LWWRegister and MVRegister for registers, ORSet and ORMap for sets and maps, RGA and YATA for sequences. Each one carries causal metadata, dots and vector clocks, and ships changes as deltas where the structure allows it. The same merge has also been lowered to RTL and checked against the virtual machine, which is the standard every other part of this stack is held to.
The useful property is what they do not need. Two replicas reach the same value without a shared clock and without a round trip to agree on an order, so a merge does not care whether an update arrived seconds ago or minutes ago, or whether the link was down in between. That is the ordinary condition for a satellite constellation and for space operations generally, where a round trip is measured in seconds or minutes and a partition is a Tuesday rather than an incident. A last writer wins register settles by causal metadata rather than by a wall clock, so two sides never have to agree about the time in order to agree about the value.
A merge picks one outcome deterministically, and a register takes the conflict policy the program declares. The replicated types run anywhere the engine runs, including in a browser, because the crate that holds them performs no IO by design.
The list below is the part of the language a program reaches for without importing anything. Units and time get the most room here because they carry arithmetic most languages hand to a library and then round.
What a program computes with before anything is imported.
Measurements carry their dimension, and conversions stay exact.
How data and code are shaped.
Concurrency that reproduces.
Where a claim goes once the type system has said all it can.
Measured against compiled languages
Geometric mean speed against C across 32 benchmarks, higher is faster. Every implementation runs the same algorithm and produces identical, verified output, and every compiled language is built at full matched optimization.
On 5 of the 32 benchmarks the LOGOS compiler reduces the work itself, folding a recursive function into a closed form, so it runs a faster algorithm rather than faster machine code. Those wins are real and each one is auditable in the generated Rust. Removing them and comparing only the 27 programs where LOGOS and C compile the same algorithm gives 1.27x the speed of C.
The 2.62x geometric mean says what the toolchain does to a real program. The 1.27x figure says what the code generator does when the comparison is held level.
Measured with hyperfine, 10 runs and 2 warmup, median reported. Intel Core i9-14900K, Ubuntu 24.04.2. Measured on LOGOS v0.10.0, with the Rust shown earlier on this page emitted by 0.10.1; the current release is 0.11.0, August 2026.
| Language | Speed vs C |
|---|---|
| LOGOS | 2.62x |
| Rust | 1.25x |
| Zig | 1.21x |
| C++ | 1.03x |
| C | 1.00x |
| Go | 0.73x |
| Java | 0.65x |
| Nim | 0.65x |
LOGOS also runs interpreted, through a bytecode virtual machine with a copy and patch JIT. Against Node and V8 it reaches first output in 2.3ms rather than 13.8ms, about six times quicker, which is the number that matters for short lived work such as functions, command line tools, and scripts.
On long running loops V8's optimizing JIT pulls ahead. Across 30 benchmarks the interpreter averages 1.04x the speed of V8, which is competitive rather than dominant.
The whole engine ships as an 11.6 MB WebAssembly bundle, with the same virtual machine and JIT as the native build and no install. The engine you ship is 24.7 MB against Node and V8 at 119.0 MB as built, or 19.3 MB against 102.1 MB stripped of debug symbols.
A hardware specification is written in English before it's written in anything else. The compiler parses that English into first order logic, lowers it through Kripke semantics so that words like "until" and "in the next cycle" become explicit quantification over states, and emits a SystemVerilog assertion.
The pairs below are real output. Each English sentence is taken from the hardware test corpus in the public repository, and each assertion is what the compiler printed for it.
Specification, in LOGOS
SystemVerilog assertion
Bounded response
assert property (@(posedge clk) Assert_irq_ |-> ##[0:3] Assert_irq_ack_);Specification, in LOGOS
SystemVerilog assertion
Next cycle, with a negated antecedent
assert property (@(posedge clk) (Assert_Grant_ && !(Assert_Request_)) |-> nexttime(!(Assert_Grant_)));Specification, in LOGOS
SystemVerilog assertion
Reset behavior
assert property (@(posedge clk) low_reset_n_ |-> nexttime(high_puc_rst_));Specification, in LOGOS
SystemVerilog assertion
Liveness, emitted as a cover rather than an assert
cover property (@(posedge clk) s_eventually(Assert_Grant_));The symbol names are the part a verification engineer asks about first. Assert_irq_ rather than irq is deliberate. The assertion and the parsed specification are emitted into one symbol table, so a solver can be asked whether the two mean the same thing. That question is the reason the pipeline exists, and an assertion using raw RTL identifiers would have nothing to compare against.
100 of the 101 sentences in the hardware corpus produce a parseable, non-degenerate assertion, measured by running the corpus through the synthesizer. 68 of the 101 produce one from concrete signal names alone, and the remaining 33 come from universally quantified English such as "every request", where a bound variable survives into the assertion for a human to bind. The output is a set of properties to check against RTL, produced from a formally parsed specification rather than from a language model.
Source: The compiler, the hardware test corpus, and the synthesizer, on GitHub(opens in a new tab)
Three ways in, in the order most people should take them. This is a signpost rather than a getting started guide.
The browser playground above runs LOGOS with nothing installed. Start here.
The build tool installs in one line.
curl -fsSL https://logicaffeine.com/install.sh | shThe compiler and the hardware test corpus are at github.com/Brahmastra-Labs/logicaffeine, and the crates are published on crates.io.
What does the language let you prove?