iiinova — where your digital self keeps evolving

Consciousness is as methodologically interesting as revelations from God. Thomas Paine noted revelation can only have validity to the recipient. Beyond that is hearsay. The state of "consciousness" as an experience makes sense only to the one experiencing it.

100

Reposted by @gavin.codes

Scidonia @scidonia.bsky.social · 14/07/2026

The gap between what written code and human understanding is widening due to AI code generation. Merging software verification with design by contract offers a way out. Top-level contracts for humans, sub-contracts for the machine prover. Full breakdown: scidonia.ai/blog/contrac...

scidonia.ai

Understanding Software in the Large: Contracts and Compositionality | Scidonia

A top-level contract tells you what a system does. Sub-contracts tell the prover how it does it. You only need to read the first one. This is componentisation in real terms — and it changes how we thi...

011

Reposted by @gavin.codes

Scidonia @scidonia.bsky.social · 18/06/2026

We used LLMs to prove PCF type preservation in Rocq from scratch. The cost? As low as $0.06. When a mechanised proof costs less than a bug report, vericoding (using AI to write code and a prover to guarantee it) becomes the new standard. scidonia.ai/blog/proof-a...

scidonia.ai

Proof as Commodity | Scidonia

We proved type preservation for PCF — a classic typed lambda calculus benchmark — using two frontier LLMs and rocq-piler. DeepSeek v4 completed it in 21 minutes for $0.06. Claude Opus 4.8 took 14 minu...

011

gavin.codes @gavin.codes · 18/06/2026

$0.06 for a non-trivial proof about programming languages. This is going to change everything.

100

gavin.codes @gavin.codes · 17/06/2026

Type preservation for PCF+Ref now at 4c on DeepSeek + Opencode + Rocqpiler 4 cents ... proof is cheaper than bananas

000

gavin.codes @gavin.codes · 17/06/2026

The approach to Vericoding in axiomander in a nutshell

000

gavin.codes @gavin.codes · 17/06/2026

1/2 Can we safely let AIs do almost all of the coding? What do we need to avoid getting mountains of slop? * Small control surface [Specification] * Deterministic proof of correctness [Proof assistant]

100

gavin.codes @gavin.codes · 15/06/2026

This is really a rough draft of the future. Specification as control surface, code as disposable and organisations of AIs with specific responsibilities.

011

gavin.codes @gavin.codes · 11/06/2026

Proving properties of software has historically been hard because proof is hard. But if we don't do the proofs, then the hard problem resolves to getting the right specification. This will remain hard, but it will probably also be the main activity in the near future. Time to take this seriously!

000

gavin.codes @gavin.codes · 10/06/2026

Just tried to run my "benchmark" proof (PCF+ref type preservation) on Fable 5. It took 10 minutes and did not make ONE SINGLE ERROR. No tactics out of place, no iteration. Just full Rocq proofs the first time. This is mental.

110

gavin.codes @gavin.codes · 04/06/2026

1/3 Proving very basic properties of software can have huge impacts. The NASA Mars Climate Orbiter failed due to a mismatch between Pound-seconds (Imperial) and Newton-seconds (Metric). This mistake cost $327 Million.

100

gavin.codes @gavin.codes · 03/06/2026

Very soon we will be neither reading, nor writing code. Software engineers will be engaged in specification management. The theorem prover is the key ingredient to make this possible. scidonia.ai/blog/opaque-...

scidonia.ai

Code Will Become Opaque — And That's Fine | Scidonia

Most software developers haven't twigged the real potential of automated theorem proving with LLMs. If provers are powerful enough, you no longer need to understand the code — only the contracts at th...

000

gavin.codes @gavin.codes · 30/05/2026

1/4 Here is a video of neuro-symbolic theorem proving in action using the (opensource) Rocq-piler MCP (we renamed when updating to Rocq) with the Rocq theorem prover.

100

gavin.codes @gavin.codes · 24/05/2026

1/2 One shotted type preservation for PCF+references, including obtaining all necessary lemmata for the proof using the latest version of our MCP for coq (github.com/scidonia/mcp...) using DeepSeek v4.

101

gavin.codes @gavin.codes · 21/05/2026

I'm making good progress on an automated theorem environment for python using only an MCP. But to make that work well, I needed interactive LLM theorem proving. For this I've developed an MCP for the Coq/Rocq theorem prover. github.com/scidonia/mcp...

github.com

GitHub - scidonia/mcp-coq-lsp: MCP server for Coq LSP

MCP server for Coq LSP. Contribute to scidonia/mcp-coq-lsp development by creating an account on GitHub.

000

gavin.codes @gavin.codes · 23/04/2026

Software engineering is now mostly robot management. I'm not sure I like it, but that's where it has to go.

100

gavin.codes @gavin.codes · 16/04/2026

Cross-checking generated content increases quality substantially, but what models should I use to *cross-check* generated content. It turns out for entity extraction you can use almost anything! Use the model which is 200x cheaper. See below 👇

