chriseth

contract BinarySearch {
  ///@why3
  /// requires { arg_data.length < UInt256.max_uint256 }
  /// requires { 0 <= to_int arg_begin <= to_int arg_end <= arg_data.length }
  /// requires { forall i j: int. 0 <= i <= j < arg_data.length -> to_int arg_data[i] <= to_int arg_data[j] }
  /// variant { to_int arg_end - to_int arg_begin }
  /// ensures {
  ///   to_int result < UInt256.max_uint256 -> (to_int arg_begin <= to_int result < to_int arg_end && to_int arg_data[to_int result] = to_int arg_value)
  /// }
  /// ensures {

patcon

# install ocaml and deps
apt-get install ocaml ocaml-native-compilers
apt-get install liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev libocamlgraph-ocaml-dev

# install opam from binaries (ocaml package manager)
# See https://opam.ocaml.org/doc/Install.html#Binarydistribution
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin/

#### OR

aaronjensen

# ATTENTION: This is now supported in plug_cowboy as of 2.1.0:
# https://hexdocs.pm/plug_cowboy/Plug.Cowboy.Drainer.html

defmodule DrainStop do
  @moduledoc """
  DrainStop Attempts to gracefully shutdown an endpoint when a normal shutdown
  occurs. It first shuts down the acceptor, ensuring that no new requests can be
  made. It then waits for all pending requests to complete. If the timeout
  expires before this happens, it stops waiting, allowing the supervision tree
  to continue its shutdown order.

chriseth

This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.

Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.

The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made

bitwalker

defmodule Config do
  @moduledoc """
  This module handles fetching values from the config with some additional niceties
  """

  @doc """
  Fetches a value from the config, or from the environment if {:system, "VAR"}
  is provided.

  An optional default value can be provided if desired.