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

Formal Verification Certificate

nasa jpl test — 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 June 8, 2026
Package commit 10aa277
Functions Verified 0/0
Ethereum Proof Etherscan
Package Summary
GitHub VeriLib
Specifications

An easier way to view the specifications is to click on the corresponding functions in VeriLib.

Assumptions
fact_check
Verus Verifier

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

bug_report
Z3 SMT Solver

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

view_in_ar
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.

computer
Hardware

Like for any software, we assume trust that the hardware correctly executes the compiled machine code.

show_chart
Cryptographic Assumptions

We assume the mathematical foundations of elliptic curve cryptography, including the hardness of the discrete logarithm problem on Curve25519.

rule
Known Properties

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

inventory_2
Dependencies

We assume correctness of the dependencies listed in the Cargo.toml file: subtle, zeroize, sha2 and the Verus standard library.

extension
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.

Verification Results

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

Manifest
{
  "VerificationSuccess": true,
  "branch": "main",
  "build_arg_commit": "10aa27768f5bcfb5e42bce921a661c47e5bfd28f",
  "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/5190",
  "commit": "10aa27768f5bcfb5e42bce921a661c47e5bfd28f",
  "commit_date_utc": null,
  "image": "verilib/probe-lean-repo-5190:1",
  "image_build_date_utc": "2026-06-08T15:12:31Z",
  "probe_extract_completed_at_utc": "2026-06-08T15:12:31Z",
  "probe_lean_version": "0.7.0",
  "repo": "https://github.com/nasa-jpl/L4YAML.git",
  "source_tree_sha256": "6311961c2ff7afe7ce75edde7718b709e183f6cbdc7f316917d6007a458cd280",
  "to_be_verified": 0,
  "unified_extract_json_path": "probe_extract.json",
  "unified_extract_json_sha256": "a719b8f2130c511e7a49ddb1e210c4ba033d3a19c555345eb85710cdd3573adb",
  "verification_source": "unified_extract_json",
  "verified_functions": [],
  "verified_functions_count": 0
}
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 10aa27768f5bcfb5e42bce921a661c47e5bfd28f (browse tree)
DockerHub / container hash sha256:727ddd20fd32287334008e340ce93b698fac4256a9191de72126009503f2a015
Manifest hash aa3f2d8f226880bfe6f03d9970d64685b6b2794956e4b8978e7c45d480956954 (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/5190/verify-script

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

  2. bash verify.sh --cert-verify-url 'https://verilib.org' 'verilib/probe-lean-repo-5190@sha256:727ddd20fd32287334008e340ce93b698fac4256a9191de72126009503f2a015' '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/5190 and /cert/5190?p=1&c=v1 pin the image below.

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