Navigation
Syntax Guide
Learn Logic
StudioCratesRoadmapContactNewsBenchmarks
ProfileGitHub
Free for individuals • Commercial licenses available

Debug Your Thoughts.

Write Code, Logic, and Math in plain English. LOGOS compiles your words into programs, proofs, and formal systems — no symbols required.

Students, engineers, researchers, and attorneys — anyone who thinks for a living.

Rust-Powered 🦀WASM ReadyMarkdown SourceProof-Checked
View more...
FILES
hello-world.logos
fibonacci.logos
counters.logos
tally.logos
View more...
hello-world.logos λ
OUTPUT
Click Run to see output

How it works

Three modes. One language: English.

λ

Write a program

Let x be 10. Show x + 5.
15

Type readable definitions. Get compiled programs — Rust under the hood, English on the surface.

Formalize an argument

Every cat sleeps.
∀x(Cat(x) → Sleep(x))

Turn plain language into First-Order Logic. Every reading surfaced — no guessing.

π

Prove a theorem

Theorem: ∀n, n + 0 = n.
Proof: by induction. ✓

Define types, state theorems, and prove them with automated tactics.

Hello World in LOGOS

hello-world.logos
# Hello, LOGOS -- A program is numbered sections of English sentences. ## Main Let greeting be "Hello, LOGOS!". Show greeting. Let x be 10. Let y be 20. Show "{x} + {y} = {x + y}".
Output
Click Run to see output

Compiles to a native binary via Rust. Zero runtime overhead.

What you get

LOGICAFFEINE translates intuition into structure — so you can test it, teach it, or ship it.

Instant Transpilation

Type normal English. Get programs, logic, and math output in seconds — readable enough to learn from, strict enough to verify.

Socratic Tutor

When your statement is ambiguous, the tutor asks questions that force clarity instead of guessing.

Assumption Surfacing

Reveal missing premises, hidden quantifiers, and scope mistakes — the usual sources of bad arguments.

Consistency & Validity Checks

Spot contradictions, invalid inferences, and rule collisions across Code, Logic, and Math modes — before they hit production or policy.

Studio + Curriculum

Explore freely in Studio, then build mastery in Learn with structured lessons and practice.

Commercial-Ready

Licensing options for teams and enterprises — with a path toward governance and controlled deployments.

Security & Policies

Capability-based security with policy blocks. Define who can do what in plain English.

Policy Blocks

Define security rules as readable policy sections. Who can access what — stated plainly.

Capabilities

Role-based access control expressed in English. No annotation soup.

Check Guards

Runtime guard checks that enforce your policies. "Check that the user is admin."

Predicates

Define custom predicates: "A User is admin if the user's role equals 'admin'."

Policy → Compiled Output
LOGOS Policy
## Definition
A User has:
    a role: 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 u is admin.
Show "Access granted".
Compiled Output
struct User {
    role: String,
}

impl User {
    fn is_admin(&self) -> bool {
        self.role == "admin"
    }
}

fn main() {
    let u = User { role: "admin".into() };
    assert!(u.is_admin());
    println!("Access granted");
}

For people who want their reasoning to survive contact with reality.

Students & Educators

Teach formal reasoning with feedback that's immediate, concrete, and harder to game than multiple choice.

Law, Policy, Compliance

Translate policy language into verifiable rules. Reduce ambiguity. Make reviews faster and safer.

Engineering & Research

Specify systems, constraints, and invariants in a form you can test — without forcing everyone into formal syntax.

How LOGOS Compares

A new approach to formal reasoning.

Feature
LOGOS
Python
Lean 4
Rust
Elixir
Syntax
English prose
Symbols
Lean DSL
Symbols
Symbols
File Format
Markdown (.md)
.py
.lean
.rs
.ex
Performance
Native (via Rust)
Interpreted
Native
Native
BEAM VM
Proofs
Built-in
None
Required
Optional
None
Memory
Ownership (English)
GC
GC
Ownership
GC

FAQ

Common questions about LOGICAFFEINE.

Is it really free?
Yes — free for individuals, universities, and teams under 25 people. For commercial licensing, contact us.
Do I need to know logic already?
No. Start in Learn. The system introduces concepts progressively and uses examples to teach scope, quantifiers, and structure.
Is this an AI that "guesses"?
The goal is the opposite: to force explicit structure. When language is ambiguous, the tutor prompts clarifying questions.
Where do I begin?
If you want speed, open Studio. If you want mastery, Start Learning and follow the lessons.
What is LOGOS written in?
Rust. The entire transpiler, parser, and runtime are written in Rust for maximum performance and safety.
How fast is it?
Native speed. LOGOS compiles to Rust, which then compiles via LLVM to optimized machine code. Zero interpreter overhead.

Make your reasoning impossible to ignore.

Start with the Curriculum, or explore any mode in the Studio. Code, Logic, Math — your call.