Upload Code
Package Summary Specifications Assumptions Verification Results Our open standard Verify it yourself Install Docker Docker image

Formal Verification Certificate

pmemlog — certified snapshot

This software package satisfies these specifications with these assumptions (see below). Specifically, everything shown with green text or background is auto-certified by VeriLib (and you can trivially re-verify it yourself), while what's shown with white background are unverified claims by the project team, included for pedagogy.

Certification date April 17, 2026
Package commit 6fa654b
Functions Verified 70/70
Ethereum Proof Etherscan
Package Summary
GitHub VeriLib

This repository is a formal verification project for a persistent-memory append-only log (pmemlog) using Verus, a verification tool for Rust that checks specifications and proofs via SMT solving. The library provides a crash-safe circular log over byte-addressable persistent memory; the Verus proofs establish that the implementation correctly refines an abstract infinite log model despite arbitrary crashes and potential storage corruption.

The verified code covers a circular on-disk layout with dual headers, CRC-based corruption detection, and a write-restricted persistent memory interface that enforces crash safety by quantifying over all possible partial-flush schedules. Verus proofs establish that recovery always reconstructs a valid abstract log state, that append and advance-head operations preserve this invariant through any crash, and that reads return correct data modulo a formally modeled corruption model.

Applications

  • Persistent append-only logs can be used as write-ahead logs (WAL) for databases and file systems running on persistent memory (e.g., Intel Optane).
  • Crash-safe logging enables durable message queues and event stores that survive power failures without data loss or silent corruption.
  • The verified crash-consistency and corruption-detection properties provide a foundation of trust for higher-level persistent data structures built on top of the log.
Specifications
Assumptions
Verus Verifier

We assume that the Verus verification system, including its standard library (vstd), correctly implements its verification logic and sound reasoning principles.

Z3 SMT Solver

Verus relies on the Z3 automated theorem prover for checking logical conditions. We assume that Z3 correctly implements SMT solving algorithms.

Rust Compiler

We assume that the Rust compiler correctly translates our verified code into machine instructions, and that it respects the semantics Verus reasons about.

Known Properties

Mathematical truths whose known proofs are not replicated within this project.

Dependencies

We assume correctness of the dependencies listed in the Cargo.toml file: crc64fast (for CRC-64 computation) and the Verus standard library (vstd).

Rust Features

Some internal functions are trusted without proof because they use Rust features Verus does not yet support (iterators, slice conversions, trait dispatch). These are marked external_body with manually written postconditions.

Hardware

We assume correct execution of machine code and that the persistent memory medium (e.g., Intel Optane DCPMM) implements the persistence semantics we model.

CRC Corruption Detection

We assume CRC-64 reliably detects corruption: if stored data and its CRC are read back and the CRC still matches, the data is uncorrupted (axiom_bytes_uncorrupted). We also assume cdb0_val and cdb1_val are distinct enough that corruption cannot transform one into the other (axiom_corruption_detecting_boolean).

Persistent Memory Model

We assume: (1) writes persist in 8-byte chunks, with any subset flushed during a crash; (2) writes are immediately visible to subsequent reads within a single execution; (3) each 8-byte chunk is written atomically.

Verification Results

Below are the formal verification results. Please check if the first test line says "VerificationSuccess": true.

