Maintained repository documentationView source on GitHub

Rendered from docs/NEWCOMER_GUIDE.md at build time without changing its status. The repository source controls if this presentation differs.

Newcomer Guide: Verification from Scratch#

Acronyms used below: application programming interface (API); artificial intelligence (AI); Boolean satisfiability problem (SAT); central processing unit (CPU); command-line interface (CLI); conjunctive normal form (CNF); deletion resolution asymmetric tautology (DRAT); directed acyclic graph (DAG); grounded decision certificate (GDC); identifier (ID); intermediate representation (IR); JavaScript Object Notation (JSON); linear resolution asymmetric tautology (LRAT); machine learning (ML); nondeterministic polynomial time (NP); operating system (OS); reduced instruction set computer (RISC); satisfiability modulo theories (SMT); Secure Hash Algorithm 256-bit (SHA-256); unsatisfiable (UNSAT); Verifier Standard (VSTD).

Welcome to Verifier Standard (VSTD). If you are new to formal verification, proof systems, or computational reproducibility, this guide is designed for you. Whether you are a high school student, an undergraduate taking your first data structures course, a compiler developer, an AI safety researcher, or a SAT solver expert, this guide introduces the core concepts and gets you running code in five minutes.

1. The 30-second intuition: grocery receipts vs. green checkmarks#

When you write software or run experiments today, tools usually give you a single bit of feedback: a green checkmark (PASS) or a red cross (FAIL).

Imagine going to the grocery store, handing over your card, and the cashier says: "Payment complete, trust me." You would ask:

You expect an itemized receipt that binds the transaction to the exact items, register, and timestamp.

In scientific computing, machine learning, and software engineering, a green checkmark does not tell you:

  1. What exact file or dataset was checked? (Did someone swap the weights or modify the dataset after the run?)
  2. What tool did the checking, and what were its bounds? (Did it run out of time and exit 0 by mistake?)
  3. Can another person reproduce the exact same bytes on their machine? (Or does it only work on the author's laptop?)
  4. How can someone prove the result wrong? (What is the refutation recipe?)

VSTD is the itemized receipt for computational claims.

It wraps any computation with five cryptographic guarantees:

claim + exact evidence + named mechanism + bounds + refutation recipe
                          │
                          ▼
                PASS / FAIL / UNKNOWN

2. Why "UNKNOWN" is your friend#

In standard tools, everything is forced into a binary: either it passed or it failed. If a test times out, a script crashes, or a theorem prover runs out of memory, systems often silently fail or crash.

In honest science, if your thermometer only measures up to 100°C and your reaction reaches 150°C, you do not write down "Reaction passed." You write down: inconclusive / out of bounds.

VSTD elevates UNKNOWN to a first-class, honorable result:

3. Five-minute Python walkthrough#

You do not need complicated tools or heavy frameworks to use VSTD. The reference library has zero required third-party dependencies—it runs on standard Python 3.10+.

Step 1: Install verifier-standard#

python -m pip install "verifier-standard==1.5.0"

Step 2: Inspect the library#

Open a Python interactive shell:

import verifier

print(verifier.__version__)
# '1.5.0'

print(verifier.__standard__)
# 'VSTD-5'

Step 3: Run the built-in defensive demonstration#

To see VSTD catch real-world defects without modifying any files on your computer, run the canonical cross-platform command:

vstd demo

You will see four defensive scenarios:

  1. Valid-looking proof, wrong artifact (REJECTED): An attacker provides a real mathematical proof, but binds it to the wrong data file. VSTD computes the SHA-256 hash and catches the mismatch immediately.
  2. Bound exhausted without a false answer (ACCEPTED/UNKNOWN): A calculation hits its resource limit. Instead of faking a pass, VSTD honestly outputs UNKNOWN.
  3. Inflated verification-cost claim (REJECTED): A script claims a verification step cost \$1,000,000 of compute when it only took milliseconds. The receipt refuses the ungrounded cost claim.
  4. Revoked ancestor behind valid descendants (GRAPH-CANDIDATE-0): A computation looks valid, but one of its upstream dependencies was revoked. VSTD traces the lineage graph and flags the compromised ancestor.

4. Seven domain lenses: how VSTD fits your field#

VSTD is domain-agnostic: it does not replace your native tools; it packages and standardizes their evidence boundaries. Here is how people in different fields use it, with concrete links to tutorials and runnable examples:

A. For Undergraduates, High Schoolers & Self-Taught Programmers#

Think of VSTD as a tamper-proof digital lab notebook. When submitting a class project, physics simulation, or machine learning experiment:

How can a grader possibly verify your work with one command?#

If you have ever handed in homework, you might wonder: How can a teacher or automated grading bot actually know my code really produced this graph without reading every single line or trusting my word?

Here is the exact three-step mechanic:

  1. Digital Fingerprints (SHA-256 Hashes): VSTD computes cryptographic fingerprints of your code (script.py) and inputs (data.csv). If anyone edits a single character or changes one number in the comma-separated values (CSV), the fingerprint changes completely into a different, unpredictable hex string.
  2. The Receipt Binding: When you run vstd run manifest.json --output my_receipt, VSTD executes your script, records the exact command, exit code, and runtime platform details (e.g. Python version and OS architecture, without recording private host environment variables or credentials), and takes fingerprints of the output files (e.g. plot.png has digest e3b0c442...).
  3. The Grader's Single Command (vstd reproduce): The grader downloads your receipt and runs: ``bash vstd reproduce my_receipt/ ` Under the hood, vstd reproduce`:
    • Checks that the inputs match the fingerprints in your receipt.
    • Creates a clean, temporary execution folder and re-runs python script.py data.csv.
    • Fingerprints the newly generated plot file and compares: Does the fresh digest match e3b0c442... byte-for-byte?
    • If they match, the grader sees: [REPRODUCE OK] 100% byte-for-byte identical output. If a student edited the graph in Photoshop or faked the numbers, the newly computed bytes will not match, and VSTD outputs REJECTED: output digest mismatch.

B. For Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) Solver Enthusiasts#

