Skip to content

v5.3.0 — SymbolicVerifier: DiagnosticResult Reference Implementation

Latest
Marketplace
Latest
Marketplace

Choose a tag to compare

View all tags
@rahuldass19 rahuldass19 released this 25 Jul 16:44
v5.3.0
9bc17d4
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

v5.3.0 — SymbolicVerifier: DiagnosticResult Reference Implementation

SymbolicVerifier is the first fully DiagnosticResult-conformant verification engine and serves as the reference implementation for future engine migrations. The unified diagnostic model is no longer aspirational — one of 13 engines now demonstrates the complete pattern.

Completed (Phase 1 + Phase 2, META #216)

  • Phase 1 — 6 public methods migrated to DiagnosticResult: verify_code, verify_function_contract, verify_safety_properties, verify_bounded, analyze_complexity, get_verification_budget
  • Phase 2 — All internal code paths produce AdvisoryCheck for non-proof-bearing analysis; developer_fields provides structured evidence; verification_mode field tracks bounded vs. unbounded analysis across every return path
  • Fail-closed math bugs (#129-#131) — All three resolved, ensuring safety constraints always block when out of budget
  • Key rotation (#224) — Secure PBKDF2-based key attestation rotation

Version Propagation

  • qwed (PyPI): 5.2.0 -> 5.3.0
  • qwed_sdk (Python): 5.2.0 -> 5.3.0
  • @qwed-ai/sdk (NPM): 5.2.0 -> 5.3.0
  • qwed (crates.io/Rust): 5.2.0 -> 5.3.0
  • API version marker: 5.2.0 -> 5.3.0
  • Docker images: 5.2.0 -> 5.3.0

Ecosystem Status

  • 1 of 13 engines conformant — SymbolicVerifier as reference implementation
  • Remaining engines tracked under META #216 (12 engines + security hardening + attestation consumption)
  • Open audit issues: #162-#164 (Logic/Graph/Reasoning), #205 (SecureCodeExecutor), #221-#231 (security hardening), #191 (attestation consumption)

Included PRs

Core: SymbolicVerifier Migration (Phase 1 + Phase 2)

  • #212 feat: migrate SymbolicVerifier to DiagnosticResult (Phase 1)
  • #239 feat: add verification_mode to SymbolicVerifier DiagnosticResults
  • #240 feat: migrate verify_bounded to return DiagnosticResult
  • #241 feat: migrate get_verification_budget to return DiagnosticResult
  • #242 feat: migrate analyze_complexity to return DiagnosticResult
  • #243 feat: migrate verify_safety_properties to return DiagnosticResult

Fail-Closed Bug Fixes (Math)

  • #217 fix(math): fail-closed on ambiguous mode (#129)
  • #218 fix(math): require eigenvalue cardinality match (#130)
  • #219 fix(math): require IRR convergence proof (#131)

Security & Key Rotation

  • #220 fix: remove unused check_assertions parameter from verify_code
  • #232 fix: use PBKDF2 instead of raw SHA-256 for key rotation hashing

Code Quality & Tooling

  • #208 docs: archive stale docs, update DEPLOYMENT.md
  • #209 docs: sync README with v5.2.0 codebase
  • #210 fix: code scanning alert no. 515 — Log Injection
  • #211 fix: replace polynomial regex with O(n) str.find loop
  • #213 fix: silence CodeQL false positives in security demo
  • #215 Add GitLab badge to README

Release Infrastructure

  • #244 release: v5.3.0-pre — version bumps, README reframe, CHANGELOG

Changelog

https://github.com/QWED-AI/qwed-verification/blob/main/CHANGELOG.md#530---2026-07-25

Assets 3
Loading