ABC (Artifact Behavioral Certificate)

An ABC binds admitted behavioral claims about selected exports to the exact WebAssembly bytes supplied to the verifier. The standalone aver-cert checks those claims under its embedded Lean 4.32 wall and emits CERTIFIED after the fixed proof root, axiom audit, and fresh kernel replay succeed.

aver-cert 0.1.x package 1 schema 4 Lean 4.32 CERTIFIED or decline

The exact artifact

The .wasm file passed to aver-cert determines the artifact identity. The verifier validates the module, computes its SHA-256, and generates ArtifactBytes.lean from the bytes it actually read. A certificate package cannot supply replacement artifact bytes, checker files, a toolchain, or a soundness wall.

aver-cert is a standalone crate and executable with an independently versioned 0.1.x release line. It has no dependency on aver-lang, aver-rt, or aver-memory. The compiler and certificate producer are outside the verifier's positive acceptance path.

ABC acceptance path

Any mismatch produces a decline. Diagnostics identify the failing gate.

  1. 01
    Read the module

    Validate WebAssembly, compute SHA-256, and parse the package envelope.

  2. 02
    Pin the format

    Require package 1, schema 4, the actual hash, and an embedded wall_id.

  3. 03
    Build a fresh checker project

    Materialize the checker-owned wall, Lean 4.32 toolchain, build files, and witness.

  4. 04
    Recover artifact facts

    Generate ArtifactBytes.lean; decode the relevant functions, types, and code bytes.

  5. 05
    Check and lower plans

    Validate Plans.lean, derive canonical bodies, then run StandardFace and ClaimAxes.

  6. 06
    Check the fixed root

    Pin the report through AverCertChecker.checked and audit its axiom closure.

  7. 07
    Replay in a fresh environment

    Run lake env leanchecker --fresh, then construct the CERTIFIED report.

ABC verification record

Verifier Standalone aver-cert, release line 0.1.x
Public package Format version 1
Statement Schema version 2
Plan authority Plans.lean
Artifact bytes Supplied by the caller; encoded by the verifier
Soundness wall Checker-owned and selected by exact wall_id
Toolchain Pinned Lean 4.32, resolved through Elan
Public proof root AverCert.Artifact.certificate
Checker root AverCertChecker.checked
Allowed axioms propext, Classical.choice, Quot.sound
Strict result CERTIFIED or decline

Generate and verify an ABC

cargo install aver-lang --features wasm
cargo install aver-cert

aver compile app.av --target wasm-gc --certify -o out/
aver-cert verify out/app.wasm out/cert
aver-cert explain out/app.wasm out/cert

aver cert verify and the other aver cert commands are exact subprocess shortcuts. They forward arguments, standard streams, and exit status to a sibling aver-cert executable or one found on PATH.

What an ABC establishes

AverCert.Artifact.certificate :
  AverCert.AcceptedArtifact.accepted AverCert.Artifact.data

A successful verification establishes that:

  • the proof concerns the exact bytes supplied to aver-cert;
  • each certified export has an admitted class with its standard domain, codomain, representation relations, host behavior, and model constraints;
  • policy, termination evidence, totality role, and runtime contracts are derived canonically from checked plans;
  • exports, imports and capabilities, the start function, and the reachable certified call surface are accounted for;
  • the named proof root uses only the allowed Lean axiom whitelist.

ABC certification levels

Level Policy Guarantee
L1 simulatesModel If evaluation returns, the value is represented by the declared model result. Named runtime contracts remain explicit premises.
L3 simulatesModelTotally Simulation is total for admitted inputs, using Lean-derived termination evidence and the required total runtime contracts.

ABC package and schema

The public package format is version 1 and its certificate statement schema is version 2. The package is untrusted input throughout verification.

cert-manifest.json Transport and reporting envelope; it carries versions, artifact hash, wall identity, report candidates, and declared uncertified exports.
Plans.lean The sole authoritative plan data; structurally checked and canonically lowered in Lean.
Model and proof modules Artifact-specific, untrusted proof data admitted through staging, pinning, and kernel checks.
ArtifactBytes.lean Absent from the package; regenerated by the verifier from the supplied .wasm.
Plan sidecars No public fragments/*.plan files and no authoritative JSON plan AST.

ABC scope and trust boundary

Scope boundaries

  • Behavioral claims apply to admitted obligations and their certified closure, not every export in the module.
  • An ABC is not a signature, authorship claim, or reproducible-build attestation.
  • Source meaning erased by WebAssembly, including user-ADT domain, representation, and model declarations, remains an explicit premise.
  • Trace and replay recordings do not participate in plan selection, theorem construction, or the verdict.
  • leanchecker --fresh belongs to the same Lean 4.32 distribution; the architecture does not claim two independently implemented kernels.

Trusted computing base

A successful ABC verdict depends on:

  • the small standalone verifier path for file I/O, hashing, version checks, safe staging, process execution, and report pinning;
  • wasmparser::Validator for complete WebAssembly validity;
  • the exact embedded Lean wall and Lean 4.32 elaborator, kernel, and build tools;
  • the canonical Elan installation used to resolve the pinned toolchain;
  • SHA-256 collision resistance, named runtime contracts, explicit source declarations, and any configured local build cache.

The positive verdict does not run or trust the Aver compiler, optimizer, producer classifier, disassembler, or Rust obligation rederivation. The retained Rust WebAssembly validator remains necessary because the Lean wall's decoder is not a complete WebAssembly validation stack.

ABC specifications