Efficient and reliable software & hardware with simple formal specifications and machine-checked proofs.