Manifest
{
  "VerificationSuccess": true,
  "atoms_note": "Verified keys: unified verification-status verified, error/failed (or similar), or proofs.verified; excludes unverified/trusted. Manifest counts: unified data — TBV = verified + error/errored; list = verified keys only. [worker] Counts recomputed from probe-verus extract on disk (status-only rules).",
  "branch": "main",
  "build_arg_commit": "6fa654b2124cfe12831fa30a8d062e5b118f4526",
  "cargo_package": "",
  "cert_readme_badge_alt": "VeriLib Certified",
  "cert_readme_badge_image_url": "https://verilib.org/assets/img/verilib-certified-badge-wide.svg",
  "cert_readme_page_url": "https://verilib.org/cert/5171",
  "commit": "6fa654b2124cfe12831fa30a8d062e5b118f4526",
  "commit_date_utc": "2026-03-11T15:35:50+01:00",
  "image": "cert-probe-docker",
  "image_build_date_utc": "2026-04-17T12:11:37Z",
  "probe_extract_completed_at_utc": "2026-04-17T12:11:37Z",
  "probe_verus_version": "6.9.1",
  "repo": "https://github.com/Beneficial-AI-Foundation/pmemlog_with_callgraph.git",
  "source_tree_sha256": "99c2df1bac56a4aa1429a3c34e0b77105a0609d9adfa0fbff300ab9d798ebdf3",
  "to_be_verified": 70,
  "unified_extract_json_path": "/opt/cert-target-src/.verilib/probes/verus_pmemlog_0.1.0.json",
  "unified_extract_json_sha256": "47fafda9f049e04b72563e69395c05a1623e3a794dfdde48a14852e5372fd5de",
  "verification_source": "unified_extract_json",
  "verified_functions": [
    "probe:pmemlog/0.1.0/logimpl_v/&UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#untrusted_get_head_and_tail()",
    "probe:pmemlog/0.1.0/logimpl_v/&UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#untrusted_read()",
    "probe:pmemlog/0.1.0/logimpl_v/&mut/UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#append_no_wrap()",
    "probe:pmemlog/0.1.0/logimpl_v/&mut/UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#append_wrap()",
    "probe:pmemlog/0.1.0/logimpl_v/&mut/UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#untrusted_advance_head()",
    "probe:pmemlog/0.1.0/logimpl_v/&mut/UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#untrusted_append()",
    "probe:pmemlog/0.1.0/logimpl_v/&mut/UntrustedLogImpl#UntrustedLogImpl<&WriteRestrictedPersistentMemory<Perm>#update_header()",
    "probe:pmemlog/0.1.0/logimpl_v/UntrustedLogImpl<&PM>#read_incorruptible_boolean()",
    "probe:pmemlog/0.1.0/logimpl_v/UntrustedLogImpl<Result<UntrustedLogImpl,/InfiniteLogErr>\nwhere\n////Perm:/CheckPermission<Seq<u8>>,\n////PM:/PersistentMemory,>#untrusted_start()",
    "probe:pmemlog/0.1.0/logimpl_v/UntrustedLogImpl<u64>#addr_logical_to_physical()",
    "probe:pmemlog/0.1.0/logimpl_v/UntrustedLogImpl<u64>#untrusted_setup()",
    "probe:pmemlog/0.1.0/logimpl_v/bytes_to_header()",
    "probe:pmemlog/0.1.0/logimpl_v/bytes_to_metadata()",
    "probe:pmemlog/0.1.0/logimpl_v/crc_and_metadata_bytes_to_header()",
    "probe:pmemlog/0.1.0/logimpl_v/header_to_bytes()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_append_data_update_view()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_append_data_update_view_crash()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_append_ib_update()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_append_ib_update_effect_on_committed()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_bytes_combine_into_header()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_data_write_is_safe()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_header_correct()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_header_crc_correct()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_header_match()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_header_split_into_bytes()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_headers_unchanged()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_inactive_header_update_view()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_inactive_header_update_view_crash()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_incorruptible_bool_unchanged()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_metadata_bytes_eq()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_pm_state_header()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_same_log_state()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_same_permissions()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_seq_addition()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_single_write_crash()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_subrange_eq()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_subrange_equality_implies_index_equality()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_subrange_equality_implies_subsubrange_equality()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_subrange_equality_implies_subsubrange_equality_forall()",
    "probe:pmemlog/0.1.0/logimpl_v/lemma_u64_bytes_eq()",
    "probe:pmemlog/0.1.0/logimpl_v/metadata_to_bytes()",
    "probe:pmemlog/0.1.0/main_t/&InfiniteLogImpl<PM>#InfiniteLogImpl<Result<(u64,/u64,/u64),/InfiniteLogErr>>#get_head_and_tail()",
    "probe:pmemlog/0.1.0/main_t/&InfiniteLogImpl<PM>#InfiniteLogImpl<u64>#read()",
    "probe:pmemlog/0.1.0/main_t/&mut/InfiniteLogImpl<PM>#InfiniteLogImpl<&Vec<u8>>#append()",
    "probe:pmemlog/0.1.0/main_t/&mut/InfiniteLogImpl<PM>#InfiniteLogImpl<u64>#advance_head()",
    "probe:pmemlog/0.1.0/main_t/InfiniteLogImpl<u64>#setup()",
    "probe:pmemlog/0.1.0/main_t/InfiniteLogImpl<u64>#start()",
    "probe:pmemlog/0.1.0/main_t/TrustedPermission<spec_fn(AbstractInfiniteLogState>#new()",
    "probe:pmemlog/0.1.0/math_v/lemma_div_relation_when_mods_have_different_order()",
    "probe:pmemlog/0.1.0/math_v/lemma_div_relation_when_mods_have_different_order_alt()",
    "probe:pmemlog/0.1.0/math_v/lemma_div_relation_when_mods_have_same_order()",
    "probe:pmemlog/0.1.0/math_v/lemma_div_relation_when_mods_have_same_order_alt()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_addition_when_bounded()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_auto_basics()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_between()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_difference_equal()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_equal()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_equal_converse()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_not_between()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_not_equal()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_subtract()",
    "probe:pmemlog/0.1.0/math_v/lemma_mod_wrapped_len()",
    "probe:pmemlog/0.1.0/math_v/lemma_mul_div_equal()",
    "probe:pmemlog/0.1.0/pmemspec_t/&WriteRestrictedPersistentMemory<Perm,/PM>#WriteRestrictedPersistentMemory<PM>#get_pm_ref()",
    "probe:pmemlog/0.1.0/pmemspec_t/&mut/WriteRestrictedPersistentMemory<Perm,/PM>#WriteRestrictedPersistentMemory<u64>#write()",
    "probe:pmemlog/0.1.0/pmemspec_t/WriteRestrictedPersistentMemory<PM>#new()",
    "probe:pmemlog/0.1.0/pmemspec_t/axiom_bytes_uncorrupted()",
    "probe:pmemlog/0.1.0/pmemspec_t/axiom_corruption_detecting_boolean()",
    "probe:pmemlog/0.1.0/pmemspec_t/read()",
    "probe:pmemlog/0.1.0/pmemspec_t/write()"
  ],
  "verified_functions_count": 70,
  "verified_functions_missing_atom_record": [],
  "verus_release_tag": "release/0.2026.01.14.88f7396"
}
Our open standard for verification certification

