From English sentences to a verified compilation stack: first-order logic, a native execution tier, hardware model checking, and a kernel-certified proof core.

Featured milestones

Core TranspilerComplete

English to first-order logic. A two-stage lexer with morphology and lexicon lookup, a recursive-descent parser over an arena AST with Discourse Representation Structures, Montague-style lambda semantics, and a Neo-Davidsonian event-semantics transpiler. Quantifier scope, relative clauses, negation, and modality, rendered to a collapsed SimpleFOL or full Unicode with event variables.

Two-stage lexerRecursive-descent parserDRS discourse trackingLambda semanticsQuantifier scopeEvent semanticsUnicode / ASCII / LaTeX

"Every user who has a key enters the room."

↓

∀x(((User(x) ∧ ∃y((Key(y) ∧ Have(x, y)))) → Enter(x, Room)))

Web PlatformComplete

A Dioxus/WASM front end: a structured Learn curriculum, a free-form Studio for English-to-FOL and compilation, and the published benchmark and release-notes pages. The browser runs the bytecode VM; native tiers fall back to it under WASM.

Dioxus WASMLearn curriculumStudioBenchmarks pageRelease notes

Imperative LanguageComplete

LOGOS as a general-purpose language: functions, structs, enums, pattern matching, a standard library, and I/O, parsed in the imperative mode of the same front end. Codegen emits Rust source plus C, Python, and TypeScript FFI bindings.

FunctionsStructs & enumsPattern matchingStandard libraryC / Python / TS FFI

## To greet (name: Text) -> Text: Return "Hello, " combined with name.

↓

Rust

#[inline] fn greet(name: String) -> String { return format!("{}{}", "Hello, ", name); }

Type SystemComplete

Refinement types, generics, sum types, and type inference, with constraints expressed in English. Escape, ownership, and liveness analysis run ahead of codegen and reject use-after-move.

Refinement typesGenericsSum typesType inferenceOwnership & escape analysis

## Main Let age: Int where it > 0 be 25. Show age.

↓

Rust

let age: i64 = 25; debug_assert!(age > 0); show(&age);

Concurrency & ActorsComplete

Channels, agents, structured parallelism, and select with timeout, lowering to async/await. Go-style concurrency written in English.

ChannelsAgentsStructured parallelismSelect with timeoutasync / await

## To worker: Show "worker done". ## Main Launch a task to worker. Show "main continues".

↓

Rust

#[tokio::main] async fn main() { tokio::spawn(async move { worker(); }); show(&String::from("main continues")); }

Distributed SystemsComplete

CRDTs, P2P gossip, and persistent storage for local-first applications with automatic conflict resolution.

CRDTsP2P gossipPersistenceConvergent countersAutomatic merge

## Definition A Counter is Shared and has: points: ConvergentCount. ## Main Let mutable c be a new Counter. Increase c's points by 10. Show c's points.

↓

Rust

pub struct Counter { pub points: GCounter, } impl Merge for Counter { fn merge(&mut self, other: &Self) { self.points.merge(&other.points); } }

Security & PoliciesComplete

Capability-based security with policy blocks and check guards: who can do what, stated in English and lowered to predicate checks.

Policy blocksCapabilitiesCheck guardsPredicates

## Definition A User has: a role, which is Text. ## Policy A User is admin if the user's role equals "admin". ## Main Let u be a new User with role "admin". Check that the u is admin. Show "passed".

↓

Rust

impl User { pub fn is_admin(&self) -> bool { self.role == "admin" } } // at the check site: if !u.is_admin() { panic_with("Security Check Failed: u is admin"); }

Proof AssistantComplete

A Calculus of Inductive Constructions kernel as the trusted core: a bidirectional type checker over which propositions are types and proofs are terms. A backward-chaining search engine proposes derivations; the kernel re-checks every one. Certificate-producing arithmetic, a finite-domain grid solver, and a CDCL SAT core with an independent RUP checker sit outside the trusted base; an optional Z3 oracle never bypasses kernel certification.

CIC kernelBackward-chaining searchKernel-certified proofsCertificate-producing arithmeticCDCL + RUPGrid solverZ3 oracle (optional)

