logos

A Lean-style proof kernel for Python

logos lets you prove properties of your Python code using a composable tactic system backed by a small trusted kernel. Write propositions as Python expressions, then discharge them with tactics — or with an LLM oracle whose output the kernel validates.

import logos
import logos.tactics as t

# Declare a theorem
@logos.theorem
def add_comm(x: int, y: int):
    return x + y == y + x

# Attach proof and validate
logos.check(add_comm.proof(t.intro("x", "y"), t.ring()))
print("Proved: addition is commutative")
Proved: addition is commutative

If the proof is wrong, LogosProofError is raised immediately. If it passes, add_comm.certified is True and you can build on it.

How it works

logos follows Lean’s architecture:

User layer       @logos.define · @logos.theorem · operator expressions
                           ↓
Tactic layer     ring · linarith · intro · cases · ...  (untrusted)
                           ↓
Proof terms      Refl · Trans · Subst · ForallIntro · ...
                           ↓
Kernel (~200 ln) infer() / check()  ←  the only trusted code

The kernel is the only trusted code (~200 lines). Tactics are arbitrary Python that produce proof terms — the kernel checks every term structurally. A tactic can even call an LLM: if the LLM produces an invalid proof, the kernel rejects it.

Install

pip install logos-ai

A taste of what you can prove

import logos
import logos.tactics as t

# 1. Define a function symbolically
@logos.define
def double(x: int):
    return x + x

# 2. Calling with a real value evaluates normally
assert double(7) == 14

# 3. Prove a property: unfold the definition, then ring arithmetic
@logos.theorem
def double_is_2x(x: int):
    return double(x) == logos.lit(2) * x

logos.check(double_is_2x.proof(t.intro("x"), t.unfold(double), t.ring()))
print("Proved: double(x) = 2x")

# 4. Linear arithmetic
@logos.theorem
def double_exceeds_x(x: int):
    return (x > logos.lit(0)) >> (double(x) > x)

logos.check(double_exceeds_x.proof(t.intro("x", "h"), t.unfold(double), t.linarith()))
print("Proved: x > 0 → double(x) > x")
Proved: double(x) = 2x
Proved: x > 0 → double(x) > x

Next steps