Pruvendo White Paper
Pruvendo White Paper
21 Feb
Pruvendo
1. We are a startup, which brings the methods of software formal verification to the wider community
2. Formal verification of software has decades of history and however all the time was under attention of the very narrow subset of IT specialists and computer scientists
3. It is because of superposition of the following reasons:
4. Therefore our main goal is to address those gaps and give the developers tools and methods allowing to:
5. What we think is valuable:
6. The main market pains we are trying to resolve are
2. Formal verification of software has decades of history and however all the time was under attention of the very narrow subset of IT specialists and computer scientists
3. It is because of superposition of the following reasons:
- Performing formal verification requires deep mathematical knowledge
- The lack of appropriate engineering out-of-the-box tools to put in common development pipeline
- The necessity to create formal specification at the early stages which often conflicts with agile principles where rapid prototyping leads directly to production
- The lack of expressive language which allows both to write not_only_declarative_functional_programs and embed it to verification subsystem
4. Therefore our main goal is to address those gaps and give the developers tools and methods allowing to:
- Express code in a more conventional way than proof assistants typically require
- Give a way to express the specification in more accessible language or graphic tools than sophisticated mathematical expressions
- Give the methodology of how to specify and verify the code instantly during the development process
- Automate everything automatable, doing all tedious work under the hood
5. What we think is valuable:
- Conscious programming - the more one understands how the code works and which coding style is more verifiable - the fewer mistakes one makes even without formal verification
- Programming is a dialogue with a computer, not a monologue. The smaller the verifiable code fragments, the better the chance of finding the right way to express engineering goals. We believe that humans and computers need a proper shared language - one that does not yet exist.
- We also believe in the old as a world principle - “no rules but mechanisms”. No one can restrict human creativity, and definitely no actual need for that. Moreover human creativity is still the only thing allowing people to evolve at least not worse than robots. Programming allows us to express human ideas in a way which can be understood by robots. Formal methods are to help them here, but that is not to be tedious or restrictive in any sense. We need to develop mechanisms and metrics which will guide humans in their dialogue with computers.
- And finally we believe that humans need to work hard to innovate. Good ideas are not enough. A truly valuable product is more than 1000 lines of code.
6. The main market pains we are trying to resolve are
- Uncertainty in how software programs work, leading to code duplication, reluctance to investigate external code, and limited contributions to open-source initiatives
- Software composability suffers when developers are uncertain of how existing code works, making it difficult to create compatible components. This leads to the problem of “the more code you write - the less usable it becomes” because of the rising internal entropy.
- Software is the subject of hacks and subsequent money loss. Our mission is to strengthen trust in technology by improving software quality and providing stakeholders with formal methods to assess product reliability.
1. We are a startup, which brings the methods of software formal verification to the wider community
2. Formal verification of software has decades of history and however all the time was under attention of the very narrow subset of IT specialists and computer scientists
3. It is because of superposition of the following reasons:
4. Therefore our main goal is to address those gaps and give the developers tools and methods allowing to:
5. What we think is valuable:
6. The main market pains we are trying to resolve are
2. Formal verification of software has decades of history and however all the time was under attention of the very narrow subset of IT specialists and computer scientists
3. It is because of superposition of the following reasons:
- Performing formal verification requires deep mathematical knowledge
- The lack of appropriate engineering out-of-the-box tools to put in common development pipeline
- The necessity to create formal specification at the early stages which often conflicts with agile principles where rapid prototyping leads directly to production
- The lack of expressive language which allows both to write not_only_declarative_functional_programs and embed it to verification subsystem
4. Therefore our main goal is to address those gaps and give the developers tools and methods allowing to:
- Express code in a more conventional way than proof assistants typically require
- Give a way to express the specification in more accessible language or graphic tools than sophisticated mathematical expressions
- Give the methodology of how to specify and verify the code instantly during the development process
- Automate everything automatable, doing all tedious work under the hood
5. What we think is valuable:
- Conscious programming - the more one understands how the code works and which coding style is more verifiable - the fewer mistakes one makes even without formal verification
- Programming is a dialogue with a computer, not a monologue. The smaller the verifiable code fragments, the better the chance of finding the right way to express engineering goals. We believe that humans and computers need a proper shared language - one that does not yet exist.
- We also believe in the old as a world principle - “no rules but mechanisms”. No one can restrict human creativity, and definitely no actual need for that. Moreover human creativity is still the only thing allowing people to evolve at least not worse than robots. Programming allows us to express human ideas in a way which can be understood by robots. Formal methods are to help them here, but that is not to be tedious or restrictive in any sense. We need to develop mechanisms and metrics which will guide humans in their dialogue with computers.
- And finally we believe that humans need to work hard to innovate. Good ideas are not enough. A truly valuable product is more than 1000 lines of code.
6. The main market pains we are trying to resolve are
- Uncertainty in how software programs work, leading to code duplication, reluctance to investigate external code, and limited contributions to open-source initiatives
- Software composability suffers when developers are uncertain of how existing code works, making it difficult to create compatible components. This leads to the problem of “the more code you write - the less usable it becomes” because of the rising internal entropy.
- Software is the subject of hacks and subsequent money loss. Our mission is to strengthen trust in technology by improving software quality and providing stakeholders with formal methods to assess product reliability.
Interested in unprecedented security of your smart contracts?
Contact us for the details and we’ll make it worth your time
