SpecMon Logo SpecMon

Verify. Monitor. Trust.

The runtime monitor that uses your formal specifications directly. What you verify is what you enforce.

Get Started GitHub GitHub

Your Specification
Is The Monitor.

Don't rewrite your specs. SpecMon ingests your existing Tamarin files directly. What you verify is exactly what we enforce. No translation errors. No divergence.

Runtime
Enforcement.

Detect violations in real-time. Whether it's a logic bug or a malicious attack, SpecMon catches it.
  • ✓ Frida or library integration
  • ✓ Negligible overhead
  • ✓ Instant alerts

Proven at Scale

Monitored WireGuard VPN in production conditions
100+ Concurrent clients
<16ms Latency
1 Unified specification

Explore SpecMon

Quick Start Monitor your first protocol in minutes with a hands-on tutorial.
Specification Basics Learn to write specifications using multiset-rewrite rules.
Unified Models Create specifications that work for both Tamarin verification and SpecMon monitoring.
Founded in Research
ACM CCS 2024 arXiv Artifact
Built at CISPA Helmholtz Center for Information Security