Protocol Verification Language
A verification-aware language with a built-in verification engine and structures.
No spam emails, just to keep you up-to-date.
Start Learning PVL
PVL is modern, intuitive and intensely documented. Check our reference for getting started.
We are still in early development phase, please email us at info@pvl.io for any missing documentation.
Why PVL?
We offer Verifiable, Reliable and Performant software.
Reliability
Combined with the verification engine, PVL has adopted many of the modern safety and reliability techniques and paradigms to eliminate as much bugs as possible in the compile-time. We have adopted techniques developed in language such as Rust, and dialects such as Cyclone.
Reliability in Our ReferenceVerifiability
PVL includes verification-aware data and control structures that allow fast and easy verification of software written in PVL. The compiler uses an internal verification engine that allows compile time verification of various types of constraints on the language constructs.
Verification in Our ReferenceCurrently we support;
-
Sequential Imperative Programs
-
If-Then-Else Structures
-
Finite Unrollable Loops
-
Recursive Functions
-
Arbitrary Loop Structures
We will add;
Performance
PVL aims to be used in high performance network and cryptographic protocols as well as formally defined algorithms. In this regard, we have worked on creating a language with as low overhead as possible while maintaining many of the modern programming language aspects as zero-cost abstractions.
Performance in Our ReferenceOur Demo Video
Our Team
Umut Şahin
Born in 1997, Umut Şahin is a programmer by heart. He have been programming since he was 11 years old. His main interests are Compilers, Operating Systems, Databases, Concurrency and Parallelism.
Alperen Keleş
Alperen Keleş is an algorithms geek that loves programming languages and formal verification. His main interets reside amongs safety and reliability of programming languages and also program synthesis as a hobby.
