v1.6.6

Verifpal 1.6.6

Changes since v1.6.5:

• More precise AEAD and forgery semantics
• Engine: Additional fixes and regression tests
• Expand search coverage, rule out more missed attacks
• Fix unlinkability regression reported by Heba Ajjour

Changes since v1.6.4:

• Improve message dropping discipline for guarded messages
• Fix #50
• Performance improvements for multi-phase models
• Clarify remote AA witness expectations
• Clarify private NFC search limits and pin attack traces
• Add private NFC comparisons for remote AA
• Clarify plaintext NFC visibility in the remote AA examples

Changes since v1.6.3:

• Code quality pass
• Cargo update
• Major source refactoring/reorganization
• Search: the rerouted pass bypasses the stuck run's own later send
• Search: the rerouted pass uses only sends that reach past the wait
• Deducer: reuse goals whose cycle cuts recur; fail clashing equations early
• Search: a rerouted send can supply a stuck receive
• Performance improvements
• ePassport models
• Unlinkability fixes
• Cargo update
• Scenario analysis bug found by Heba Ajjour
• Fix #45, #46, #47

Changes since v1.6.2:

• Eliminate classes of missed attacks

Changes since v1.6.1:

• More engine tightening + bug fixes + tests
• Remove vestiges of old engine
• Minor bug fixes + more tests
• Fix #44

Changes since v1.6.0:

