Introduction

SAPLE — the Symbolic Algebraic Process Logic Engine — is a formal verification framework. It models systems as process equations over a shared state environment and detects vulnerabilities through three complementary techniques:

• Structural pattern matching against abstract behavior signatures (CWE-classified when used for vulnerability detection).
• Concrete symbolic execution against user-provided inputs.
• SMT constraint solving via an SMT solver (Z3 by default; any SMT-LIB-compatible solver can be plugged in) to filter false positives and confirm extracted rules.

The framework consists of a specification language (SPL), a parser, an algebraic core, an analyzer, and a CLI binary called saple.

What SPL models

SPL describes a concurrent system as a collection of:

• Schemas — shared typed state and invariants.
• Transitions — guarded, atomic state updates.
• Agents — process equations over those transitions.
• Systems — composition of agents, properties to verify, and patterns to check.
• Patterns — abstract behavior signatures (a behavior trace plus a constraint), used for vulnerability detection and other property checks.

What SAPLE finds

SAPLE ships with examples that demonstrate detection of:

• Integer overflows (CWE-190), buffer overflows (CWE-787 / CWE-121 / CWE-122 / CWE-805), use-after-free (CWE-416).
• Deadlocks and missed mutual exclusion.
• Reentrancy and race conditions in smart contracts.
• Data races and stale reads in cache-coherence protocols.
• Malformed input acceptance and resource exhaustion in network stacks.

How SAPLE differs from a model checker

Traditional model checkers (SPIN, NuSMV, TLA+) explore reachable states of an explicit state machine. SAPLE works at the level of process equations: behaviors are algebraic terms (prefix ., choice +, parallel ||, iteration *), and analysis proceeds by structural rewriting plus targeted SMT queries. The result is a framework that scales to long traces while preserving algebraic clarity.

Project & language naming

The framework is SAPLE; the language is SPL. The on-disk file extension remains .sbl and the CLI binary remains saple for compatibility with the existing repository.