This issue is a task to write/propose an RFC for a new default output format for Kani.

There are a number of needs here:

1. Cleanup Kani's output #1194
2. Feature Request: Vast cargo kani output simplification #1653 (closed but has good discussion)
3. Organize the output from Kani to make it more user friendly #598
4. Report memory usage for verification step #1675
5. Kani should not print warnings about concurrency primitives (as long as it's single-threaded) #1460
6. We should give better output for unbounded unwinding that the raw CBMC output.
7. Support --output-format=terse kani-github-action#10
8. Print out current task and timestamp for better user experience #1713
9. UI unclear: reported results need to be clearer about the harness #1711
10. Add user friendly Kani driver messages #1899
11. Remove terse output requirement for parallel jobs  #3357

The RFC should address how the output changes with the parallel runner kani -j.

The goal should be (I think:)

1. Default output
2. Verbose output
3. Quiet output (probably nothing: just exit status)
4. Plus: possible differences for being interactive (terminal) versus batch (redirected to file / CI). (Colors + live status info as considerations)

I think I will designate as out-of-scope:

1. Design Machine Readable Output - RFC #942
2. Add Report, YAML Display Options to Output #681

There are likely a lot of decisions to be made here. I'm not even going to start the list of questions yet.