The crates the toolchain is made of

Turns English sentences into first order logic through a lexer, a parser and a semantic pipeline.

Holds the English vocabulary types and looks words up for the translator.

Runs the analysis and optimization passes, then executes a program through the interpreter, the bytecode virtual machine, or generated Rust, C and SystemVerilog.

A small trusted Calculus of Constructions type checker that every other component re-checks its results against. The kernel has no path to the lexicon, so it never sees an English word.

Searches for proofs by backward chaining, certifies what it finds into kernel terms, and offers a hint when the search stalls.

Encodes a verification IR into the Z3 SMT solver to decide validity, equivalence and temporal properties.

Proves the Rust the compiler emits behaves the same as the LOGOS source that produced it.

The low level JIT layer: executable memory pages, prebaked machine code stencils, and an x86-64 code generator. On every other target the crate compiles to nothing and the bytecode machine runs instead.

Connects the stencil JIT to the bytecode virtual machine, so a hot loop upgrades to native code without being rewritten. Native targets only.

Deterministic concurrency: a scheduler, channels, select, a logical clock, and seed and trace replay. A run is a function of the program and the seed, and replays bit for bit, which spares you the bug that only happens on the third Tuesday under load.

The foundation layer: arena allocation, string interning, source spans, exact numbers, units, money, time, UUIDs and hashes.

The runtime value types, and the eight conflict free replicated types that converge without coordination. WASM safe, with no IO of its own.

Console, clock, filesystem and networking, plus the post-quantum cryptography primitives.

The largo command line tool, which creates, builds, runs, proves, formats and publishes LOGOS projects.

The language server that gives an editor live diagnostics, completion, hover and refactoring.