tiny-XOR-verified

Formally verified XOR gate. Two-layer threshold network computing exclusive or with 100% accuracy.

Architecture

Component	Value
Inputs	2
Outputs	1
Neurons	3 (2 hidden, 1 output)
Layers	2
Parameters	9
Layer 1, Neuron 1 (OR)
Weights	[1, 1]
Bias	-1
Layer 1, Neuron 2 (NAND)
Weights	[-1, -1]
Bias	1
Layer 2 (AND)
Weights	[1, 1]
Bias	-2
Activation	Heaviside step (all layers)

Key Properties

• 100% accuracy (4/4 inputs correct)
• Coq-proven correctness
• Minimal 2-layer architecture (XOR is not linearly separable)
• Integer weights
• Commutative: XOR(x,y) = XOR(y,x)
• Associative: XOR(x,XOR(y,z)) = XOR(XOR(x,y),z)
• Self-inverse: XOR(x,XOR(x,y)) = y

Why 2 Layers?

XOR is the classic example of a function that is not linearly separable - a single threshold neuron cannot compute it. This network uses the minimal architecture:

Layer 1: Compute OR and NAND in parallel Layer 2: Compute AND of results

This implements: XOR(x,y) = AND(OR(x,y), NAND(x,y))

Usage

import torch
from safetensors.torch import load_file

weights = load_file('xor.safetensors')

def xor_gate(x, y):
    inputs = torch.tensor([float(x), float(y)])

    # Layer 1: OR and NAND
    or_sum = (inputs * weights['layer1.neuron1.weight']).sum() + weights['layer1.neuron1.bias']
    or_out = int(or_sum >= 0)

    nand_sum = (inputs * weights['layer1.neuron2.weight']).sum() + weights['layer1.neuron2.bias']
    nand_out = int(nand_sum >= 0)

    # Layer 2: AND
    layer1_outs = torch.tensor([float(or_out), float(nand_out)])
    and_sum = (layer1_outs * weights['layer2.weight']).sum() + weights['layer2.bias']
    return int(and_sum >= 0)

# Test
print(xor_gate(0, 0))  # 0
print(xor_gate(0, 1))  # 1
print(xor_gate(1, 0))  # 1
print(xor_gate(1, 1))  # 0

Verification

Coq Theorem:

Theorem xor_correct : forall x y, xor_circuit x y = xorb x y.

Proven axiom-free with properties:

• Commutativity
• Associativity
• Identity (XOR with false)
• Complement (XOR with true gives NOT)
• Nilpotence (XOR with itself gives false)
• Involution (XOR is self-inverse)

Full proof: coq-circuits/Boolean/XOR.v

Circuit Operation

Input (x,y)	OR	NAND	AND(OR,NAND)	XOR
(0,0)	0	1	0	0
(0,1)	1	1	1	1
(1,0)	1	1	1	1
(1,1)	1	0	0	0

XOR outputs true when inputs differ.

Citation

@software{tiny_xor_prover_2025,
  title={tiny-XOR-verified: Formally Verified XOR Gate},
  author={Norton, Charles},
  url={https://huggingface.co/phanerozoic/tiny-XOR-verified},
  year={2025}
}