File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -98,10 +98,10 @@ Despite end-to-end verification, three low-probability sources of error remain:
9898 developed as an integrated tactic for Lean and thus does not natively support the SMT-LIB format.
9999 To use it in SMT-COMP, we developed a wrapper called `leanwuzla` @leanwuzla that translates
100100 SMT-LIB queries into Lean propositions for `bv_decide` to decide. This wrapper is not formally verified.
101- However, extensive testing on SMT-LIB 2024 provides high confidence in its correctness.
101+ However, extensive testing on SMT-LIB 2025 provides high confidence in its correctness.
102102
1031032. *Compiler Bugs* in Lean 4, which might produce a binary misaligned with source semantics.
104- Again, successful runs on SMT-LIB 2024 benchmarks offer indirect validation.
104+ Again, successful runs on SMT-LIB 2025 benchmarks offer indirect validation.
105105
1061063. *Kernel Unsoundness* , which could undermine proof checking. The Lean kernel follows the De Bruijn criterion
107107 @barendregt2005challenge and has a small, audited codebase, making serious soundness failures extremely unlikely.
You can’t perform that action at this time.
0 commit comments