tiny-AND-verified

Formally verified AND gate. Single threshold neuron computing conjunction with 100% accuracy.

Architecture

Component	Value
Inputs	2
Outputs	1
Neurons	1
Parameters	3
Weights	[1, 1]
Bias	-2
Activation	Heaviside step

Key Properties

• 100% accuracy (4/4 inputs correct)
• Coq-proven correctness
• Single threshold neuron
• Integer weights
• Commutative: AND(x,y) = AND(y,x)
• Associative: AND(x,AND(y,z)) = AND(AND(x,y),z)
• Idempotent: AND(x,x) = x

Usage

import torch
from safetensors.torch import load_file

weights = load_file('model.safetensors')

def and_gate(x, y):
    inputs = torch.tensor([float(x), float(y)])
    weighted_sum = (inputs * weights['weight']).sum() + weights['bias']
    return int(weighted_sum >= 0)

print(and_gate(0, 0))  # 0
print(and_gate(0, 1))  # 0
print(and_gate(1, 0))  # 0
print(and_gate(1, 1))  # 1

Or use the provided model class:

from model import ThresholdAND

model = ThresholdAND.from_safetensors('model.safetensors')
print(model(1, 1))  # 1

Verification

Coq Theorem:

Theorem and_correct : forall x y, and_circuit x y = andb x y.

Proven axiom-free with properties:

• Commutativity
• Associativity
• Identity (AND with true)
• Absorption (AND with false)
• Idempotence

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

Circuit Operation

Input combination produces weighted sum:

• (0,0): 01 + 01 - 2 = -2 < 0 -> 0
• (0,1): 01 + 11 - 2 = -1 < 0 -> 0
• (1,0): 11 + 01 - 2 = -1 < 0 -> 0
• (1,1): 11 + 11 - 2 = 0 >= 0 -> 1

Requires both inputs to reach threshold.

Files

tiny-AND-verified/
├── model.safetensors  # Network weights (3 params)
├── model.py           # Inference code
├── config.json        # Model metadata
└── README.md          # This file

Citation

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

License

MIT