Skip to content

R4 — the VerInf demo

Choose a tag to compare

View all tags
@levineuwirth levineuwirth released this 05 Sep 21:39
· 1 commit to main since this release
r4
This tag was signed with the committer’s verified signature.
levineuwirth Levi Neuwirth
SSH Key Fingerprint: 6qqOcmELc9a91Bl8g4EymWRWXkIHKNxQ+BsbhGDC/ms
Verified
Learn about vigilant mode.
c3bcf23
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Proof Broker closes 19/19 targeted Lean obligations in a real downstream consumer — VerInf's softmax-bracket spike, statements untouched. External search (cvc4 / cvc5 / z3), every certificate checked before Lean accepts the result, everything within the sanctioned axiom ceiling.

Evidence and generated tables: proof-broker-demo · write-up · decision records: delta.md §5.7.

Assets 2
Loading