We have designed our VeriLib verification certificates to meet three goals:

  • Transparency: Easy to see precisely what has been verified about what code with what tooling & assumptions
  • Reproducibility: Easy for user to automatically reproduce all certified claims, so no need to trust the issuer of the certificate
  • Usability: Quick and easy to build the desired level of trust:
    • Busy users can choose trust crowdsourcing: simply trusting software with the green checkmark, knowing that if it were fraudulent, someone else would probably have tried to reproduce it, failed, sounded the alarm, and permanently destroyed VeriLib’s credibility.
    • More hardcore users can automatically repeat and inspect the entire verification process on their own machine.

Here is how this works in detail. The green checkmark displayed (at the top of certificate pages such as this one) is not static, but dynamically generated if and only if three hashes stored on the Ethereum blockchain satisfy these properties:

a) The GitHub repo hash matches that of the linked repo (certifying that we’re verifying the right code)

b) The DockerHub container hash matches that of the linked container (certifying that we’re using the right verification tooling)

c) The manifest hash matches that of the displayed manifest (certifying that we’re showing the right verification result)

d) That the manifest shows VerificationSuccess = true

Blockchain commit time — (on-chain timestamp: Ethereum proof)
GitHub / repo hash 6fa654b2124cfe12831fa30a8d062e5b118f4526 (browse tree)
DockerHub / container hash sha256:5babe4d12da24234862a4b95cca8bb36a7be3e70c0f9159aa38b0430d2087bb5
Manifest hash bdf7b92a14a1dff3133eaa06d997d2dd2b0b9d9084f733cc13176d35cf8d037f (SHA-256 of published JSON file)

Running the Verify it yourself script (instructions below) checks that applying the verification tooling (b) to the code (a) reproduces the manifest (c).

To save you time, VeriLib has already auto-run this same script, which produces both pedagogical output to the terminal and the result summary file manifest.json.

We encourage you to not only run this tooling, but also inspect it for correctness. You can build trust in this certificate page by checking the text in green against the manifest, and by noting that the manifest lists as successfully verified all functions in the Specifications section.

Verify it yourself

You do not need to clone any repository. Download the small bash script below using wget or curl. Running it pulls the prebuilt image from Docker Hub and writes the same manifests and lists this page publishes. A full run can take a long time and use significant disk space—plan for that before you start.

  1. Get the script with wget (saves as verify.sh in the current directory):
    wget -O verify.sh https://verilib.org/cert/5171/verify-script

    Same URL with curl: curl -fsSL -o verify.sh https://verilib.org/cert/5171/verify-script

  2. bash verify.sh --cert-verify-url 'https://verilib.org' 'verilib/repo-5171@sha256:5babe4d12da24234862a4b95cca8bb36a7be3e70c0f9159aa38b0430d2087bb5' 'VERIFICATION_RESULTS'

Once you have finished running the script, the file VERIFICATION_RESULTS/manifest.json should match what is shown in the Results section above (downloadable here).

Install Docker

You need a working Docker install before you can pull the certificate image or run the verification script. For the canonical, up-to-date steps (including licensing and system requirements), use Docker’s official guide: Get Docker.

  • macOS: Install Docker Desktop for Mac (Apple Silicon or Intel per your Mac). Open the app from Applications, complete onboarding, and wait until Docker reports “running”. Detailed steps: Install Docker Desktop on Mac.
  • Windows: Install Docker Desktop for Windows. Use WSL 2 backend when prompted. After install, start Docker Desktop and wait until it is ready. Detailed steps: Install Docker Desktop on Windows.
  • Linux: Install Docker Engine (and optionally Docker Compose plugin) for your distribution—do not rely on a random apt package without checking Docker’s repo instructions. Detailed steps: Install Docker Engine (choose your distro: Ubuntu, Debian, Fedora, etc.).

Smoke test: In a terminal, run docker version. You should see both Client and Server sections. If you see docker: command not found, the CLI is not on your PATH yet—restart the terminal or finish Docker Desktop’s setup.

Reproducible Docker image (open source)

Latest certificate: v1 — /cert/5171 and /cert/5171?p=1&c=v1 pin the image below.

The Docker image verilib/repo-5171@sha256:5babe4d12da24234862a4b95cca8bb36a7be3e70c0f9159aa38b0430d2087bb5 on Docker Hub matches this certificate’s published dockerHubImageDigest / manifest image. Use Verify it yourself to pull and run—no clone required.