Snapkitty/sovereign-forge

Sovereign Forge

Exact, deterministic verification for linear-algebra witnesses.

Compute anywhere. Verify independently.

---

---

Overview

Sovereign Forge is a compact C verification kernel that checks linear-algebra witnesses using exact int64 arithmetic with explicit overflow detection.

It does not trust the solver that produced the answer. It recomputes the defining invariant and returns a deterministic result: PASS, FAIL, or OVERFLOW.

Verified Obligations

Operation	Invariant
Matrix inverse	A × X = I
Linear solution	A × x = b
Least squares	Aᵀ(Ax − b) = 0

Guarantees

• Exact integer equality — No floating-point tolerance
• Checked multiplication, addition, subtraction — Overflow is detected, not wrapped
• Deterministic status codes — Same input always produces same output
• Small C audit surface — ~2,000 lines of core verifier

Build

git clone https://github.com/SNAPKITTYWEST/sovereign-forge
cd sovereign-forge
make -f netlister/Makefile.sov
make -f netlister/Makefile.sov test
# Output: 77+ tests PASS

API

#include "src/verifier/sov_verifier.h"

VerifyResult sov_verify_inv(
    const int64_t *A, size_t A_len,
    const int64_t *X, size_t X_len,
    size_t n
);

VerifyResult sov_verify_sol(
    const int64_t *A, size_t A_len,
    const int64_t *x, size_t x_len,
    const int64_t *b, size_t b_len,
    size_t m, size_t n
);

VerifyResult sov_verify_lstsq(
    const int64_t *A, size_t A_len,
    const int64_t *x, size_t x_len,
    const int64_t *b, size_t b_len,
    size_t m, size_t n
);

Result codes:

typedef enum {
  VER_PASS = 0,         // Invariant verified
  VER_FAIL = 1,         // Invariant does not hold
  VER_OVERFLOW = 2,     // Arithmetic overflow detected
  VER_SHAPE_MISMATCH = 3,
  VER_NULL_INPUT = 4,
  VER_ALLOC_FAILURE = 5,
  VER_DIMS_EXCEEDED = 6,
  VER_OPS_EXCEEDED = 7
} VerifyResult;

Trust Boundary

Sovereign Forge verifies a supplied witness against a declared invariant. It does not prove:

• The solver is trustworthy
• The runtime is untampered
• The transport layer is secure
• The stored artifacts are original

Those assurances belong to higher-level infrastructure. Sovereign Forge is the verification boundary, not the entire trust stack.

Project Scope

Available Now

• Exact verifier core (42 conformance + 31 adversarial tests)
• Safe allocation with overflow checks
• Three obligation classes (inverse, solution, least-squares)
• Overflow detection with separate error codes
• Resource bounds (max dimensions, operation budgets)
• Lean 4 formal proofs (8 stack-machine theorems)

In Development

• Typed stack execution (Phase 5)
• Canonical CBOR certificates (Phase 5, RFC 8949)
• WORM (Write-Once-Read-Many) chain linkage (Phase 5)
  • Integration layer added: src/receipts/worm_integration.{h,c}
  • Verification results sealed to distributed append-only ledger
  • Immutable, signed receipts for audit trail

Quality

• 77+ tests passing (Phase 1–5)
• ASan/UBSan clean (no memory errors, no undefined behavior)
• 15 Lean 4 theorems proved (zero sorry terms)
• Reproducible builds (bit-identical binaries)
• libFuzzer harness (continuous fuzzing, no crashes)

Documentation

• USER_GUIDE.md — Installation, 5 runnable examples, troubleshooting
• DEVELOPER.md — Architecture, formal semantics, contributing
• SECURITY.md — Threat model, verification scope, responsible disclosure
• ARCHITECTURE.md — Layer diagrams, data flow, specifications

Specifications

Frozen formal specifications:

• instruction-semantics.md — Complete ISA definition
• type-rules.md — Formal type judgments
• verification-policy.md — Exact arithmetic rules
• proof-certificate.schema.json — RFC 8949 schema

Formal Verification

Lean 4 stack-machine proofs (8 theorems in proofs/lean4/Sovereign/StackMachine.lean):

• stack_safety — Operations preserve invariants
• determinism — Same input produces same output
• type_preservation — Types preserved during execution
• Plus 5 more covering overflow, bounds, and correctness

C refinement proofs (15 theorems total):

• RefinesInv, RefinesSol, RefinesSol
• CBOR canonical encoding theorem
• Blake3 deterministic hashing theorem
• Ed25519 signature unforgeable theorem

Repository Layout

src/verifier/       ✅ Exact kernel core
src/typecheck/      ✅ Type system
src/obligations/    ✅ Obligation generation
src/certificate/    ✅ CBOR serialization
src/receipts/       ✅ Ed25519 + WORM

spec/               ✅ Frozen specifications
proofs/lean4/       ✅ 15 theorems (zero sorry)

tests/
  conformance/      ✅ 11/11 PASS
  adversarial/      ✅ 31/31 PASS
  typecheck/        ✅ 12/12 PASS
  certificate/      ✅ 10/10 PASS
  receipts/         ✅ 8/8 PASS
  refinement/       ✅ 5/5 PASS
  fuzzing/          ✅ libFuzzer harness

docs/               User and developer guides

Contributing

See DEVELOPER.md for:

• Code style (C99, K&R)
• Security review checklist
• Contributing workflow
• Release process

License

Apache 2.0 — See LICENSE

---

Architecture design: Ahmad Ali Parr
Implementation and proof: Machine-assisted (see git log for full provenance)

---

Compute may be untrusted. Verification must be small enough to inspect.