Skip to content

VeriLib Documentation

VeriLib is a free open-source library of formally verified code and tools for proving that code does what you want — that it meets your specifications.

The goal is to make formal verification much more widely used: cheaper automation → broader adoption → larger benchmarks → better AI-powered verification tools.

Get started About VeriLib Browse verilib.org

Get started

Start with a framework workflow and connect your project in minutes.

  • Quick start

    Install verilib-cli, authenticate, and initialize your first repository.

    Quick start

  • CLI reference

    Repository commands, verification workflow, and CI patterns.

    Scripts and CLI

  • First contribution

    Fork, branch, open a PR, and follow the docs checklist.

    Contributing

  • Glossary

    Verification statuses, atom kinds, and color mapping.

    Glossary

Build with the platform

  • Frontend

    PHP + React UX at verilib.org: uploads, certify, and /v2 API — enqueues work for workers.

  • verilib-cli

    Public Rust CLI: auth, init, deploy/pull, and local create / atomize / specify / verify.

  • Atomizer

    Upload and atomize RabbitMQ workers — S3, language probes, Schema 3.0 parse, MySQL atoms.

  • Certificates

    Probe Docker images plus DB-free validate/promote workers (Sepolia, mainnet, Docker Hub).

  • System map

    End-to-end map: CLI and UI → API/queues → atomizer and cert workers.

Why formal verification?

Traditional software testing can only prove the presence of bugs. Formal verification can prove their absence. Bugs have enabled cyberattacks, rocket crashes, and large-scale outages — the 2024 CrowdStrike incident alone cost over $10 billion.

VeriLib also supports a safer path for AI: instead of trusting opaque neural networks in safety-critical settings, write a clear specification, let AI produce code and a proof, then check the proof with a small trusted verifier.

VeriLib is supported by the US-based non-profit Beneficial AI Foundation, which funds technical AI safety research.

Read the full About Live about on verilib.org Beneficial AI Foundation

Explore more

How you can help

Use VeriLib, upload and share verified code, and send bug reports or feature requests. Start with the Quick start or browse the library at verilib.org.