This article was just wildly misleading, the title is well, it speaks for itself.

Interesting language and rather than 'formally proven' as the article wildly claims it is a strongly typed system ala Haskell. So yep looks a great idea for secure systems - but formally proven - bah! :-)

Has anyone here actually formally proved a non trivial program, say a couple of hundred lines on NCSS?

How about tens of thousands, hundreds of thousands or millions of lines of code. The complexity of the proof would be insanely complicated such that the level of expertise to define the requirements would be (if at all within the limits of human endeavour) only for maybe a handful of people. And do those people make good business analysts, or hackers, or entrepreneurs or even just communicators.

Jeez the misinformation that gets spread!