Anti-Vibe Coding

1. Machine-Checked Certificate No software artifact is correct without an explicit, machine-checkable proof.

2. Zero Implicit Computation Proof checkers must not hide logic behind opaque normalisation heuristics.

3. Minimal TCB Kernel Trusted kernels must remain small (~20k LOC) so they can be audited by humans.

4. Deterministic Replay Every proof step and build phase must produce bit-for-bit reproducible outcomes.

5. Explicit Assumptions All axioms, premises, and FFIs must be explicitly quantified and tracked.

6. Invariant Primacy Formulate state invariants and specifications before writing or accepting code.

7. Rejection of the Vibe If an AI generates code that you cannot formally specify, reject it immediately.

8. Proof Stability Proofs must not break due to cosmetic refactoring or minor runtime updates.

9. Universal Blame Errors must point directly to the exact logical premise that was violated.

10. High-Assurance Longevity Build software to last decades, grounded in immutable mathematical truths.

1. Local NFV/FFI vs. Global $d Variable Groups Metamath couples unrelated statements via ambient disjoint-variable ($d) groups. Obelisk uses local, decidable boolean side conditions (NFV and FFI) scoped strictly to the inference rule.

2. Self-Hosted CakeML/SML'97 Kernel vs. Python/C++ Instead of ad-hoc imperative string checkers in Python or C++, Obelisk enforces soundness via LCF abstract types in portable SML'97 compiled by the verified CakeML compiler.

3. Algebraic ASTs vs. Formula-Building Spam Metamath prints dozens of syntactic steps just to prove a formula is well-formed. Obelisk's SML algebraic datatypes (Fm_Expre, Class_Expre) guarantee well-formedness statically.

4. Compact Proof Terms vs. Verbose Step Tables Dumping hundreds of repetitive step-by-step RPN table rows hides mathematical structure. Obelisk represents proofs as concise LCF/Curry–Howard proof terms.