Galois has announced new Isabelle support for SAW, enabling generation of Isabelle theories from Cryptol specifications. This integration combines SAW's usability with Isabelle's expressivity for cryptographic protocol verification. The development was done in collaboration with Apple and includes new commands, tactics, and supporting libraries.
Background
SAW (Software Analysis Workbench) is a tool for verifying software and hardware systems, while Isabelle is a popular interactive theorem prover. Cryptol is a domain-specific language for specifying cryptographic algorithms.
- Source
- Lobsters
- Published
- May 23, 2026 at 05:59 AM
- Score
- 7.0 / 10