fix: audit formal-verif honesty — relabel admits, run bazel test#99
Merged
Conversation
Closes 5 findings from the 2026-04-30 audit. Does NOT discharge any proof
obligation; relabels existing admits as specifications and tightens the
CI gate so the next dishonesty is caught.
C-1 — annotate Verus assume(false) sites as SPECIFICATION ONLY
C-2 — fix Lean status table to match sorry'd proof bodies
C-3 — add verification/rocq/README.md stating it's an unrealised stub
C-7 — Bazel CI now runs bazel test //...; remove continue-on-error
from formal-verif jobs that pass
M-9 — add paths filter to rust.yml so docs-only PRs skip cargo/bazel
Fixes: C-1, C-2, C-3, C-7, M-9
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 tasks
The original PR-D classified Verus + Kani matrix jobs as "passing" and removed continue-on-error: true. CI showed they were not actually passing — the previous greens were masking-as-success. Re-add the mask on a per-job basis with explicit WIP comments tying each masked job to its blocking audit finding (C-1 for Verus admits, C-7 for the new bazel-test step). Rocq remains masked as before (audit C-3). Net effect for audit C-7: partial closure. The mask is now per-job and documented; ungating happens as proofs are discharged. Honesty is in the labelling, not yet in the gate strength. Trace: skip Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 30, 2026
Bumps Cargo.toml, MODULE.bazel, src/cli/BUILD.bazel, and Cargo.lock to 0.8.1. Adds CHANGELOG.md (new file, repo did not have one) with the full release notes. This release closes 26 of 33 findings from the 2026-04-30 14-perspective audit. Specific fix-PRs are #96 (STPA-Sec / docs), #97 (hygiene), #98 (parser hardness), #99 (formal-verif honesty + CI), #100 (keyless / OIDC hardening). Two findings (cert-pinning enforcement, no_std verifier) are deferred to issue #95 and issue #79 respectively. Note on H-8 (version drift): MODULE.bazel and src/cli/BUILD.bazel were at 0.2.7 on main; this commit takes them straight to 0.8.1. PR #97 also bumps these to 0.8.0 as part of its H-8 fix; whichever PR merges last has a trivial conflict that resolves to 0.8.1. Trace: skip Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
May 1, 2026
Bumps Cargo.toml, MODULE.bazel, src/cli/BUILD.bazel, and Cargo.lock to 0.8.1. Adds CHANGELOG.md (new file, repo did not have one) with the full release notes. This release closes 26 of 33 findings from the 2026-04-30 14-perspective audit. Specific fix-PRs are #96 (STPA-Sec / docs), #97 (hygiene), #98 (parser hardness), #99 (formal-verif honesty + CI), #100 (keyless / OIDC hardening). Two findings (cert-pinning enforcement, no_std verifier) are deferred to issue #95 and issue #79 respectively. Note on H-8 (version drift): MODULE.bazel and src/cli/BUILD.bazel were at 0.2.7 on main; this commit takes them straight to 0.8.1. PR #97 also bumps these to 0.8.0 as part of its H-8 fix; whichever PR merges last has a trivial conflict that resolves to 0.8.1. Trace: skip Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 1, 2026
Bumps Cargo.toml, MODULE.bazel, src/cli/BUILD.bazel, and Cargo.lock to 0.8.1. Adds CHANGELOG.md (new file, repo did not have one) with the full release notes. This release closes 26 of 33 findings from the 2026-04-30 14-perspective audit. Specific fix-PRs are #96 (STPA-Sec / docs), #97 (hygiene), #98 (parser hardness), #99 (formal-verif honesty + CI), #100 (keyless / OIDC hardening). Two findings (cert-pinning enforcement, no_std verifier) are deferred to issue #95 and issue #79 respectively. Note on H-8 (version drift): MODULE.bazel and src/cli/BUILD.bazel were at 0.2.7 on main; this commit takes them straight to 0.8.1. PR #97 also bumps these to 0.8.0 as part of its H-8 fix; whichever PR merges last has a trivial conflict that resolves to 0.8.1. Trace: skip Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes 4 of 5 originally-targeted findings + partial closure of C-7. No new proofs added — this PR is about honesty and gate clarity.
Findings closed in this PR
theorem_*-named functions ending inassume(false)are now annotated as SPECIFICATION ONLY insrc/lib/src/verus_proofs/dsse_proofs.rsandmerkle_proofs.rs. Doc comments above each admit explain what the open proof obligation is.lean/Ed25519.leanstatus table corrected.verification_equation_completeandbasepoint_prime_ordernow marked assorry/ open.verification_equation_sound(proven) unchanged.verification/rocq/README.mdclearly states the directory holds Rust extraction stubs; no.vfiles have been written.rust.ymlgainspaths:filters so doc-only changes don't fire the cross-OS cargo + bazel matrix.C-7 partial closure
Original plan was to remove
continue-on-error: truefrom formal-verif jobs that "pass", and addbazel test //...to the Bazel CI step. CI showed the assumption was wrong: the formal-verif jobs were not passing — the previous greens were masking-as-success. The amendment commit (ci: amend audit C-7 — partial closure with explicit WIP labels) re-adds the mask per job with explicit comments tying each to its blocking audit finding:continue-on-error: true # WIP — see audit C-1continue-on-error: true # WIP — see audit C-7 partial closure(varint and dsse pass; format/merkle/wasm_module fail; ungate selectively in a follow-up)continue-on-error: true # WIP — see audit C-3(unchanged from main)bazel test //...step in rust.yml:continue-on-error: true # WIP — see audit C-7 partial closureNet audit C-7 effect: the mask is now per-job and documented, not blanket. Each masked job names which finding makes it WIP. Ungating becomes a tracked task per finding rather than a sea of red.
What this PR does NOT do
continue-on-errormask globally — only renames it from "blanket coverup" to "audited list of WIP items".Test plan
cargo build --workspace --releasecleancargo test --workspace --no-runcleanAudit context:
audit/2026-04-30/findings.md. Companion PRs: #96, #97, #98, #100. Capstone: #101.