Formal Verification Framework
SAPLE models systems as process equations over a shared state environment and verifies arbitrary properties — safety, liveness, mutual exclusion, custom patterns — through structural pattern matching, symbolic execution, and SMT-based constraint solving.
From GitHub Releases · Install instructions · All releases
What SAPLE does
A specification language (SPL) and an analyzer for verifying arbitrary properties over concurrent systems.
Process algebra
Model systems as schemas, transitions, agents, and behaviour equations. Sequential, choice, parallel, and guarded composition are first-class.
Any property
Safety, liveness, mutual exclusion, deadlock freedom — or your own pattern. Properties are written in SPL alongside the model; nothing is hardcoded.
SMT solving
Constraint satisfiability rules out false positives. Pluggable SMT solver — Z3 by default, any SMT-LIB-compatible backend can be wired in. Symbolic execution checks property violations against concrete or symbolic state.
Rule extraction
Findings become reusable, cross-validated rules — exportable as JSON for downstream tooling or digital-twin integration.
Supported input representations
Translate code from existing formats into SPL and verify it the same way.
x86-64
Assembly → SPL via saple translate ... --arch x86-64.
ARM64 / AArch64
ARM64 assembly (including AArch64 PAO) → SPL via --arch arm64.
Clang IR & VHDL
LLVM/Clang IR for C/C++/Rust front-ends, and VHDL for hardware. --arch clang / --arch vhdl.
Smart contracts
Blockchain contract source → SPL via --arch blockchain.
Example
The classic dining philosophers. Five agents, five forks, three properties to verify.
# Verify safety and liveness of the dining philosophers protocol
saple analyze examples/dining_philosophers.sbl --verbose
# Properties checked:
# noDeadlock : some philosopher can always act
# mutualExclusion : adjacent philosophers never eat simultaneously
# progress : at least one philosopher can eventually eat
# Result: all properties hold across the modelled state space.