Which parts aren't automated?

Plenty of line still have drivers.

The only fully automated lines are 1 and 14.

The parts involving humans.

Interesting. Do you have any additional information on this?

It seems to be not OCaml:

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

Pure languages are also great for this kind of thing, because of the lack of side-effects (aka Haskell's moto). OCaml manages its imperative parts in a way that isn't as good had Haskell does, but it's probably possible to get a very clean code that is mostly pure, allowing a mathematical proof of safety.

My bad. I heard from this from a friend that used to work at the RATP (Paris Subway). Thanks you for the link, very instructive !