Blockchain technologies are moving fast and their distributed nature as well as their high-stake (financial) applications make it crucial to “get things right”. Moreover, blockchain technologies often come with a high cost for maintaining blockchain infrastructure and for running applications. In this thesis formal reasoning is used for guaranteeing correctness while reducing the cost of (i) maintaining the infrastructure by optimising blockchain protocols, and (ii) running applications by optimising blockchain programs—so called smart contracts. Both have a clear cost measure: for protocols the amount of exchanged messages, and for smart contracts the monetary cost of execution. In the first result for blockchain protocols starting from a proof of correctness for an abstract blockchain consensus protocol using infinitely many messages and infinite state, a refinement proof transfers correctness to a concrete implementation of the protocol reducing the cost to finite resources. In the second result I move from a blockchain to a block graph. This block graph embeds the run of a deterministic byzantine fault tolerant protocol, thereby getting parallelism “for free” and reducing the exchanged messages to the point of omission. For blockchain programs, I optimise programs executed on the Ethereum blockchain. As a first result, I use superoptimisation and encode the search for cheaper, but observationally equivalent, program as a search problem for an automated theorem prover. Since solving this search problem is in itself expensive, my second result is an efficient encoding of the search problem. Finally for reusing found optimisations, my third results gives a framework to generate peephole optimisation rules for a smart contract compiler.