The only fully automated lines are 1 and 14.

First real success was Meteor line 14 driverless metro in Paris: Over 110 000 lines of B models were written, generating 86 000 lines of Ada. No bugs were detected after the proofs, neither at the functional validation, at the integration validation, at on-site test, nor since the metro lines operate (October 1998). The safety-critical software is still in version 1.0 in year 2007, without any bug detected so far.

From: http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf

       |bool foo(bool i, bool j) {
      2|    return i ||
      1|           j;
       |}
       |
       |void main() {
      1|    foo(true, false);
      1|    foo(false, false);
       |}