Install it

curl -fsSL https://logicaffeine.com/install.sh | sh

Prebuilt largo binaries for Linux/macOS (x64 + arm64) and Windows x64

(irm https://logicaffeine.com/install.ps1 | iex), SHA-256-verified, no toolchain, no sudo.

Add --full for the flavor with Z3 static verification bundled. This release also widens

the CLI itself: largo repl (interactive imperative + English→FOL sessions), largo logic,

largo prove, largo sat, largo fmt, largo emit, largo doc, largo add/remove,

shell completions, and live cargo output during builds.

The editor teaches you to code

The language server grew from 14 to 20 providers and became genuinely socratic. Hover,

completion documentation, and the REPL's new :explain all render one lesson table

(logicaffeine_language::teach): a plain-sentence explanation, a runnable example, and a

guiding question for every taught keyword, every ## block type, and the built-in types.

All 39 parse-error explanations follow the contract *what happened → why → a guiding

question → the next step*, and all 158 stdlib prelude definitions carry literate ## Note

docs that surface in hover, completion, and signature help — while the runtime prelude

strips them byte-exactly. Diagnostics deepened the same way: the typechecker, ownership,

and escape checkers report every failing statement on its own span with cause links

("was given away here" points at the exact Give), and on save the generated Rust runs

through cargo check with every rustc finding translated back to English on user-source

spans — English with a borrow checker. Semantic highlighting is resolution-aware,

references and rename cross files, and the workspace indexes every .lg/.md for

symbols and goto-definition.

The VSCode extension ships with this release as per-platform VSIXs attached to the GitHub

release (marketplace listings come later): each bundles one server binary, a TextMate

grammar rewritten against the real surface and locked to the quickguide by ratchet, and

run/verify/prove code lenses wired to largo — behind a CI install gate that installs the

actual packaged VSIX into a real VSCode on three OSes and asserts diagnostics round-trip

before anything releases.

EXODIA — the native execution tier

The English-like language no longer runs only on a tree-walking interpreter. It now executes on a register bytecode VM with a copy-and-patch JIT on top, and the JIT carries a contiguous register-allocating x86-64 backend (EXODIA). On the interpreter benchmark suite the VM+JIT geomean moves from 3.34x to roughly 1.0x against Node/V8, with 12 of 31 programs faster than V8.

The bytecode VM

A register bytecode VM in logicaffeine-compile is the live engine for both the synchronous native path and WASM. It is corpus-certified against the tree-walking interpreter as a shadow oracle, and its Int fast paths are bit-identical to the kernel by the wrapping-i64 spec, pinned by an edge-grid differential. Release-bench on a representative program: tree-walker 70ms, VM 16.6ms (4.2x), tiered 6.0ms (11.7x).

The tier-up seam

Hot functions compile per call with argument guards and kind-inference (parameters Int, comparisons Bool). Hot Main loops region-tier through an OSR-lite path with incoming-dead analysis and per-entry guards, so loops that never reach a function-level JIT still run native. Anything outside the supported integer/float subset fails closed back to bytecode — the deopt contract — so correctness never depends on the JIT accepting a given program.

logicaffeine-forge — the executable-memory layer and EXODIA backend

logicaffeine-forge is the foundation the copy-and-patch JIT builds on. JitPage allocates page-aligned memory, copies machine code into it, flips the page to executable, and hands back a callable function pointer. At runtime, compiling a function is memcpy(stencil bytes) followed by patching relocations. On top of the stencil runtime sits the J1 micro-op compiler and the EXODIA contiguous register-allocating region/function x86-64 codegen tier (regalloc.rs, x64asm.rs), which replaces per-stencil-piece dispatch with allocated registers and contiguous code.

Platform-correct W^X

Write-xor-execute is handled per platform: on macOS/aarch64 (Apple Silicon) via mmap(MAP_JIT) with per-thread pthread_jit_write_protect_np toggling and a mandatory sys_icache_invalidate; on other Unix via mmap(RW) then mprotect(RX) with an I-cache flush on aarch64 Linux; on Windows via VirtualAlloc then VirtualProtect then FlushInstructionCache. The JIT is native-only; the browser continues to run the bytecode VM.

logicaffeine-jit — the native tier

logicaffeine-jit is the seam between the VM and the forge. ForgeTier translates VM bytecode into the forge's MicroOp subset for both whole functions (ChainFn) and hot loop regions (RegionChain), and install() makes the tier process-wide — largo installs it at startup. The crate is #![cfg(not(target_arch = "wasm32"))], so WASM builds it to nothing.

logicaffeine-synth — offline proof tooling for the stencils

logicaffeine-synth (EXODIA Phase 2) proves the JIT's integer micro-operations correct offline. It carries Z3 specifications for the micro-ops over 64-bit bitvectors, satisfiability and algebraic-property gates, and a three-way witness harness that runs Z3-chosen inputs through the real compiled stencil. It runs at development and CI time and never on the production runtime path.

logicaffeine-runtime — deterministic concurrency

logicaffeine-runtime is the operational semantics of concurrency for the interpreter and VM: the task scheduler, FIFO channels, Select, a logical-clock timer wheel, and the seed/trace machinery. A run is a deterministic function of (program, seed) and replays bit-for-bit from (program, trace) through a single Chooser::decide choke point. It is pure std, WASM-safe, tokio-free, and by charter never linked into AOT-compiled binaries — the compiled path uses logicaffeine-system instead.

logicaffeine-tv — translation validation

logicaffeine-tv proves that the Rust emitted by the compiler is observationally equivalent to its LOGOS source, per compile, by symbolically executing both sides into the shared logicaffeine-verify domain and discharging the equivalence with Z3. check_encoder_sound cross-validates the LOGOS encoder against the tree-walking interpreter — the trust anchor that catches a buggy encoder rather than letting it prove two wrong things equal. This is translation validation at rung 3–4: the trust boundary is the encoders, Z3, and rustc.

Verified arithmetic and proof work

The kernel gains proof-producing arithmetic (arith.rs) with certificates, the proof engine gains modal translation and independent verification, and the solver stack adds a CDCL core with an incremental grid solver, grounding, and trust-tiers.

Strict whole-input parsing

compile() now rejects parses that strand tokens (TrailingTokens) instead of silently dropping meaning — for a hardware spec, a dropped until AWREADY clause is a wrong assertion, not a style issue. The parser gains the coverage to match: noun-noun compound heads, possessive heads over ambiguous noun/verb words, trailing temporal operators inside If-consequents, postposed when-clauses, and quantified or cardinal objects under modals and under never.

Also in this release

The general CDCL solver dropped its per-conflict allocations (~30% faster on random 3-SAT,

byte-identical search) and decides binary clauses straight from the watch lists; the

/benchmarks solver section now shows our certified proof size beside every winning family

and adds CaDiCaL and CryptoMiniSat to the field. The site itself is prerendered (real

per-route HTML with per-page metadata for crawlers and link unfurlers) and code-split — a

first visit downloads ~683 KB gzipped instead of 3.9 MB. And no LOGOS program can

stack-overflow the compiler anymore: a 5,000-term expression chain gets a graceful

diagnostic teaching both fixes, on every surface from the CLI to the web Studio.

Published

logicaffeine-forge, logicaffeine-jit and logicaffeine-runtime join the lockstep version line and the crates.io publish pipeline, shipping and versioning alongside the rest of the workspace.