Ilja Zakharov was one of the greatest contributors to the Klever project. He was the primary developer of such components as Environment Model Generator, Program Fragment Generator, Schedulers and Controller. Besides, he created a lot of environment model specifications for different kinds of target programs and made considerable scientific researches. We appreciate his work very much.
Recently Ilja Zakharov became a Verification Engineer at the Runtime Verification company. There he will be engaged in application of formal methods for smart contracts and tools used for their verification. We wish him good luck and hope that the gained experience will help him at the new position.