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¶
Start with a framework workflow and connect your project in minutes.
-
Quick start
Install
verilib-cli, authenticate, and initialize your first repository. -
CLI reference
Repository commands, verification workflow, and CI patterns.
-
First contribution
Fork, branch, open a PR, and follow the docs checklist.
-
Glossary
Verification statuses, atom kinds, and color mapping.
Build with the platform¶
-
PHP + React UX at verilib.org: uploads, certify, and
/v2API — enqueues work for workers. -
Public Rust CLI: auth, init, deploy/pull, and local create / atomize / specify / verify.
-
Upload and atomize RabbitMQ workers — S3, language probes, Schema 3.0 parse, MySQL atoms.
-
Probe Docker images plus DB-free validate/promote workers (Sepolia, mainnet, Docker Hub).
-
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¶
Documentation hub Architecture API specification Repo list Troubleshooting How to write docs Community GitHub org
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.