Question about how tla+ can do and how it works

[remuscl <remus.cl...@xxxxxxxxx>]

Hi, I'm new to tla+ and watching the video tutorials now, and I have two question about what tla+ could do and how it works.

There is a snippet of C code:

```c
assert(N >= 0);
for(i = 0; i < N; i++){
  f(i);
}
```

We have the conclusion:

```c
N = 0: loop 0 times
N = 1: loop 1 time and equal to `f(0)`
N > 1: loop N times and equal to `f(0), f(1), f(2) ... f(N-1)`
```

Q1:
    Could we use tla+ to prove the above conclusion is always true when N is ANY valid natural number (>= 0)?

Q2:
    If the answer of Q1 is "yes", and how tla+ works? By the appropriate amount of sample testing or strict proof by some certain math methods which are ALWAYS right?

Thank you very much for your time.