There is a lot involved in providing a loan as a company, mostly in terms of legalities and risk management. As a lender it is important to have a clear record of the customers applying for a loan, as this helps assessing the risk that comes with providing a loan. Furthermore, it is required by law to know who it is that you are providing a loan to. To achieve this, loan providers gather a variety of personal and financial information. The gathering of such information has traditionally been a time consuming practice, both for the customer and the lender. The customer is required to manually find and submit information, and in turn the lender has to verify that the received information is not fraudulent or incorrect. If collection of personal information, payrolls and credits could be done in an automated way, both the customer and the lender will benefit greatly. We have designed and developed the Customer Verification Engine, the CVE, in order to solve this time consuming process of collecting and submitting documents. The CVE is capable of cleverly combining several external data sources, creating a clear record of the customer. While previously the customer had to manually provide a large set of documents, it is now done at the push of a button. Furthermore, by having a system where the information is retrieved, rather than provided by the customer, the verification becomes significantly more reliable, as there is little to no room for the customer to provide fraudulent information. The CVE is a robust and scalable system that is capable of handling unexpected behavior both in terms of input and connection to external sources. An extensive test suite verifies correct behavior of the CVE under both normal and unexpected circumstances. The information gathered by the CVE will be relied upon to determine whether or not a customer is eligible for a loan. As the CVE will be continued to be worked upon, we have put effort into making it extendable for future developers. Using the extensive documentation and the modularity of the system, it should be straightforward for future developers to add new integrations with external parties to the CVE.

Bitcoin’s underlying consensus algorithm, Proof of Work, is of inefficient nature. Due to the sheer size that Bitcoin has grown to over the recent years, power consumption has increased so much that the Bitcoin network has been estimated to consume more power than the whole country of Ireland. This paper investigates several alternatives to the Proof of Work consensus algorithm, with a focus on energy efficiency. We found permissioned and permissionless consensus algorithms that offer solutions that consume significantly less energy than Proof of Work.

Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof in the style of Hoare. This process has been mechanized by the introduction of Separation Logic and computer assisted verification tools. However, the tools fail to achieve the readability and convenience of manual paper proof outlines. This is a pity, because getting ideas and proofs across is essential for scientific research. I introduce a mechanization for proof outlines of imperative programs to interactively write human readable outlines in the dependently typed programming language and proof assistant Agda. I achieve this by introducing practical syntax and proof automation to write concise proof outlines for a simple imperative programming language based on λ-calculus. The proposed solution results in proof outlines that combine the readability of paper proof outlines and the precision of mechanization.