InvariantDijkstra.scala

trait Color
case object Black extends Color
case object White extends Color

type Pair = Tuple2[Color,Color]

case class Urn(b: Int, w: Int) {
  require (b >= 0 && w >= 0 && b + w >= 1)
  lazy val random = new java.util.Random
  private def takeOne(): (Color, Urn) = {
    val choice = random.nextInt(b + w)
    if (choice < b)
      (Black, Urn(b - 1, w))
    else
      (White, Urn(b, w - 1))
  }
  def takePair(): (Pair,Urn) = {
    require (b + w >= 2)
    val t1 = takeOne()
    val t2 = t1._2.takeOne()
    ((t1._1, t2._1), t2._2)
  }
  def putBack(color: Color): Urn = color match {
    case Black => Urn(b + 1, w)
    case White => Urn(b, w + 1)
  }
}

object Game {
  def play(urn: Urn): Color = urn match {
    // end states
    case Urn(1,0) => Black
    case Urn(0,1) => White
    case _        => urn.takePair match {
      case ((Black,Black), turn) => play(turn.putBack(Black))
      case ((White,White), turn) => play(turn.putBack(Black))
      case (_, turn)             => play(turn.putBack(White))
    } 
  }
}

https://www.youtube.com/watch?v=GX3URhx6i2E
For a video lecture by Dr Dijkstra on this problem recorded in 1990 by Sun Microsystems. The lecture titles: "General structure about correctness argument about programs". I had uploaded the lecture in 2016 and someone just pointed to this github link for the code. Great work!