• Remove --saturate (closes #43)
• Fix #42
• Fix #38, #39, #40, #41
• Fix #37
• LaTeX rendering improvements
• Fix #32, #33, #34, #35, #36
• Improvements for Verifpal Workbench

Changelog

• 9823fcc: Engine: Additional fixes and regression tests (@nadimkobeissi)
• 7c25b85: Expand search coverage, rule out more missed attacks (@nadimkobeissi)
• c626f1b: Fix unlinkability regression reported by Heba Ajjour (@nadimkobeissi)
• 650f258: More precise AEAD and forgery semantics (@nadimkobeissi)
• f96ea96: More precise AEAD and forgery semantics (@nadimkobeissi)

v1.6.5

Verifpal 1.6.5

Changes since v1.6.4:

• Improve message dropping discipline for guarded messages
• Fix #50
• Performance improvements for multi-phase models
• Clarify remote AA witness expectations
• Clarify private NFC search limits and pin attack traces
• Add private NFC comparisons for remote AA
• Clarify plaintext NFC visibility in the remote AA examples

Changes since v1.6.3:

• Code quality pass
• Cargo update
• Major source refactoring/reorganization
• Search: the rerouted pass bypasses the stuck run's own later send
• Search: the rerouted pass uses only sends that reach past the wait
• Deducer: reuse goals whose cycle cuts recur; fail clashing equations early
• Search: a rerouted send can supply a stuck receive
• Performance improvements
• ePassport models
• Unlinkability fixes
• Cargo update
• Scenario analysis bug found by Heba Ajjour
• Fix #45, #46, #47

Changes since v1.6.2:

• Eliminate classes of missed attacks

Changes since v1.6.1:

• More engine tightening + bug fixes + tests
• Remove vestiges of old engine
• Minor bug fixes + more tests
• Fix #44

Changes since v1.6.0:

• Remove --saturate (closes #43)
• Fix #42
• Fix #38, #39, #40, #41
• Fix #37
• LaTeX rendering improvements
• Fix #32, #33, #34, #35, #36
• Improvements for Verifpal Workbench

Changes since v1.5.2:

• Replace the gate-based engine with joint execution
• Performance pass with five engine improvements

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• 32fbf2e: Add private NFC comparisons for remote AA (@idrassi)
• df59050: Clarify plaintext NFC visibility in the remote AA examples (@idrassi)
• 4fd7628: Clarify private NFC search limits and pin attack traces (@idrassi)
• a63cd15: Clarify remote AA witness expectations (@idrassi)
• 2d7b183: Fix #50 (@nadimkobeissi)
• 9039059: Improve message dropping discipline for guarded messages (@nadimkobeissi)
• 43e48bc: Performance improvements for multi-phase models (@nadimkobeissi)
• 894c119: Simplify README.md (@nadimkobeissi)
• c09b040: Simplify README.md (@nadimkobeissi)

v1.6.4

Verifpal 1.6.4

Changes since v1.6.3:

• Code quality pass
• Cargo update
• Major source refactoring/reorganization
• Search: the rerouted pass bypasses the stuck run's own later send
• Search: the rerouted pass uses only sends that reach past the wait
• Deducer: reuse goals whose cycle cuts recur; fail clashing equations early
• Search: a rerouted send can supply a stuck receive
• Performance improvements
• ePassport models
• Unlinkability fixes
• Cargo update
• Scenario analysis bug found by Heba Ajjour
• Fix #45, #46, #47

Changes since v1.6.2:

• Eliminate classes of missed attacks

Changes since v1.6.1:

• More engine tightening + bug fixes + tests
• Remove vestiges of old engine
• Minor bug fixes + more tests
• Fix #44

Changes since v1.6.0:

• Remove --saturate (closes #43)
• Fix #42
• Fix #38, #39, #40, #41
• Fix #37
• LaTeX rendering improvements
• Fix #32, #33, #34, #35, #36
• Improvements for Verifpal Workbench

Changes since v1.5.2:

• Replace the gate-based engine with joint execution
• Performance pass with five engine improvements

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• ab0b702: Cargo update (@nadimkobeissi)
• 9d88b16: Cargo update (@nadimkobeissi)
• e5762e4: Code quality pass (@nadimkobeissi)
• 6acd799: Deducer: reuse goals whose cycle cuts recur; fail clashing equations early (@nadimkobeissi)
• 67ce380: Fix #45, #46, #47 (@nadimkobeissi)
• f9dd68c: Major source refactoring/reorganization (@nadimkobeissi)
• 23a2dd3: Performance improvements (@nadimkobeissi)
• 5962ede: Scenario analysis bug found by Heba Ajjour (@nadimkobeissi)
• 7a308d4: Search: a rerouted send can supply a stuck receive (@nadimkobeissi)
• 8c568a9: Search: the rerouted pass bypasses the stuck run's own later send (@nadimkobeissi)
• 4ba3d77: Search: the rerouted pass uses only sends that reach past the wait (@nadimkobeissi)
• 3dc377f: Unlinkability fixes (@nadimkobeissi)
• 0de4233: ePassport models (@nadimkobeissi)

v1.6.3

Verifpal 1.6.3

Changes since v1.6.2:

• Eliminate classes of missed attacks

Changes since v1.6.1:

• More engine tightening + bug fixes + tests
• Remove vestiges of old engine
• Minor bug fixes + more tests
• Fix #44

Changes since v1.6.0:

• Remove --saturate (closes #43)
• Fix #42
• Fix #38, #39, #40, #41
• Fix #37
• LaTeX rendering improvements
• Fix #32, #33, #34, #35, #36
• Improvements for Verifpal Workbench

Changes since v1.5.2:

• Replace the gate-based engine with joint execution
• Performance pass with five engine improvements

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• e2ae943: Eliminate classes of missed attacks (@nadimkobeissi)

v1.6.2

Verifpal 1.6.2

Changes since v1.6.1:

• More engine tightening + bug fixes + tests
• Remove vestiges of old engine
• Minor bug fixes + more tests
• Fix #44

Changes since v1.6.0:

• Remove --saturate (closes #43)
• Fix #42
• Fix #38, #39, #40, #41
• Fix #37
• LaTeX rendering improvements
• Fix #32, #33, #34, #35, #36
• Improvements for Verifpal Workbench

Changes since v1.5.2:

• Replace the gate-based engine with joint execution
• Performance pass with five engine improvements

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• 5bc5ab7: Fix #44 (@nadimkobeissi)
• e5504dc: Minor bug fixes + more tests (@nadimkobeissi)
• f713833: More engine tightening + bug fixes + tests (@nadimkobeissi)
• 55fff91: Remove vestiges of old engine (@nadimkobeissi)

v1.6.1

Verifpal 1.6.1

Changes since v1.6.0:

• Remove --saturate (closes #43)
• Fix #42
• Fix #38, #39, #40, #41
• Fix #37
• LaTeX rendering improvements
• Fix #32, #33, #34, #35, #36
• Improvements for Verifpal Workbench

Changes since v1.5.2:

• Replace the gate-based engine with joint execution
• Performance pass with five engine improvements

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• ecfb26a: Fix #32, #33, #34, #35, #36 (@nadimkobeissi)
• 02f5c39: Fix #37 (@nadimkobeissi)
• eac587a: Fix #38, #39, #40, #41 (@nadimkobeissi)
• da6a352: Fix #42 (@nadimkobeissi)
• d151157: Improvements for Verifpal Workbench (@nadimkobeissi)
• 8530d85: LaTeX rendering improvements (@nadimkobeissi)
• a85b9bf: Remove --saturate (closes #43) (@nadimkobeissi)
• 35b6bd6: Remove debug line (@nadimkobeissi)

v1.6.0

Verifpal 1.6.0

Changes since v1.5.2:

• Replace the gate-based engine with joint execution
• Performance pass with five engine improvements

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• 34f0c21: Performance pass with five engine improvements (@nadimkobeissi)
• f025edc: Replace the gate-based engine with joint execution (@nadimkobeissi)
• 0b01651: Restore some narrator improvements (@nadimkobeissi)
• 0180a16: Restore some narrator improvements (cont.) (@nadimkobeissi)
• 7e21f4a: Restore some narrator improvements (cont.) (@nadimkobeissi)
• 547b87d: Update CLAUDE.md (@nadimkobeissi)

v1.5.2

Verifpal 1.5.2

Changes since v1.5.1:

• Fix: guarded downstream forward lost a duplicate acceptance
  Found by Heba Ajjour, University College of Applied Sciences, Gaza, Palestine.
• Performance audit + minor bug fixes

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• d0969fd: Fix: guarded downstream forward lost a duplicate acceptance (@nadimkobeissi)
• 4c7a4da: Performance audit + minor bug fixes (@nadimkobeissi)

v1.5.1

Verifpal 1.5.1

Changes since v1.5.0:

• Performance optimization pass
• Validate concrete replay witnesses and preserve execution constraints [ci]

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• 9546906: Performance optimization pass (@nadimkobeissi)
• 827c079: Remove junglegym_threshold_ring.vp (@nadimkobeissi)
• 7259772: Validate concrete replay witnesses and preserve execution constraints [ci] (@nadimkobeissi)

v1.5.0

Verifpal 1.5.0

Changes since v1.4.12:

• Verifpal 1.5 focuses on the correctness of the verifier itself.
  We used frontier AI models to audit the engine, reproduce errors
  in small protocol models, and develop fixes.
  Read the full blog post:
  https://symbolic.software/blog/2026-09-20-verifpal-1-5/

Changelog

• b9b7964: Claim a guard was bypassed upstream only where an unguarded hop exists (@nadimkobeissi)
• 5007395: Fix four more classes of missed and false attacks, one of them a crash (@nadimkobeissi)
• da733b8: Fix seven classes of missed and false attacks found by auditing the engine (@nadimkobeissi)
• b579fc2: Fix six more classes of missed and false attacks found by auditing the engine (@nadimkobeissi)
• e326cfb: Give every learned value the executions that produce it (@nadimkobeissi)
• fe92ada: Judge a query's preconditions in the execution that produced the violation (@nadimkobeissi)
• 8e6287f: cargo update (@nadimkobeissi)