You need requirements, evidence and proof in your development pipeline. Also well maintained and exhaustive E2E tests. Also run code gardening sessions from time to time.

FYI @PrologInfo :)

The theorems and the differential test: looted.github.io/kibi/guide/…

Kibi's numeric checks are Prolog: intervals.pl folds each comparison on a variable into an interval and asks if it's empty. Now those folds are proved exact in Lean 4, and CI runs 200k cases through the Prolog code, the Lean model and a CLP(Q)/CLP(FD) oracle.

Legacy codebase aside, creating formal proof in greenfield projects has upsides: the proof is created when the context is fresh. The problem with legacy codebases is really that context (in broad sense) is probably long gone, and the code doesn't necessarily express it (bugs).

Update: as of today something can. The formal proof lane is out: certificates that cover every case, re-checked by Kibi itself. xitter.cf/kibi_dev/status/211462…

Hey @ArthurLiu0725! It's up to you and your CI really. Contradictions get blocked at commit gate (git hooks), for proof levels you could set your CI to block on requirement/proof level. Haven't tried the latter though.

How certificates bind to claims: looted.github.io/kibi/guide/… Setup prompt: github.com/Looted/kibi#quick…

Passing tests are evidence, not proof. They sample cases. New in Kibi: the formal proof lane. A requirement is marked proved only when a certificate covers every case (every enum member, a typechecked switch, z3/cvc5 returning unsat) and Kibi re-checks it itself.

Hey Martin! In Kibi every requirement has a firmness level and only a person sign-off will give it a firm level. When it comes to testing, Kibi assigns every requirement an evidence level: looted.github.io/kibi/guide/…. Untested code will never reach tested, let alone proved.

Feel free to send a DM or skim through the docs: looted.github.io/kibi/. The formal proof work is still on develop but landing soon.

Each requirement gets a computed level: proved > tested > asserted > unverified. “Proved” is formal: requirements compile to typed facts, solvers check consistency and emit certificates a separate checker re-verifies.

Hey @MichaelObasa! Kibi never counts an agent’s claim as evidence. Agent-written requirements stay unverified until a person approves them. Kibi runs the tests itself and ties each receipt to a hash of the code.

11/ Kibi is a repo-local knowledge base for coding agents, checked by Prolog (bundled on Linux and macOS). npm i -D kibi-core kibi-cli kibi-mcp github.com/Looted/kibi Proof ladder: looted.github.io/kibi/guide/…

10/ It's plain Markdown, so it renders wherever your agent replies, chat apps and cloud sessions included, plus a self-contained HTML page. /kibi-signoff in Claude Code, Cursor, ZCode and OpenCode. VS Code opens it in a panel. Hooks ask for it once an agent writes requirements.

9/ Before you sign off, kibi signoff shows what a change adds, rewrites, retires or affects, each requirement quoted with its firmness, proof state and evidence level. kibi signoff --questions numbers the decisions waiting for you, next to the rule each one would change.

8/ Changing your mind is fine. Changing it quietly isn't. Every supersede needs a "Why this changed" section, and a non-firm decision can't replace a firm one. Rules imported from your docs count as firm. Only agent-written ones start as default.

7/ Firmness: every requirement and ADR says how firmly it was decided. firm: a person stated it, and it cites their words default: can be revisited on evidence exploratory: a guess Agents ask before changing a firm rule, and can't reword one in place.

6/ Each answer leaves a certificate: a model when the facts are consistent, an irreducible core when they aren't. A small separate checker re-checks every certificate by evaluation only. It never reruns the search that found it. kibi check --write-certificates certs.json

5/ A contradiction comes back as the smallest set of facts that can't hold at once, plus the requirements behind them, so you know what to change or supersede. Anything it can't compare (mixed units, unsupported operators) is reported as unresolved, never as consistent.