> it respects boolean logic.

Intuitionist or classical?

Intuitionist. Truth is provability; the propagation model is basically digital logic. If you mark a premise to a conclusion false, the conclusion is then marked "false" but it really just means "it is false that it is proven"; vitiated. Might still be true, just needs further work.

You would need a highly disciplined and motivated set of people in the team. I have been on courses where teams do this on pen/paper and it is a real skill and it is all you do for days. Forget anything else like programming, finishing work, etc.

I'd be stoked if you wrote more about this experience and shared it somewhere.