100

gavin.codes @gavin.codes · 14/04/2026

Riffing on an idea that is making the rounds of using a wiki knowledge base to drive your LLM, we tried this approach just for chat short term memory. The results were very sensitive to the ontology and organisation, we get better results than raw summary. It works amazingly well! See below 👇

120

gavin.codes @gavin.codes · 13/04/2026

Ontologies can be helpful in structuring short term memory for interactive agents. We developed a methodology for short-term memory assessment and demonstrate a comparison between naive summarisation and ontology centric memory. Full discussion and methodology below 👇

110

gavin.codes @gavin.codes · 10/04/2026

Entity extraction from documents can provide huge benefits to organisations. If your model is hallucinating information - it will pollute downstream assets. The key is appropriate provenance tracking and cross checking. Methodology link below 👇

100

Reposted by @gavin.codes

Scidonia @scidonia.bsky.social · 09/04/2026

We benchmarked Claude Sonnet 4.6, GPT-5.4, and Gemini 3 Pro on PERSON entity extraction across eight open-licence documents, spanning 18th-century literary prose, research papers, biomedical articles, & Wikipedia. Here is what we found - scidonia.ai/blog/llm-ent...

scidonia.ai

Which LLM Finds People Best? Benchmarking Claude, GPT-5.4 and Gemini 3 on PERSON Entity Extraction | Scidonia

We ran three frontier models on 8 open-licence documents and measured how accurately each one identifies named people — before and after cross-checking. The results reveal meaningful differences in hallucination rates and the value of verification.

011

gavin.codes @gavin.codes · 09/04/2026

Are you using the right models to analyze your documents? When performing large-context entity extraction, model matters and cross checking has an important impact on precision. It is easier for models to check than to generate, so checking is often worthwhile.

010

gavin.codes @gavin.codes · 22/12/2025

Here is concrete example of a Neurosymbolic programming framework using a proof assistant which is also a programming language (Rocq). All you have to do is drop this MCP in your opencode (or similar) coding framework and you can have LLMs write certifiably correct code. github.com/scidonia/mcp...

github.com

GitHub - scidonia/mcp-coq-lsp: MCP server for Coq LSP

MCP server for Coq LSP. Contribute to scidonia/mcp-coq-lsp development by creating an account on GitHub.

010

gavin.codes @gavin.codes · 11/12/2025

At bookwyrm.ai we've been performing experiments in Neural-symbolic programming and we're getting amazing results. Generative AI driven by both specification and formal verification.

121

gavin.codes @gavin.codes · 09/12/2025

🧵1/ I've been conducting experiments with the use of LLMs for "Design by Contract" (DbC), a paradigm described by Bertrand Meyer. DbC is quite straightforward to use in a language like python (for instance using icontract). The idea is essentially to:

131

gavin.codes @gavin.codes · 08/12/2025

AI can't replace humans but that doesn't mean you can't use it to achieve important workflow efficiencies.

010

Reposted by @gavin.codes

Scidonia @scidonia.bsky.social · 04/12/2025

As a dev-focused startup, talking with developers is important to understand what is important to you. We would love to talk with fellow developers to show off BookWrym and to get your feedback. Willing to help? Please send us a DM or fill in the form on this page: bookwyrm.ai/contact #developers

041

gavin.codes @gavin.codes · 04/12/2025

1/ If you're using AIs to generate code, you might want to have a look at this chart. Language choice now should also take into account AI comprehension and writing abilities.

110

Reposted by @gavin.codes

Scidonia @scidonia.bsky.social · 04/12/2025

BookWyrm #API for back office automation. Extract text from docs > create semantic chunks > structure with Pydantic models > automate workflows. Type-safe JSON output, source attribution, quality scores. Perfect for invoicing, compliance, data entry. bookwyrm.ai/backoffice-automation #ai #dev

bookwyrm.ai

Back office Automation - Build Reliable AI Pipelines with BookWyrm

Learn how to build reliable back office automation using BookWyrm's data pipeline. Transform unstructured documents into AI-ready data for automated backoffice workflows.

041

gavin.codes @gavin.codes · 01/12/2025

1/ AI is changing the way we write code and that means tools and methodologies have to change. It’s time to bring en.wikipedia.org/wiki/Design_... back into style.

en.wikipedia.org

Design by contract - Wikipedia

100

gavin.codes @gavin.codes · 28/11/2025

1/ I used to lecture in CS. Due to AI, I can tell you if I did it now I would not allow any computers in my class room at all. Assignments would be pen and paper. Students need to learn to reason, first and foremost.

110

gavin.codes @gavin.codes · 26/11/2025

1/ Reactors I have known and loved: LAMPRE One of the weirdest and most innovative reactors that I've come across is the LAMPRE reactor. As some may know, one of the biggest safety problems that nuclear reactors experience is a meltdown, which usually occurs from a loss of coolant event.

131