tiny-HalfAdder-verified

Formally verified half adder circuit. Adds two 1-bit inputs, producing sum and carry outputs with 100% accuracy.

Architecture

Component	Value
Inputs	2 (a, b)
Outputs	2 (sum, carry)
Neurons	4 (3 for XOR + 1 for AND)
Parameters	12
Depth	2 layers
Activation	Heaviside step

Key Properties

• 100% accuracy (4/4 input combinations correct)
• Coq-proven correctness
• Compositional design: XOR for sum, AND for carry
• Building block for multi-bit adders
• Compatible with neuromorphic hardware

Circuit Design

Sum output: a XOR b

• 2-layer XOR network
• Layer 1: OR and NAND neurons in parallel
• Layer 2: AND neuron
• 3 neurons, 9 parameters

Carry output: a AND b

• Single AND neuron
• 1 neuron, 3 parameters

Both outputs computed in parallel with max depth of 2 layers.

Usage

import torch
from safetensors.torch import load_file

weights = load_file('halfadder.safetensors')

def heaviside(x):
    return int(x >= 0)

def half_adder(a, b):
    inputs = torch.tensor([float(a), float(b)])

    # Compute sum (XOR)
    or_out = heaviside((inputs * weights['sum.layer1.or.weight']).sum() +
                       weights['sum.layer1.or.bias'])
    nand_out = heaviside((inputs * weights['sum.layer1.nand.weight']).sum() +
                         weights['sum.layer1.nand.bias'])
    layer1_outs = torch.tensor([float(or_out), float(nand_out)])
    sum_out = heaviside((layer1_outs * weights['sum.layer2.weight']).sum() +
                        weights['sum.layer2.bias'])

    # Compute carry (AND)
    carry_out = heaviside((inputs * weights['carry.weight']).sum() +
                          weights['carry.bias'])

    return sum_out, carry_out

# Test
print(half_adder(0, 0))  # (0, 0)
print(half_adder(0, 1))  # (1, 0)
print(half_adder(1, 0))  # (1, 0)
print(half_adder(1, 1))  # (0, 1) - sum=0, carry=1

Truth Table

a	b	sum	carry
0	0	0	0
0	1	1	0
1	0	1	0
1	1	0	1

Verification

Coq Theorem:

Theorem half_adder_correct : forall a b,
  half_adder a b = half_adder_spec a b.

Where half_adder_spec is defined as:

Definition half_adder_spec (a b : bool) : bool * bool :=
  (xorb a b, andb a b).

Proven axiom-free with verified properties:

• Commutativity: half_adder a b = half_adder b a
• Identity: half_adder false a = (a, false)
• Self-addition: half_adder a a = (false, a)

Full proof: coq-circuits/Arithmetic/HalfAdder.v

Applications

• Building block for full adders
• Component of ripple-carry adders
• Base unit for multi-bit arithmetic
• Educational hardware design

Citation

@software{tiny_halfadder_verified_2025,
  title={tiny-HalfAdder-verified: Formally Verified Half Adder},
  author={Norton, Charles},
  url={https://huggingface.co/phanerozoic/tiny-HalfAdder-verified},
  year={2025}
}