Showcases
ERC20 Solidity Smart-Contract Verification & The DAO BUG PROOFS
Framework and the model in Coq theorem prover system to prove the properties of ERC-20 Ethereum Solidity smart-contracts, with the showcase application to “The DAO” bug.
Loan Calculator
As an enterprise-like FinTech example, we’ve developed a loan payment calculator microservice system with the Coq-verified core and typesafe Haskell layer for interoperability with other services via REST-interface.
Developed as a part of FinProof meta-project.
Pilot Program
Learn how certified programming technology vision and technology stack integrates with your existing system, or can be used to develop the new one from scratch.