Smart Contracts

Smart contracts are programs which execute on a blockchain, every step of their execution is checked as a part of the blockchain’s Consensus Protocol, ensuring that no individual party can maliciously or erroneously alter the result of running a smart contract.

Some examples of smart contract programming languages are:

Solidity
Vyper
Michelson
Liquidity
Scilla
DeepSEA

Links to this page

Week 1 - Plutus Pioneer Program

A nice property of Plutus Smart Contracts is that if you run a smart contract locally (and it succeeds) then it is guaranteed to succeed on chain as long as the UTXOs are still unspent.
Interesting formal methods and/or blockchain projects

DeepSEA - A language to write verified Smart Contracts
Formal Methods and Blockchain

Formal methods applied to the blockchain involves, for example, the use of computer-assisted proofs the verify properties about Smart Contracts.