All required criteria passed for the exact source tree built and verified by FalseGreen.
This does not prove universal correctness. Assurance is limited to the explicit formal properties, assumptions, models, summaries, and scope recorded in this report.
chain linking is exact successor arithmetic and never wraps at the u64 ceiling — formal-proofs, floor-green, both-rungs-proven
Plan (frozen)
Objective
Verify the open-source falsegreen-ledger program exactly as published: the mechanical floor (release build, full offline test suite, clippy -D warnings, rustfmt) as frozen criteria, and one frozen claim — chain linking is exact successor arithmetic and never wraps at the u64 ceiling — carried by two formal encodings the machines discharge (Kani bounded over the shipped src/rules.rs arithmetic; an unbounded Creusot Why3 proof of the guarded Pearlite spec in src/spec.rs over both translated items).
the program builds, tests, lints and formats clean offline, exactly as published
-
a proof-only claim carried without the mechanical floor would leave the shipped binary itself unverified
formal-proofs
the chain-link claim is discharged by both formal encodings on the published source
mechanical-floor
the encodings encode the claim as read at freeze time — the encoding↔claim equivalence is the frozen human judgement the report exposes verbatim
Acceptance conditions, and the evidence that decides each:
Scope
Condition
Evidence
mechanical-floor
every frozen criterion passes on the published source: release build, the full test suite, clippy with -D warnings, rustfmt check
build, behavioral-test, static-analysis, build
formal-proofs
the Kani rung returns proven over the shipped arithmetic (no counterexample), and the Creusot rung closes every verification condition for the frozen targets (measured: 4/4 obligations, incl. the shipped rule's u64-addition safety obligation)
proof, proof
overall
the published program is accepted: all four criteria green AND both proof rows proven, in one attempt, with the per-obligation prover disclosure and verbatim clauses in the signed report
Each entry is ONE frozen claim, the PROVER that worked on it, and the formal proposition that prover was asked to discharge — read out of the frozen encoding, so the machine's text sits next to the author's sentence. The full rows (any counterexample trace, the admitted assumptions) are in the signed JSON report.
Attempt #1
chain linking is exact successor arithmetic and never wraps at the u64 ceiling
PROVEN
“record N links to record N-1 iff prev_hash equals record N-1's hash AND seq is the exact u64 successor of record N-1's seq; the successor is never taken modulo the u64 ceiling — no seq may link past u64::MAX (the chain cannot wrap) — and on the guarded domain (prev below u64::MAX) the predicate is exactly seq == prev + 1”
chain linking is exact successor arithmetic and never wraps at the u64 ceiling
PROVEN 4 / 4
“record N links to record N-1 iff prev_hash equals record N-1's hash AND seq is the exact u64 successor of record N-1's seq; the successor is never taken modulo the u64 ceiling — no seq may link past u64::MAX (the chain cannot wrap) — and on the guarded domain (prev below u64::MAX) the predicate is exactly seq == prev + 1”
89 components inventoried (evidence, in the signed JSON report)
License policy
yes
NOT ASSESSED
no licence policy frozen — the licence facts are inventory, nothing was asserted · 88 licence facts inventoried (evidence, in the signed JSON report)
How to read this table.PASS — the evidence was collected and nothing in it violated the frozen policy. FAIL — the evidence showed a violation the policy forbids; that alone fails the Job. INSUFFICIENT EVIDENCE — the evidence could not be collected, or could not be decided for a reason outside the code (a stale snapshot, an unavailable tool, output the parser could not read). It is never a pass, and it holds the Job at insufficient_evidence rather than accepting it. NOT ASSESSED — no policy is frozen for this class, so nothing was asserted about it; the facts are recorded as inventory and the class does not hold the Job. The findings table lists only what the frozen policy JUDGED — a graded severity, supply-chain drift, or a licence breaking the frozen policy. Everything else the tools recorded (components, licence facts) is inventory: not a finding, counted on the class row above, kept in the signed JSON report. A finding is OPEN unless it is resolved, not affected, or covered by a recorded exception.
Attempt security history (the full per-attempt sections are in the signed JSON report):
Full content is embedded in the signed JSON report (report schema v13).
spdx-3.0 sha256:b0d1a45bd3f26e73a0d907549a605ab07a7e846d4e2352eb94d798a0b7582a3d embedded in the JSON report (66947 bytes)
cyclonedx-1.7 sha256:8a23b906c0d49c0932df91526ca4734e1a40ba84ca8d1ff29b88faba692394ec embedded in the JSON report (32209 bytes)
cyclonedx-1.7-vex sha256:bcb2993e5908166bc0f99215bf7e14bf48ad76f3081437da4e42b9f19fd8ae7b embedded in the JSON report (632 bytes)
Signature
This report is cryptographically signed: Ed25519 over the canonical report content. The public key is embedded in the report — verification is offline and registry-free (falsegreen verify-report).
