---
license: mit
tags:
- formal-verification
- coq
- threshold-logic
- neuromorphic
- multi-layer
---

# 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

```python
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**:
```coq
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](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/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

```bibtex
@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}
}
```