Squirrel: Computationally sound symbolic proofs
===============================================

Squirrel proves protocol security in a symbolic-looking logic whose results are computationally sound, bridging the gap between Tamarin-style automation and EasyCrypt-style guarantees.

Maintainer: Inria (Bana-Comon logic)
Website: https://squirrel-prover.github.io
Category: Proof systems and computational proofs
Targets: Protocols
Approach: Interactive prover in the computationally complete symbolic attacker model
Access: Open source
Status: Active research
Strengths: Computational soundness with symbolic ergonomics. | Interactive control.
Limits: Research maturity. | Small community. | Limited primitives.
Firms using it: none listed
Sources: https://squirrel-prover.github.io

Source page: https://sorryfree.com/frameworks/squirrel/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13