A follow-up. The previous article described what we are building. This one describes how it works in practice - and why the shift from academic tool to industrial platform matters.
In a previous article, I described the architecture of a protocol analyzer we are building: automatic repair, sixteen attacker models, GNN-guided search, modular crate design. That was the "what." This article is the "how" - how this tool gets used, what it changes in practice, and why we believe it represents a shift from laboratory instrument to industrial platform.
ProVerif and Tamarin are remarkable achievements in formal methods. They are also laboratory instruments by design. You install them on a research machine, write a model in their DSL, run analysis in a terminal, read the output. This workflow is fine for a PhD student. It does not work for a security engineer at a company that ships TLS implementations.
The gap concerns where these tools live in the development lifecycle, not what they can prove. Existing tools sit outside CI pipelines, outside IDEs, outside deployment workflows. They are consulted - if at all - after a protocol is designed, before it ships. Rarely during development, rarely after deployment.
We are building something that lives inside the lifecycle.
CI/CD integration: verify on every commit
The analyzer ships as a GitHub Action. Every time a protocol description changes - a new message flow, a modified key exchange, an added authentication step - the analyzer runs automatically. It checks whether the change introduces a vulnerability. If it does, the action fails with a concrete attack trace and a proposed fix.
This is not a theoretical capability. The action is designed to run in minutes on standard CI hardware, not hours on a research cluster. The performance targets we described in the previous article - 10x to 50x speedup, sub-ten-minute analysis for real-world protocols - exist to make this practical. A tool that takes six hours to analyze a protocol cannot run in CI. One that takes six minutes can.
Beyond GitHub Actions, the analyzer provides a CLI that integrates with any CI system - GitLab CI, Jenkins, Buildkite. The output is machine-readable: SARIF for security scanners, JSON for custom pipelines, JUnit XML for test reporting. Protocol verification becomes another test suite in the pipeline.
IDE integration: find vulnerabilities while you write
The analyzer ships a Language Server Protocol (LSP) implementation. In a VS Code editor, this means: syntax highlighting for the protocol DSL, inline error reporting as you type, hover documentation for security properties, and one-click analysis from the editor.
The experience is analogous to writing Rust with rust-analyzer: the tool understands what you are writing and gives feedback in real time. When you define a key exchange step, the analyzer checks whether the key material is properly authenticated. When you add a new message, it checks whether the freshness guarantees hold. The vulnerability is flagged before you commit the code - not after.
Real-time analysis: the daemon and the sniffer
This is where the tool stops being a verifier and becomes a platform.
The analyzer runs as a background daemon with a gRPC API. Any service in the infrastructure can send a protocol description and receive analysis results. But the daemon does more than wait for requests - it listens to live traffic.
The sniffer module captures network traffic (PCAP), reconstructs protocol sessions from packet streams, and feeds them to the symbolic engine in real time. When a TLS handshake happens on the network, the analyzer checks whether that handshake - with its specific cipher suite, extensions, and parameters - satisfies the security properties. When an unusual pattern appears - a repeated nonce, an unexpected message order, a downgrade attempt - it flags the anomaly.
This is live verification - analysis that runs while the protocol is executing, not after the fact.
The real-time constraint changes the engineering at its core. Traditional protocol analysis explores the full state space - every possible interleaving, every attacker action. That takes hours. Real-time analysis uses a bounded model: explore the state space up to depth N, report what you find, continue monitoring. The GNN-guided search from our previous article is critical here - it prioritizes the most promising exploration paths, finding attacks faster in bounded time.
Web interface: collaboration, not just output
The analyzer ships a web UI. This is a requirement for adoption, not a luxury.
Security review is a collaborative process. An analyst finds an attack, a protocol designer evaluates the proposed fix, a manager decides whether the risk is acceptable. In existing tools, this workflow happens outside the tool: screenshots in Slack, traces in emails, decisions in meetings.
The web UI makes the analysis itself collaborative. Attack graphs are rendered in 3D - navigable, zoomable, inspectable. Repair proposals are presented side-by-side with the original protocol, with the differences highlighted. Reviewers can comment, approve, or reject fixes. The entire security review happens inside the platform.
Converters: meeting people where they are
The analyzer accepts input from ProVerif, Tamarin, Scyther, Avispa, CryptoVerif, and Maude descriptions. This is an adoption strategy, not a convenience feature.
Thousands of protocols are already modeled in these languages. Researchers and engineers who have invested years in ProVerif models should not have to rewrite them. They import their existing description, run the analyzer, and get the same output plus repair proposals plus real-time monitoring plus CI integration.
The converters are imperfect - each source language has constructs that do not map cleanly. But they handle the common case well enough to lower the barrier from "I should try this tool" to "I just tried this tool."
Let us be explicit about what we are building. A tool does one thing from the command line. A platform integrates into workflows, provides APIs, runs continuously, and collaborates with other systems.
The protocol analyzer we are building has:
- A CLI for direct use and scripting
- A GitHub Action for CI/CD
- An LSP server for IDE integration
- A gRPC API for programmatic access
- A daemon for continuous monitoring
- A sniffer for real-time traffic analysis
- A web UI for collaborative review
- WASM bindings for browser-based playground
- Converters from five existing tools
This is a platform. The symbolic analysis core - the part described in the previous article - is the engine. Everything else is the interface between that engine and the world where protocols are built, deployed, and attacked.
The revolution is practical, not technical
The technical contributions matter: automatic repair, GNN-guided search, incremental closure, sixteen attacker models. But the reason they matter is that they enable a new capability - protocol verification that runs in CI, in your IDE, on your network, in real time.
ProVerif and Tamarin proved that symbolic protocol analysis is possible. We are trying to prove that it is practical - practical enough to run on every commit, practical enough to catch vulnerabilities while you type, practical enough to monitor live traffic.
That is the shift: from laboratory instrument to industrial platform. From "analyze after design" to "verify during development and after deployment." From a tool that finds attacks to a platform that finds them, fixes them, and watches for them.
Status
The CI/CD action, the LSP server, the daemon, and the sniffer are in active development. The web UI has working prototypes. The converters handle common cases. The core engine - described in the previous article - is functional and stable.
This project is under active development. The platform described here is being built, not shipped. But the direction is clear, and the architecture supports it.
This project is under active development. This article describes the planned platform capabilities of a tool still being built. The previous article covers the core engine architecture; this one covers the interfaces between that engine and the development lifecycle.
Follow the project: github.com/Sup4ikX - a preview release will be published there as soon as the first production version is ready.