nesy-solver
neurosymbolic proof playground
Playground
Strategy
Certificates
About
Obligation
Language:
SMT-LIB
Lean
Coq
Idris2
Agda
Class:
auto (recommend)
safety
linearity
termination
equiv
correctness
confluence
totality
invariant
refinement
model-check
other
Prover:
auto (strategy)
Z3
CVC5
Coq
Lean
Idris2
Agda
Isabelle
Dafny
F*
Prove
Clear
Result
Submit an obligation to see the prover's verdict.