Modern SAT and SMT solvers decide whether a propositional logic formula is satisfiable (SAT) or unsatisfiable (UNSAT). But solver implementations are complex and can have soundness bugs:

C. For Compiler and Systems Engineers#

Compilers optimize programs across multiple intermediate representations (IR). A compiler bug can silently miscompile code into incorrect machine instructions:

D. For AI Safety Researchers and Transfinite Mathematicians#

When analyzing self-referential systems, recursive agent loops, ordinal bounds, or non-well-founded belief graphs:

E. For Intellidynamics and AI Benchmarkers#

Automated agent evaluations and language model leaderboards are plagued by prompt leaking, test-set contamination, and stochastic output variance:

F. For Deep Mathematics & Theorem Provers (Lean 4, Metamath, and Formal Kernels)#

When working in advanced mathematical foundations, interactive theorem provers (such as Lean 4, Coq, Isabelle, or Metamath) and foundational algebraic kernels produce mechanically checked proofs:

G. For Nanochemistry, Molecular Robotics & Mechanosynthesis (Self-Assembly Containment and Anti-Replication Gates)#

In molecular dynamics simulations, chemical reaction networks (CRNs), and autonomous molecular robotics (such as deoxyribonucleic acid (DNA) origami walkers or mechanosynthetic tooltips), molecular self-assembly poses an urgent containment challenge: preventing runaway autocatalytic self-replication.

A molecular design tool or simulation might assert: "This molecular machine only constructs the target crystal structure." But in reality:

VSTD provides the computational containment seal:

  1. Coordinate and Stoichiometric Binding: VSTD binds the exact atomic coordinate files, force-field potential parameter files, stoichiometric reaction matrices, and simulation integration steps into an immutable receipt.
  2. Refutation Route for Containment Claims: An assertion of "Non-self-replicating under standard physiological conditions" is paired with an explicit refutation recipe: any researcher or adversary who demonstrates a reachable catalytic cycle (a series of reaction steps with activation energies below threshold E_a < E_{\text{barrier}}) leading to exponential autocatalysis overturns the claim.
  3. Synthesis Interlock: Physical robotic nanofabrication devices can require an Ed25519-signed VSTD receipt proving that containment bounds were verified before releasing chemical feedstocks or beginning automated assembly.

5. Next steps#

Now that you understand the mental model: