Unanswered Questions

Background In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...

Is there a website that maintains a list, or is there a list, of tools that support verification of programs written in languages supported by the GCC compiler front ends: C, C++, Objective-C, Fortran,...

For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as add_assoc : forall (x y : T), x + y + z = x + (y + z). We can thus prove ...

I am trying to learn formal methods and have been learning Dafny and practicing by verifying Leetcode problems. I have gotten stuck on this one. https://leetcode.com/problems/diameter-of-binary-tree/...

I'm wanting to find a modern proof assistant that I can use for modeling distributed systems or similar protocols/algorithms. TLA+ is the most commonly used language in that field, but I recently ...

I have a set of algebraic axioms. I need to prove an equation, an algebraic law. What I did was applying "trivial" rewrite rules by a theorem prover from both ends, and then an automatic ...

This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway. I would like to consider the simplest possible formally verified ...

Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...

Is there a written account on how to carry out research in formal verification with proof assistants? Formalisation of standard mathematics, verification of information systems and developing proof ...