Isabelle is a generic proof engine, can be combined with any fronted which satisfies its API (it’s a bit more complicated) so yes such thing exists. Proof assi

Isabelle is a generic proof engine, can be combined with any fronted which satisfies its API (it’s a bit more complicated) so yes such thing exists. Proof assistants aren’t whimsical like cottage industry of programming languages. Proof assistants are divided into 3 parts, the core or foundation (F) which is a very small language at the heart of the prover, the vernacular (V) the language in which humans write the code and the meta language for proof search and meta programming (M). The V is translated into F and this translation is often proven to be correct. De Bruin criteria says that F has to be small and should be independently checked (mostly through inspection or mechanization in other framework). In Coq the proof derives is again checked from ground up by F when you write Qed. Andrej Bauer explains better than I can. https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista/376973#376973 https://mathoverflow.net/questions/376839/what-makes-depende...