Formal Verification and Proofs
Collection
Zero-sorry Lean 4 theorems, Agda formalizations, and cross-language verification. Every proof compiles. No axiom admits. • 12 items • Updated
YAML Metadata Warning:empty or missing yaml metadata in repo card
Check out the documentation for more information.
██████╗ ██╗ ██╗██████╗ ███████╗
██╔══██╗██║ ██║██╔══██╗██╔════╝
██████╔╝██║ ██║██████╔╝█████╗
██╔═══╝ ██║ ██║██╔══██╗██╔══╝
██║ ╚██████╔╝██║ ██║███████╗
╚═╝ ╚═════╝ ╚═╝ ╚═╝╚══════╝
██╗ ██╗ █████╗ ██╗ ██╗██████╗ ██╗████████╗██╗ ██╗
██║ ██║██╔══██╗██║ ██║██╔══██╗██║╚══██╔══╝╚██╗ ██╔╝
██║ ██║███████║██║ ██║██║ ██║██║ ██║ ╚████╔╝
╚██╗ ██╔╝██╔══██║██║ ██║██║ ██║██║ ██║ ╚██╔╝
╚████╔╝ ██║ ██║███████╗██║██████╔╝██║ ██║ ██║
╚═══╝ ╚═╝ ╚═╝╚══════╝╚═╝╚═════╝ ╚═╝ ╚═╝ ╚═╝
Formal verification from NAND gates to proof certificates.
What Is This?
A self-contained formal verification engine built from first principles. No Z3. No SMT solver dependency. No Lean. No Coq. Just:
- A source language (
.nffiles) where NAND is the only primitive - A compiler that elaborates definitions into Boolean circuits
- A SAT solver (DPLL + CDCL with clause learning) that searches for proofs
- A proof-producing backend that emits resolution certificates
- A trusted kernel (~80 lines) that independently verifies those certificates
The foundational principle: the engine searches, the kernel decides.
╔══════════════════════════════════════════════════════════════════════════╗
║ ║
║ THE SEPARATION ║
║ ║
║ SOLVER (complex, 1000+ LOC) KERNEL (simple, ~80 LOC) ║
║ ───────────────────────── ────────────────────── ║
║ ║
║ Heuristics, backtracking, Resolution step checker ║
║ clause learning, unit prop, Clause validation ║
║ decision ordering, restarts Hash verification ║
║ ║
║ MAY HAVE BUGS MUST BE CORRECT ║
║ (if buggy: proof won't verify) (if buggy: false validity) ║
║ ║
║ A bug in the solver = A bug in the kernel = ║
║ "failed to find proof" "accepted invalid proof" ║
║ (safe failure) (unsound — the only real risk) ║
║ ║
╚══════════════════════════════════════════════════════════════════════════╝
Quick Start
git clone https://github.com/SNAPKITTYWEST/pure-validity
cd pure-validity
cabal build
cabal run pure-validity -- examples/gates.nf
Module: gates
Properties: 16
[OK] not_true
[OK] not_false
[OK] and_tt
[OK] and_tf
[OK] and_ft
[OK] and_ff
[OK] or_tt
[OK] or_tf
[OK] or_ft
[OK] or_ff
[OK] xor_tt
[OK] xor_tf
[OK] xor_ft
[OK] xor_ff
16/16 verified.
The Language — .nf files
NAND is the only hardware primitive. Everything else is defined, not assumed.
-- gates.nf — derive all logic from NAND alone
def not(x) = (x | x);
def and(x y) = not((x | y));
def or(x y) = (not(x) | not(y));
def xor(x y) = ((x | (x | y)) | (y | (x | y)));
-- Prove correctness of derived gates
prove and_tt: and(true true) = true;
prove xor_tf: xor(true false) = true;
Syntax Reference
╔════════════════════╦═══════════════════════════════════════════════╗
║ CONSTRUCT ║ MEANING ║
╠════════════════════╬═══════════════════════════════════════════════╣
║ (a | b) ║ NAND — the only primitive gate ║
║ def f(x y) = e; ║ Define a named circuit ║
║ prove n: e; ║ State and verify a property ║
║ assert e; ║ Verify without naming ║
║ true / false ║ Boolean constants ║
║ -- comment ║ Line comment ║
║ module name; ║ Module declaration ║
╚════════════════════╩═══════════════════════════════════════════════╝
Verification Pipeline
.nf source file
│
▼
┌─────────────────────────────────────────────────────────┐
│ LEXER + PARSER │
│ Language/Lexer.hs + Language/Parser.hs │
│ Source text → Token stream → AST (Module of Stmts) │
└─────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────┐
│ ELABORATOR │
│ Language/Elaborator.hs │
│ AST → Boolean IR (BExpr trees — NAND-only) │
│ Inlines function applications, resolves names │
└─────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────┐
│ TSEITIN TRANSFORM │
│ SAT/CNF.hs │
│ BExpr → CNF (conjunctive normal form) │
│ Introduces auxiliary variables, linear blowup │
└─────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────┐
│ SAT SOLVER (DPLL + CDCL) │
│ SAT/DPLL.hs + SAT/CDCL.hs │
│ Unit propagation → decision → conflict → backtrack │
│ Clause learning on conflict (CDCL) │
│ Proof-producing: records resolution steps │
└─────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────┐
│ PROOF CERTIFICATE │
│ Proof/Certificate.hs + Proof/Produce.hs │
│ Resolution steps + SHA-256 hash │
│ Conclusion: Valid | Unsatisfiable | CounterExample │
└─────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────┐
│ TRUSTED KERNEL (~80 LOC) │
│ Checker/Kernel.hs │
│ Independently verifies every resolution step │
│ Accepts or rejects the certificate │
│ THE ONLY CODE THAT MUST BE CORRECT │
└─────────────────────────────────────────────────────────┘
│
▼
[OK] Property verified / [FAIL] Counterexample found
Architecture — Why Two Layers?
The insight from proof-carrying code (Necula 1997): separate the search from the checking.
A solver can be arbitrarily complex — heuristics, restarts, clause deletion, VSIDS scoring. If it has a bug, it just fails to find the proof. The system remains sound.
The kernel is trivial by comparison. It receives a claimed proof (sequence of resolution steps) and mechanically verifies each step: did resolving clause A with clause B on pivot variable P actually produce clause C? That's it. ~80 lines. Auditable by hand.
╔══════════════════════════════════════════════════════════════╗
║ ║
║ Solver bug → "could not prove" (safe, retry with better ║
║ heuristics or more time) ║
║ ║
║ Kernel bug → false validity claim (unsound — THE risk) ║
║ But kernel is 80 LOC, auditable, testable ║
║ ║
╚══════════════════════════════════════════════════════════════╝
Fortran Backend
For hardware-scale verification (thousands of gates), the Fortran backend provides vectorized clause checking and bounded model checking:
! bitvec_ops.f90 — bulk NAND evaluation + clause checking
call bulk_clause_check(clauses, num_clauses, clause_lens, assignment, num_vars, satisfied)
! state_machine.f90 — bounded model checking with induction
result = bmc_check(transition_gates, ..., init_state, state_width, bound)
The Fortran modules handle:
- Vectorized NAND evaluation over flat gate arrays
- Bulk satisfiability checking across all clauses simultaneously
- Ripple-carry addition for arithmetic circuit verification
- Bounded model checking (BMC) for sequential circuits
- k-induction for unbounded property proofs
Examples
╔═══════════════════╦══════════════════════════════════════════════════╗
║ FILE ║ WHAT IT PROVES ║
╠═══════════════════╬══════════════════════════════════════════════════╣
║ nand.nf ║ NAND truth table (the primitive) ║
║ gates.nf ║ NOT/AND/OR/XOR all correct from NAND alone ║
║ half_adder.nf ║ Binary arithmetic: sum and carry correct ║
║ demorgan.nf ║ De Morgan's Laws hold for NAND-derived gates ║
║ mux.nf ║ 2-to-1 multiplexer selects correctly ║
╚═══════════════════╩══════════════════════════════════════════════════╝
Run all examples:
for f in examples/*.nf; do cabal run pure-validity -- "$f"; echo; done
Project Layout
pure-validity/
├── pure-validity.cabal Build configuration
├── README.md This file
│
├── src/
│ ├── Main.hs Entry point — file → parse → prove → check
│ ├── Language/
│ │ ├── AST.hs Abstract syntax (Expr, Stmt, Module)
│ │ ├── Lexer.hs Tokenizer (keywords, operators, idents)
│ │ ├── Parser.hs Recursive descent parser
│ │ └── Elaborator.hs AST → Boolean IR (inline + resolve)
│ ├── IR/
│ │ ├── Boolean.hs BExpr type + eval + NAND/AND/OR/XOR
│ │ ├── NAND.hs NAND normal form transformation
│ │ └── BitVec.hs Bit-vector arithmetic (add, eq, const)
│ ├── SAT/
│ │ ├── CNF.hs Clause/literal types + Tseitin transform
│ │ ├── UnitProp.hs Unit propagation (BCP)
│ │ ├── DPLL.hs Davis-Putnam-Logemann-Loveland solver
│ │ └── CDCL.hs Conflict-Driven Clause Learning solver
│ ├── Proof/
│ │ ├── Certificate.hs ProofStep, ProofCertificate types
│ │ └── Produce.hs Validity/UNSAT proof generation
│ └── Checker/
│ └── Kernel.hs THE TRUSTED KERNEL (~80 LOC)
│
├── fortran/
│ ├── bitvec_ops.f90 Vectorized NAND + bulk clause check
│ └── state_machine.f90 BMC + k-induction for sequential circuits
│
├── examples/
│ ├── nand.nf NAND primitive proofs
│ ├── gates.nf All gates from NAND
│ ├── half_adder.nf Arithmetic correctness
│ ├── demorgan.nf De Morgan's Laws
│ └── mux.nf Multiplexer properties
│
└── test/
└── Spec.hs 20 tests — IR, solver, kernel, parser
Run Tests
cabal test
[OK] NAND truth table
[OK] NOT from NAND
[OK] AND from NAND
[OK] OR from NAND
[OK] XOR from NAND
[OK] Half adder sum
[OK] Half adder carry
[OK] BitVec add 3+5=8
[OK] Tseitin preserves satisfiability
[OK] DPLL finds SAT
[OK] DPLL finds UNSAT
[OK] Unit propagation
[OK] Proof certificate valid
[OK] Checker accepts valid
[OK] Checker rejects invalid
[OK] Parse module
[OK] Elaborate module
[OK] NAND normal form
[OK] De Morgan via eval
[OK] MUX correctness
20/20 tests passed.
Requirements
- GHC 8.10+ (Haskell compiler)
- Cabal 3.0+
- gfortran (for Fortran backend, optional)
- Zero external solver dependencies (no Z3, no MiniSat, no SMT-LIB)
# Install GHC + Cabal (if needed)
curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh
# Build and run
cabal build
cabal run pure-validity -- examples/gates.nf
cabal test
Theory
The verification approach combines:
- Tseitin transformation — Boolean formula to CNF with linear blowup (not exponential)
- DPLL — systematic backtracking search with unit propagation
- CDCL — conflict-driven clause learning for exponential speedup on structured problems
- Resolution proofs — the solver records why it concluded UNSAT
- Proof checking — independent verification that each resolution step is valid
To prove a property P holds: negate P, convert to CNF, prove UNSAT. If the negation is unsatisfiable, the original property is valid (true under all assignments).
Built by Ahmad Ali Parr + SnapKitty Collective
╔══════════════════════════════════════════════════════╗
║ ║
║ The engine searches. ║
║ The kernel decides. ║
║ ║
║ If the kernel is correct, the system is sound. ║
║ The kernel is 80 lines. ║
║ Read them yourself. ║
║ ║
╚══════════════════════════════════════════════════════╝
Inference Providers NEW
This model isn't deployed by any Inference Provider. 🙋 Ask for provider support