LOGOS is released under the Business Source License 1.1. The source code is publicly available, and the software is free to use for individuals and small teams.

Free Use

You may use LOGOS at no cost if you are:

An individual
A university or educational institution
An organization with fewer than 25 employees

Commercial License Required

If your organization has 25 or more employees and you wish to use LOGOS as a Logic Service, a commercial license is required. Contact us to discuss licensing options for your organization.

Open Source Transition

On December 24, 2029, LOGOS will transition to the MIT License, making it fully open source.

What You Get

One language for code, logic, math, hardware verification, and distributed systems

English-Native Programming

Programs, proofs, and logic in plain English
Compiles to native Rust via LLVM
Ownership and borrowing in natural language

Formal Logic & Semantics

English → First-Order Logic transpilation
Quantifier disambiguation with all scope readings
Discourse tracking and anaphora resolution

Type Theory & Proofs

Calculus of Constructions with dependent types
Automated tactics: induction, ring, simp, omega
Kernel-verified proof certification

Hardware Verification & SVA

English specs to SystemVerilog Assertions
FOL-to-SVA synthesis via Futamura projections
Bounded model checking and CEGAR refinement
AXI4, APB, and handshake protocol templates

Distributed Systems & CRDTs

GCounter, PNCounter, ORSet, RGA, ORMap
libp2p networking with GossipSub
Automatic merge and eventual consistency

Security & Concurrency

Capability-based access control
CSP channels and structured concurrency
Arena allocation — no garbage collector

Verification & Tooling

Z3 SMT solver for static verification
Interactive Studio with live compilation
CLI tool (largo) and WASM runtime