VBM is a standard for software that is specified and proved in Lean, builds freestanding with no operating-system runtime, and is written by coding agents. Its components are named vbm-<name>, and each is scored by a program that recomputes every number from the repository. Correctness is the important measure and landedness (how fast and cleanly changes land) is the second; they are reported separately and never blended into one score.
Read the manifesto: what the standard is, what it claims and what it does not.
Status: early. This repository is the standard and its tooling: the guidelines, the scorecard program, and the registry of scored repositories. Seven repositories are public. Live tools: vbm-land, the landing tool; it is not scored. Libraries: vbm-json and vbm-sse are live and scored; vbm-llm and vbm-context are pre-release and have no card yet. Foundation: vbm-simd is pre-release and unscored, and vbm-rt is early (a repository with a README and a license, nothing extracted yet). Two libraries are scored so far. Their cards say what passes and what does not, and every number is on the card, not here: see the vbm-json card and the vbm-sse card. The rows without a link are plans, not releases. Nothing here is a finished product, and the scorecard says what it cannot measure instead of guessing.
- Read the guidelines: the index; start with specification first.
- Scaffold a library with the new-vbm-library skill.
- Land with vbm-land, the landing tool (trunk-based, one lander, no pull requests for a single owner).
- Gate and prove: prove-and-gate; every gate gets a negative self-test.
- Score and register: run-the-scorecard, then register-in-the-registry.
Also: flip-checklist (publishing a repo), write-a-binding and consume-a-pinned-library.
| Name | What it is | Kind | Status | Correctness | Landedness | Card |
|---|---|---|---|---|---|---|
| vbm-land | The landing tool and its skills: one lander, one red definition, freeze marker | tool | live | unscored | unscored | - |
| vbm-rt | The freestanding runtime shim (allocator, mem* replacements, WebAssembly and native) and the ABI description with the C header and binding generators; consumers vbm-json and vbm-sse | foundation | live | unscored | unscored | - |
| vbm-simd | Bit-vector model of vector instructions, a trusted shim per instruction set, proved kernels | foundation | live | unscored | unscored | - |
| vbm-acp | Agent client protocol, pinned core profile | library | planned | unscored | unscored | - |
| vbm-baseN | base64, base64url and base16 | library | planned | unscored | unscored | - |
| vbm-context | A typed, verified agent context state (goal, obligations, facts with provenance, bounded compaction) for long-horizon LLM agents | library | live | unscored | unscored | - |
| vbm-http1 | HTTP/1.1 message framing and body length | library | planned | unscored | unscored | - |
| vbm-journal | Append-only, hash-chained log and a generic chain checker | library | planned | unscored | unscored | - |
| vbm-json | Verified JSON codec | library | live | FAIL (2 of 3; Trusted generation not yet defined) | FAIL | card |
| vbm-jsonrpc | JSON-RPC 2.0 codec and request/response matching | library | planned | unscored | unscored | - |
| vbm-llm | The wire contract of the LLM provider conventions (OpenAI, Anthropic, OpenRouter): codecs, stream fold, tool-call turns, usage and finish-reason arithmetic | library | live | unscored | unscored | - |
| vbm-mcp | Model context protocol client, pinned profile over stdio | library | planned | unscored | unscored | - |
| vbm-oauth | OAuth client flows as a state machine | library | planned | unscored | unscored | - |
| vbm-sse | Server-sent event streams | library | live | PASS (2 of 3; Trusted generation not yet defined) | PASS | card |
| vbm-uri | URI parsing and resolution (RFC 3986) | library | planned | unscored | unscored | - |
The adapter for the first row runs its subject as described in these notes; its card page shows every metric, and its one-page PDF is one page.
The pieces every library shares are being split out so that each repository stops carrying its own copy. Live: vbm-land, the landing tool, tag v0.1.0 (signed). Early: vbm-rt, the freestanding runtime shim together with the ABI description and the C header and binding generators (consumers vbm-json and vbm-sse); the repository exists, nothing is extracted into it yet. There is no kit file and no bundle: a library pins each of them by signed tag through the one update flow, with hermetic tests. Every gate carve-out must be documented and protected: an exception that is not written down and on the protected list is a hole, not a carve-out.
Everything runs through mise (it pins the Python of the runner, which is stdlib-only). You need git, jq, bash, flock, python3 (with PyYAML), a C compiler, ps, ssh-keygen, bwrap (bubblewrap) and coredumpctl (systemd-coredump); a missing tool fails the gate rather than skipping a check. The gate that every change passes, the same one CI runs:
mise exec -- scripts/tier1.sh
To score a repository: mise exec -- scorecard/scorecard run --repo <path> --commit <sha> (see run-the-scorecard). Without --sandbox nothing of the subject executes.
A repo passes an ideal when every measured part of it is at or above its floor. A card has two verdicts, Correctness first (ideals 1, 3, 4 and 7) and Landedness second (ideal 6), then a profile of the rest (ideals 2 and 5) that is in neither; there is no single score and no averaging. One failed ideal fails its verdict, a metric the scorecard cannot measure counts as a fail, and the Correctness line says how many of its four ideals were measured (never a bare PASS while one, trusted code generation, has no metric yet).
- Verified. The code that runs is the specification or derived from it: specified share 100% (a library), no unproved escapes and no non-standard axioms, non-vacuity 100% (a changed specification breaks a proof).
- Bare metal. It builds freestanding and needs no libc symbols (or a short named list).
- Correct by construction. No hand-written tests of the code (the tests are generated from the specification), mutation score 100%.
- Trusted code generation. Reproducible builds, each artifact traces to its specification, generator and toolchain, and a second compiler agrees.
- Resource efficiency. Within 2x of the best scalar independent implementation on throughput (the gap to SIMD parsers is stated on the card, not floored), with memory and latency tracked.
- Velocity (landedness). The fast gate on a typical change, with its cache warm, runs under 60 seconds; a cold clone with no cache runs within 600 seconds; there are no open pull requests.
- Process honesty. Every gate has a self-test that has been watched to fail, and the attack suite passes.
The exact definitions, floors and the reasoning are in scorecard/SPEC.md and scorecard/DECISIONS.md.
The registry lists the repositories we have scored. Anyone may run the scorecard on their own repository and publish the card (run-the-scorecard): Level 1 certifies from a proof export, and nothing of your repository runs.
To be listed, open an issue here with the card. Listing without our review waits for the isolation that makes Level 2 (running subject code) safe (register-in-the-registry).
A script reads your repo at the pinned commit and prints one JSON card: every number comes from a command, never from what a document says. Your repo is treated as untrusted code: files are read only if the adapter declares them, and anything that has to run (a build, a proof check, a gate) runs in a sandbox with no network, a read-only copy of your repo, no secrets and hard limits on time, memory and disk.
The card records the commit, the sandbox and its limits, so a score can be reproduced and audited. The design is in scorecard/SPEC.md; the sandbox contract is checked by scripts/sandbox-conformance.sh.
Small files, one idea each (index):
- Verified by construction, the trusted base is a budget, the boundary never decides, specification first, gates need negative self-tests
- Write once, generate many, generated code is checked independently, tests come from the specification, efficiency is a budget
- Trunk-based landing, choose the landing mechanism, a fast gate and small changes, one lander, revert first, no pull requests for a single owner
Read CONTRIBUTING.md first: the owner lands changes directly with the repository's own lander, so a pull request is a proposal. Report a vulnerability privately: SECURITY.md.
License: Apache-2.0 (see LICENSE).
It covers the code, the tooling and the guidelines text.