---
license: mit
tags:
- formal-verification
- coq
- threshold-logic
- neuromorphic
- arithmetic
- adder
---

# tiny-FullAdder-verified

Formally verified full adder circuit. Adds three 1-bit inputs (a, b, carry_in), producing sum and carry_out outputs with 100% accuracy.

## Architecture

| Component | Value |
|-----------|-------|
| Inputs | 3 (a, b, carry_in) |
| Outputs | 2 (sum, carry_out) |
| Neurons | 9 (2 HalfAdders + OR) |
| Parameters | 27 |
| Depth | 3 layers |
| Activation | Heaviside step |

## Key Properties

- 100% accuracy (8/8 input combinations correct)
- Coq-proven correctness
- Compositional design: 2 HalfAdders + OR gate
- Building block for ripple-carry adders
- Compatible with neuromorphic hardware

## Circuit Design

Composed from two half adders and an OR gate:

```
HalfAdder1: (a, b) -> (s1, c1)
HalfAdder2: (s1, carry_in) -> (sum, c2)
carry_out = OR(c1, c2)
```

**Components:**
- 2 HalfAdders: 4 neurons each (XOR + AND)
- 1 OR gate: 1 neuron
- Total: 9 neurons, 27 parameters, depth 3

## Usage

```python
import torch
from safetensors.torch import load_file

weights = load_file('fulladder.safetensors')

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

def full_adder(a, b, carry_in):
    # HalfAdder1: (a, b) -> (s1, c1)
    inputs_ha1 = torch.tensor([float(a), float(b)])

    or_out1 = heaviside((inputs_ha1 * weights['ha1.sum.layer1.or.weight']).sum() +
                        weights['ha1.sum.layer1.or.bias'])
    nand_out1 = heaviside((inputs_ha1 * weights['ha1.sum.layer1.nand.weight']).sum() +
                          weights['ha1.sum.layer1.nand.bias'])
    layer1_outs1 = torch.tensor([float(or_out1), float(nand_out1)])
    s1 = heaviside((layer1_outs1 * weights['ha1.sum.layer2.weight']).sum() +
                   weights['ha1.sum.layer2.bias'])
    c1 = heaviside((inputs_ha1 * weights['ha1.carry.weight']).sum() +
                   weights['ha1.carry.bias'])

    # HalfAdder2: (s1, carry_in) -> (sum, c2)
    inputs_ha2 = torch.tensor([float(s1), float(carry_in)])

    or_out2 = heaviside((inputs_ha2 * weights['ha2.sum.layer1.or.weight']).sum() +
                        weights['ha2.sum.layer1.or.bias'])
    nand_out2 = heaviside((inputs_ha2 * weights['ha2.sum.layer1.nand.weight']).sum() +
                          weights['ha2.sum.layer1.nand.bias'])
    layer1_outs2 = torch.tensor([float(or_out2), float(nand_out2)])
    sum_out = heaviside((layer1_outs2 * weights['ha2.sum.layer2.weight']).sum() +
                        weights['ha2.sum.layer2.bias'])
    c2 = heaviside((inputs_ha2 * weights['ha2.carry.weight']).sum() +
                   weights['ha2.carry.bias'])

    # Carry out: OR(c1, c2)
    carry_inputs = torch.tensor([float(c1), float(c2)])
    carry_out = heaviside((carry_inputs * weights['carry_or.weight']).sum() +
                          weights['carry_or.bias'])

    return sum_out, carry_out

# Test
print(full_adder(0, 0, 0))  # (0, 0)
print(full_adder(1, 1, 0))  # (0, 1) - 1+1=2, sum=0, carry=1
print(full_adder(1, 1, 1))  # (1, 1) - 1+1+1=3, sum=1, carry=1
```

## Truth Table

| a | b | cin | sum | cout |
|---|---|-----|-----|------|
| 0 | 0 | 0   | 0   | 0    |
| 0 | 0 | 1   | 1   | 0    |
| 0 | 1 | 0   | 1   | 0    |
| 0 | 1 | 1   | 0   | 1    |
| 1 | 0 | 0   | 1   | 0    |
| 1 | 0 | 1   | 0   | 1    |
| 1 | 1 | 0   | 0   | 1    |
| 1 | 1 | 1   | 1   | 1    |

## Verification

**Coq Theorem**:
```coq
Theorem full_adder_correct : forall a b c,
  full_adder a b c = full_adder_spec a b c.
```

Where `full_adder_spec` computes:
- `sum = a XOR b XOR c`
- `carry_out = (a AND b) OR (c AND (a XOR b))`

Proven axiom-free with verified properties:
- Commutativity in first two arguments
- Equivalence to half adder when carry_in = false
- Exhaustive correctness on all 8 input combinations

Full proof: [coq-circuits/Arithmetic/FullAdder.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Arithmetic/FullAdder.v)

## Applications

- Building block for multi-bit ripple-carry adders
- Component of ALU designs
- Foundational for all integer arithmetic circuits
- Educational hardware design

## Citation

```bibtex
@software{tiny_fulladder_verified_2025,
  title={tiny-FullAdder-verified: Formally Verified Full Adder},
  author={Norton, Charles},
  url={https://huggingface.co/phanerozoic/tiny-FullAdder-verified},
  year={2025}
}
```