equivalence-aware-computing
Safe operations in Idris2 with dependent types, exposed via a Zig FFI. Aims at full formal verification; only partly proven today — see AFFIRMATION.adoc and PROOF-NEEDS.adoc for what is and isn't.
