Hi, I am interested in verifying properties of Elixir code. In particular, I write code for financial institutions and I am exploring if formal verification can be useful for me.

A loan contract starts in a unsigned state, waiting for some party to propose an amount.

When an amount is proposed, the contract enters a state when it waits for signatures from lender and lendee.

Whenever an amount is proposed, both signatures are reset, so that a lendee never has to pay more than he agreed to, because every time the amount is changed, new signatures are needed.

The contract is done when all debt has been paid (and not more).

Is there an easy-to-use solution for verifying this property in the Elixir/Erlang ecossystem?

The answer might rely on property-based testing, as long as it is exhaustive up to a given measure, as in bounded model checking.

My code is:

defmodule Loan do

  def start() do
    spawn(__MODULE__, :main_loop, [:unsigned])
  end

  def main_loop(:done) do
    receive do
      :show ->
        IO.puts("Contract is finished")
        apply(__MODULE__, :main_loop, [:done])
    end
  end

  def main_loop(:unsigned) do
    receive do
      {:propose, amount} ->
        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: false, lender: false]])
    end
  end

  @spec main_loop(:proposal, any, [{:lendee, any} | {:lender, any}, ...]) :: any
  def main_loop(:proposal, amount, lendee: true, lender: true) do
    IO.puts("Contract is now signed, contract value is #{amount}")
    apply(__MODULE__, :main_loop, [:signed, amount])
  end

  def main_loop(:proposal, amount, lendee: lendee, lender: lender) do
    receive do
      :sign_lendee ->
        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: true, lender: lender]])

      :sign_lender ->
        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: lendee, lender: true]])

      {:propose, amount} ->
        apply(__MODULE__, :main_loop, [:proposal, amount, lendee: false, lender: false])

      :show ->
        case {lendee, lender} do
          {false, false} ->
            IO.puts("No one has signed, contract value is #{amount}")

          {false, true} ->
            IO.puts("Lender has signed, contract value is #{amount}")

          {true, false} ->
            IO.puts("Lendee has signed, contract value is #{amount}")

          {true, true} ->
            IO.puts("Both lender and lendee have signed, contract value is #{amount}")
        end

        apply(__MODULE__, :main_loop, [:proposal, amount, [lendee: lendee, lender: lender]])
    end
  end

  def main_loop(:signed, balance) when balance > 0 do
    receive do
      :show ->
        IO.puts(balance)
        apply(__MODULE__, :main_loop, [:signed, balance])

      {:pay, amount} when amount <= balance ->
        IO.puts("Paying #{amount} to lender")
        apply(__MODULE__, :main_loop, [:signed, balance - amount])
    end
  end

  def main_loop(:signed, 0) do
    IO.puts("Contract is finished")
    main_loop(:done)
  end
end