P0 hardening: axiom audit, Ed25519 certificates, stamp gating, real verify

[nrupala]

Summary

Closes the four P0 ship-blockers from the adversarial strengthen assessment (workspace/certification-authority/strengthen-assessment.md). No certificate may be sold until these are closed — this PR closes them.

Note: this branch is based on remote main. The diff also picks up the previously-unpushed Sept 26 validation work (explicit Lake targets, vacuous-build guard, honesty regression tests) for the touched files, since that was never pushed.

P0-1: Axiom audit (core/prover.py)

• After every successful elaboration, #print axioms runs for each proven theorem (via a temp copy — no module imports needed, works for generated files outside the lakefile's static roots).
• Verification fails closed on any axiom outside Lean's standard set (propext, Quot.sound, funext, Classical.choice). sorryAx is deliberately excluded.
• The axiom sneaky : False → 1 = 2 exploit now reports verified=False, naming the smuggled axiom. Axiom failures are not LLM-repairable — the loop ends honestly.
• The elaboration gate is now lake env lean <file> instead of lake build <module>: Lake cannot address generated modules outside static roots (pre-existing: lake build Algorithms.<name> failed with "unknown target", so run_proof could never verify in the real repo layout). Elaborating the file directly cannot be vacuous.

P0-2: Ed25519 replaces HMAC (core/security.py, core/licensing.py)

• ProofCertificate and LicenseCertificate now use Ed25519. The public verification key is embedded in the certificate and covered by the signature — third parties and agents can verify without a shared secret.
• New Ed25519KeyPair, KeyStore.create_signing_key / load_signing_key; cryptography added to requirements.txt (stdlib-only constraint yields deliberately — hand-rolling Ed25519 would be worse). Module docstrings corrected (no more false "stdlib only" claim).

P0-3: Stamp gating (cli.py extract_python)

• __proof_verified__ = True and "formally verified" language are emitted only when verification_status == "verified". Failed/unverified proofs ship an honest NOT-verified label.

P0-4: Real verify (cli.py)

• cmd_verify / cmd_publish now run verify_certificate_artifact(): Ed25519 signature check → issuer-key binding against the trusted keystore key → fresh Lean elaboration of the stored proof → axiom audit. Fails closed on every uncertainty.
• Tampered certificates fail loudly (SIGNATURE INVALID); publish refuses when verification fails. The lean --c /dev/null theater is gone.

Behavior-test evidence (real toolchain, not mocks)

• Exploit E2E through run_proof: 1 = 2 via smuggled axiom → verified=False, log names sneaky.
• Legitimate proof (2 + 3 = 5 by rfl) → still verified=True.
• verify CLI on genuine cert+proof → VERIFICATION PASSED (signature, issuer binding, fresh elaboration, axiom audit all green).
• verify CLI on tampered cert → SIGNATURE INVALID, exit 1.
• publish CLI on tampered cert → Publish REFUSED, exit 1, nothing published.
• verify CLI on failed-status cert → honest NOT machine-verified, exit 1.
• Third-party verification with public key alone (no secret) → passes.

Test report

• pytest tests/: 167 passed (includes new axiom-smuggling regression test, Ed25519 roundtrip/tamper/wrong-key tests, keystore signing-key roundtrip).
• ruff check + ruff format --check: clean. mypy (CI flags): clean.
• CI: this repo has GitHub Actions (lint, typecheck, tests) — merge only when green.

Out of scope (remain open)

P1/P2 items from the assessment: certificate schema v2 (serial/validity/revocation), migration re-signing, _parse_spec truncation fix, public registry, audit-log signing, AEAD ciphers, batch-artifact labeling, marketing claim audit.

[cloudflare-workers-and-pages]

Deploying axiomcode-site with    Cloudflare Pages

Latest commit:	af58a48
Status:	🚫  Build failed.

View logs