## Main Let x be 10. While x > 0 (decreasing x): Set x to x - 1.

↓

Rust

// `decreasing x` proves the metric falls each iteration let mut x = 10; while x > 0 { x = x - 1; }

Native Compilation TierComplete

Three execution tiers below the front end: generated Rust source, a register-bytecode VM with optimizer (oracle facts, GVN, LICM, DCE, scalarization, loop-split), and a native AOT/JIT path. The VM profiles hot integer/float regions and recursive functions and tiers them down through a copy-and-patch JIT — stencils stamped out by memcpy and patched at relocations — to EXODIA, a contiguous register-allocating x86-64 backend. Anything outside the supported subset declines and stays on bytecode (the deopt contract). The benchmark suite measures the codegen path against ten languages with hyperfine; runtime parity with V8/Node, and head-to-head comparison against C.

Bytecode VMOptimizer (GVN / LICM / DCE)Copy-and-patch JITEXODIA register-allocating x86-64Auto-memoization10-language benchmarksV8 / Node parity

## Main Let total be 0. Repeat for i from 1 to 100: Set total to total + i. Show total.

↓

Rust

let mut total = 0; for i in 1..=100 { total = total + i; } show(&total);

Hardware VerificationComplete

SystemVerilog Assertions synthesized from English specifications, with IEEE 1800-2017 and 1800-2023 coverage: property connectives, LTL temporal operators, sequence composition, abort operators, and real-valued checker variables. The model-checking engine runs bounded model checking, IC3/PDR, k-induction, Craig interpolation, and predicate-abstraction CEGAR over Z3's bitvector theory, with vacuity analysis, assume-guarantee composition, and SMT-LIB2 export.

English → SVAIEEE 1800-2017 / 1800-2023Bounded model checkingIC3 / PDRK-inductionCraig interpolationBitvector theory

Always, if req holds, then eventually ack holds.

↓

SVA

assert property (@(posedge clk) Hold_req_ |-> s_eventually(Hold_ack_));

Translation ValidationIn Progress

Proving the compiler's output matches its input. The logicaffeine-tv crate symbolically executes the LOGOS source into the shared verification domain and discharges equivalence with Z3 (rung 3–4: the trust boundary is the encoder, Z3, and rustc). The source-side executor and its meta-soundness oracle — cross-validating the encoder against the tree-walking interpreter — are in place; the Rust-emitter-side executor that closes full source-to-Rust equivalence is the remaining work.

Symbolic executionZ3 equivalenceEncoder soundness oracleOut-of-fragment exclusion

Quantum BackendPlanned

A Cirq v2 backend mirroring the SVA architecture: 17 sprints, 314 planned tests across 13 files, taking the same FOL-to-target synthesis path to quantum circuits.

Cirq v2Circuit synthesisFOL-to-quantum

SiliconPlanned

The LOGOS chip. The AOT tier already runs at 2.6× the speed of C — faster than C, C++, Rust, and Zig, the fastest language in the suite — so the general-purpose CPU is tapped out, and the next order of magnitude leaves it for a full-custom HPC SoC. The register-VM ops become a native ISA, the copy-and-patch stencils become hardwired functional units, and the Jones-optimal Futamura specializer configures a spatial dataflow fabric: implementation is a partial evaluation of the specification, so the compiled program *is* the circuit, correct by construction. Because that residual is a statically-known dataflow, there is no speculative cache hierarchy to pay for — memory is scheduled onto scratchpads, not guessed. The crypto and codec kernels already written in Logos — Keccak-f[1600], the ML-KEM / ML-DSA NTT, SHA-3, group-varint — drop onto dedicated accelerators for line-rate post-quantum crypto and serialization. And the goal is not only speed but power: with no cache hierarchy and no speculation to feed, the fabric spends energy only on the computation that runs — driving toward the Landauer limit, and, through reversible logic, past it. Because the same substrate that verifies English specs emits SVA, extracts Verilog, and proves BitVec(n) properties across every bus width, the chip is designed and formally proven in Logos itself: self-hosting, zero-defect silicon.

LOGOS-ISA coresStencils → functional unitsFutamura dataflow fabricNo cache hierarchyLow power → LandauerPQC acceleratorsSelf-verified RTL