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 a 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 fill those lacks 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 a 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:
- It is quite hard to realize the FV without deep mathematical knowledge
- The lack of appropriate engineering tools taken from the box to put in common development pipeline
- The necessity to create formal specification at the early stages which virtually contradicts with agile principles when rapid prototyping transforms to the product instantly
- 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 fill those lacks and give the developers tools and methods allowing to:
- Express the code in more conventional way than proof assistants require
- Give a way to express the specification in more realizable language or graphic tools than sophisticated mathematical expressions
- Give the methodology of how 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 realizes of how the code works and which coding style is more verifiable — the less mistakes she makes a priori even without verification
- Programming is dialogue with a computer — not monologue. The smaller fragments of the code, which are answerable by computer it consists of, — the more chance one finds the better way to express the engineering goals. We believe that a human being should find the proper language with a computer to explain what she needs. They actually do not have a common one yet.
- We also believe in the old as a world principle — “no rules but mechanisms”. Noone can restrict humans 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 restrictable 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. Really valuable product cannot consist of 1000 lines of code :)
6. The main market pains we are trying to resolve are
- Uncertainty in work of the software programs, which leads to very high level of duplicates, no wish to investigate external code, and to contribute to open source initiatives
- Software composability is the subsequence of the previous problem. When one is uncertain of how the software works, it is difficult to create a new piece of code which corresponds to the existing. And 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. We are not here to blame hackers or to help rich people to become more rich, but to help good guys to increase their belief in technology by improving the quality of the products, giving them a way to assess them from the formal point of view.
1. We are a startup, which brings the methods of software formal verification to the wider community
2. Formal verification of software has a 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 fill those lacks 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 a 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:
- It is quite hard to realize the FV without deep mathematical knowledge
- The lack of appropriate engineering tools taken from the box to put in common development pipeline
- The necessity to create formal specification at the early stages which virtually contradicts with agile principles when rapid prototyping transforms to the product instantly
- 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 fill those lacks and give the developers tools and methods allowing to:
- Express the code in more conventional way than proof assistants require
- Give a way to express the specification in more realizable language or graphic tools than sophisticated mathematical expressions
- Give the methodology of how 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 realizes of how the code works and which coding style is more verifiable — the less mistakes she makes a priori even without verification
- Programming is dialogue with a computer — not monologue. The smaller fragments of the code, which are answerable by computer it consists of, — the more chance one finds the better way to express the engineering goals. We believe that a human being should find the proper language with a computer to explain what she needs. They actually do not have a common one yet.
- We also believe in the old as a world principle — “no rules but mechanisms”. Noone can restrict humans 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 restrictable 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. Really valuable product cannot consist of 1000 lines of code :)
6. The main market pains we are trying to resolve are
- Uncertainty in work of the software programs, which leads to very high level of duplicates, no wish to investigate external code, and to contribute to open source initiatives
- Software composability is the subsequence of the previous problem. When one is uncertain of how the software works, it is difficult to create a new piece of code which corresponds to the existing. And 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. We are not here to blame hackers or to help rich people to become more rich, but to help good guys to increase their belief in technology by improving the quality of the products, giving them a way to assess them from the formal point of view.
Interested in unprecedented security of your smart contracts?
Inquire us for the details and we’ll make it worth your time
