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

# tiny-NOT-prover

Formally verified NOT gate. Single threshold neuron computing negation with 100% accuracy.

## Architecture

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

## Key Properties

- 100% accuracy (2/2 inputs correct)
- Coq-proven correctness
- Single threshold neuron
- Integer weights
- Involutive: NOT(NOT(x)) = x

## Usage

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

weights = load_file('not.safetensors')

def not_gate(x):
    # Heaviside: weighted_sum + bias >= 0
    return int((x * weights['weight'] + weights['bias']) >= 0)

# Test
print(not_gate(0))  # 1
print(not_gate(1))  # 0
```

## Verification

**Coq Theorem**:
```coq
Theorem not_correct : forall x, not_circuit x = negb x.
```

Proven axiom-free. Full proof: [coq-circuits/Boolean/NOT.v](https://github.com/CharlesCNorton/coq-circuits)

## Citation

```bibtex
@software{tiny_not_prover_2025,
  title={tiny-NOT-prover: Formally Verified NOT Gate},
  author={Norton, Charles},
  url={https://huggingface.co/phanerozoic/tiny-NOT-prover},
  year={2025}
}
```