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 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 ...

First of all, sorry if my question is too nonsensical and naive, I'm just getting started with Isabelle/HOL. I am reading Hou's "Fundamentals of Logic and Computation: With Practical Automated ...

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 ...