docs: update documentation for v0.2.0 and formal verification integration

README.adoc:
- Add Idris badge "Powered by Idris"
- Update tagline: "with permanence, powered by formal verification"
- Add rescript-dom-mounter to architecture (high-assurance rendering)
- Add Proven library (Idris2) to architecture
- Add formal verification layer to tech stack
- Update links to proven and rescript-dom-mounter repos

ROADMAP.adoc:
- Mark v0.2.0 (Deployment & Infrastructure) as COMPLETE
- Update v0.1.0 status to 70% complete
- Add v0.4.0 milestone: Formal Verification Integration
  * rescript-dom-mounter integration
  * Proven library (Idris2) proofs
  * Verified formula evaluation
  * Type-level guarantees for data integrity
- Reorder milestones: Views → Formal Verification → Collaboration → Automations
- Add v0.8.0 (Advanced Features) and v1.0.0 (Production Release) milestones
- Update last modified date to 2026-02-05

STATE.scm:
- Update version: 0.1.0 → 0.2.0
- Update project name: formbase → glyphbase
- Update updated timestamp: 2026-02-05T12:30:00Z
- Add "formerly: formbase" metadata
- Update tagline: "Carve your data in stone"
- Add tech stack entries: high-assurance, formal-verification
- Update database: FormDB → Lithoglyph
- Update overall completion: 55% → 70%
- Add deployment-infrastructure component: 100% COMPLETE
- Add formal-verification component: 0% (planned for v0.4.0)
- Update working features with Phase 2 deliverables:
  * GitHub Pages landing page
  * Docker multi-stage builds
  * docker-compose stack
  * Multi-arch images (amd64, arm64)
  * Automated releases to ghcr.io
  * 6 installation methods

ECOSYSTEM.scm:
- Update name: formbase → glyphbase
- Add "formerly: FormBase" metadata
- Update purpose: add "and formal verification"
- Update related projects:
  * formdb → lithoglyph (foundation)
  * Add rescript-dom-mounter (dependency)
  * Add proven (dependency - Idris2 verification)
  * fqldt → gql-dt (sibling-standard)
  * formdb-studio → lithoglyph-studio
  * formdb-debugger → lithoglyph-debugger
  * Add airtable (inspiration)
- Update what-this-is: add "formally verified" description
- Update what-this-is-not: clarify positioning

META.scm:
- Update name: formbase → glyphbase
- Add "formerly: formbase" metadata
- Accept ADR-004 (custom grid component)
- Add ADR-005 (Formal verification with Idris2)
  * Type-level correctness proofs
  * Integration with Proven library
  * Compile-time verification
- Add ADR-006 (High-assurance DOM rendering)
  * rescript-dom-mounter for critical UI
  * XSS prevention at type level
  * End-to-end proofs with Proven
- Add ADR-007 (GitHub Pages + Docker deployment)
  * Custom domain support
  * Multi-arch builds
  * 6 installation methods
- Add why-formal-verification rationale
- Update why-formdb-backend → why-lithoglyph-backend

All repos confirmed to have Hypatia and Scorecard workflows.

Phase 2 (Deployment & Infrastructure) complete.
Formal verification integration planned for v0.4.0.

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

Author: Jonathan D.A. Jewell

ECOSYSTEM.scm

@@ -1,82 +1,102 @@
 ; SPDX-License-Identifier: PMPL-1.0-or-later
-; FormBase - Ecosystem Position
+; Glyphbase - Ecosystem Position
 
 (ecosystem
   (version "1.0")
-  (name "formbase")
+  (name "glyphbase")
   (type "application")
-  (purpose "Open-source Airtable alternative with provenance tracking")
+  (purpose "Open-source Airtable alternative with permanence and formal verification")
+  (formerly "formbase")
 
   (position-in-ecosystem
-    (role "End-user spreadsheet-database application")
+    (role "End-user spreadsheet-database application with provenance")
     (layer "Application layer")
-    (users "Non-technical users, researchers, teams, small businesses"))
+    (users "Non-technical users, researchers, teams, small businesses, scientists"))
 
   (related-projects
-    (project "formdb"
+    (project "lithoglyph"
       (relationship foundation)
-      (url "https://github.com/hyperpolymath/formdb")
-      (description "The narrative-first database that powers FormBase")
-      (integration "All data stored in FormDB with provenance"))
+      (url "https://github.com/hyperpolymath/lithoglyph")
+      (description "Stone-carved database engine with provenance and reversibility")
+      (integration "All data stored in Lithoglyph with full audit trail"))
 
-    (project "fqldt"
+    (project "rescript-dom-mounter"
+      (relationship dependency)
+      (url "https://github.com/hyperpolymath/rescript-dom-mounter")
+      (description "High-assurance DOM rendering library")
+      (integration "Used for critical UI components requiring formal verification"))
+
+    (project "proven"
+      (relationship dependency)
+      (url "https://github.com/hyperpolymath/proven")
+      (description "Idris2 formal verification library")
+      (integration "Type-level correctness proofs for data operations"))
+
+    (project "gql-dt"
       (relationship sibling-standard)
-      (url "https://github.com/hyperpolymath/fqldt")
-      (description "Dependently-typed query language")
-      (integration "Formulas may use FQLdt for type-checked expressions"))
+      (url "https://github.com/hyperpolymath/gql-dt")
+      (description "Glyph Query Language with dependent types")
+      (integration "Advanced queries with type-level guarantees"))
 
-    (project "formdb-studio"
+    (project "lithoglyph-studio"
       (relationship sibling-standard)
-      (url "https://github.com/hyperpolymath/formdb-studio")
-      (description "Admin GUI for FormDB")
-      (integration "FormBase for end-users, Studio for admins/developers"))
+      (url "https://github.com/hyperpolymath/lithoglyph-studio")
+      (description "Admin GUI for Lithoglyph databases")
+      (integration "Glyphbase for end-users, Studio for admins/developers"))
 
-    (project "formdb-debugger"
+    (project "lithoglyph-debugger"
       (relationship sibling-standard)
-      (url "https://github.com/hyperpolymath/formdb-debugger")
+      (url "https://github.com/hyperpolymath/lithoglyph-debugger")
       (description "Proof-carrying database debugger")
-      (integration "Debug and recover FormBase data with proofs"))
+      (integration "Debug and recover Glyphbase data with proofs"))
 
     (project "bofig"
       (relationship potential-consumer)
       (url "https://github.com/hyperpolymath/bofig")
       (description "Evidence graph for investigative journalism")
-      (integration "BoFIG could embed FormBase for evidence management"))
+      (integration "BoFIG could embed Glyphbase for evidence management"))
 
-    (project "zotero-formdb"
+    (project "zotero-formbd"
       (relationship sibling-standard)
-      (url "https://github.com/hyperpolymath/zotero-formdb")
+      (url "https://github.com/hyperpolymath/zotero-formbd")
       (description "Reference manager with PROMPT scores")
-      (integration "Shared PROMPT scoring system"))
+      (integration "Shared PROMPT scoring methodology"))
+
+    (project "airtable"
+      (relationship inspiration)
+      (url "https://airtable.com")
+      (description "Commercial spreadsheet-database hybrid")
+      (integration "UX inspiration for views and interface design"))
 
     (project "nocodb"
       (relationship inspiration)
       (url "https://github.com/nocodb/nocodb")
       (description "Open source Airtable alternative")
-      (integration "UX inspiration, not code sharing"))
+      (integration "Reference for open-source implementation patterns"))
 
     (project "baserow"
       (relationship inspiration)
       (url "https://github.com/bram2w/baserow")
-      (description "Self-hosted database")
-      (integration "UX inspiration, not code sharing"))
+      (description "Self-hosted no-code database")
+      (integration "Self-hosting deployment patterns"))
 
     (project "yjs"
       (relationship dependency)
       (url "https://github.com/yjs/yjs")
-      (description "CRDT framework for collaboration")
-      (integration "Real-time sync and offline support")))
+      (description "CRDT framework for real-time collaboration")
+      (integration "Conflict-free multi-user editing and offline support")))
 
   (what-this-is
     ("A spreadsheet-database hybrid for non-technical users")
-    ("An Airtable alternative with provenance built-in")
-    ("A self-hosted, offline-first data management tool")
-    ("A collaborative workspace with real-time sync")
-    ("A research-grade data collection platform with PROMPT scores"))
+    ("An Airtable alternative with permanence - every change carved in stone")
+    ("A self-hosted, offline-first data management platform")
+    ("A collaborative workspace with real-time sync via CRDTs")
+    ("A research-grade data platform with PROMPT quality scores")
+    ("A formally verified application using Idris2 correctness proofs"))
 
   (what-this-is-not
-    ("Not a replacement for Excel/Sheets (different use case)")
-    ("Not a general-purpose database admin tool (use FormDB Studio)")
-    ("Not a BI/analytics platform (use Metabase etc.)")
-    ("Not a form builder only (forms are one view type)")
-    ("Not a low-code app builder (focused on data, not apps)")))
+    ("Not a replacement for Excel/Sheets - different collaboration model")
+    ("Not a general-purpose database admin tool - use Lithoglyph Studio instead")
+    ("Not a BI/analytics platform - use Metabase or similar")
+    ("Not just a form builder - forms are one view type among many")
+    ("Not a low-code app builder - focused on data management, not app development")))

META.scm

@@ -3,7 +3,8 @@
 
 (meta
   (version "1.0")
-  (name "formbase")
+  (name "glyphbase")
+  (formerly "formbase")
   (media-type "application/meta+scheme")
 
   (architecture-decisions
@@ -44,14 +45,54 @@
         ("Requires careful state management")))
 
     (adr-004
-      (status proposed)
+      (status accepted)
       (date "2026-01-11")
       (title "Custom grid component vs library")
       (context "Need a spreadsheet-like grid with excellent performance")
-      (decision "Evaluate AG Grid vs custom implementation")
+      (decision "Build custom grid component for full control and accessibility")
+      (consequences
+        ("Full control over rendering and behavior")
+        ("Accessibility-first design from the ground up")
+        ("No commercial license restrictions")
+        ("Slower initial development but better long-term")))
+
+    (adr-005
+      (status accepted)
+      (date "2026-02-05")
+      (title "Formal verification with Idris2")
+      (context "Need mathematical guarantees for critical data operations")
+      (decision "Integrate Proven library (Idris2) for type-level correctness proofs")
       (consequences
-        ("AG Grid: faster to market, commercial license")
-        ("Custom: full control, accessible, slower development"))))
+        ("Type-level guarantees for CRUD operations")
+        ("Provable correctness for formula evaluation")
+        ("Steeper learning curve for contributors")
+        ("Compile-time verification of data integrity")
+        ("Integration with rescript-dom-mounter for UI proofs")))
+
+    (adr-006
+      (status accepted)
+      (date "2026-02-05")
+      (title "High-assurance DOM rendering")
+      (context "UI bugs in data management apps can cause data loss")
+      (decision "Use rescript-dom-mounter for critical UI components")
+      (consequences
+        ("Formal verification of DOM rendering correctness")
+        ("Prevention of XSS and injection attacks at type level")
+        ("Better error messages during development")
+        ("Integration with Proven library for end-to-end proofs")))
+
+    (adr-007
+      (status accepted)
+      (date "2026-02-05")
+      (title "GitHub Pages + Docker deployment")
+      (context "Need simple deployment with custom domain support")
+      (decision "Use GitHub Pages for docs/landing, Docker for application")
+      (consequences
+        ("Free hosting for documentation site")
+        ("Custom domain (glyphbase.lithoglyph.org)")
+        ("Multi-arch Docker images (amd64, arm64)")
+        ("Automated releases to ghcr.io")
+        ("6 installation methods for different use cases"))))
 
   (development-practices
     (code-style
@@ -84,11 +125,20 @@
       (features "feat/* - feature branches")))
 
   (design-rationale
-    (why-formdb-backend
-      "FormBase is not just another Airtable clone. By building on FormDB,
-       every cell change automatically has provenance, every operation is
-       reversible, and data quality can be scored. These are table stakes
-       for research, journalism, and any domain where trust matters.")
+    (why-lithoglyph-backend
+      "Glyphbase is not just another Airtable clone. By building on Lithoglyph,
+       every cell change is carved in stone with provenance, every operation is
+       mathematically reversible, and data quality can be scored via PROMPT.
+       These guarantees are essential for research, journalism, legal work,
+       and any domain where trust and auditability matter.")
+
+    (why-formal-verification
+      "Data management applications have a unique responsibility: users trust
+       them with critical information. By using Idris2 for formal verification,
+       we provide mathematical proofs that our CRUD operations are correct,
+       formulas are evaluated properly, and UI rendering cannot introduce
+       data corruption. This level of assurance is unprecedented in spreadsheet
+       software and sets a new standard for data integrity.")
 
     (why-offline-first
       "Most spreadsheet tools assume constant connectivity. FormBase uses

README.adoc

@@ -1,4 +1,5 @@
 image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"]
+image:https://img.shields.io/badge/Powered_by-Idris-purple.svg[Powered by Idris,link="https://www.idris-lang.org/"]
 // SPDX-License-Identifier: PMPL-1.0-or-later
 // SPDX-FileCopyrightText: 2025 hyperpolymath
 
@@ -10,7 +11,7 @@ image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,
 [.lead]
 *Carve your data in stone.*
 
-_The open-source Airtable alternative with permanence._
+_The open-source Airtable alternative with permanence, powered by formal verification._
 
 == What is Glyphbase?
 
@@ -69,16 +70,21 @@ _Coming soon_
 ----
 ┌─────────────────────────────────────────────────────────────┐
 │  Browser UI (ReScript + React)                              │
+│  • rescript-dom-mounter (high-assurance rendering)          │
+│  • Proven library integration (Idris formal verification)   │
 │  Grid | Kanban | Calendar | Gallery | Form Builder          │
 ├─────────────────────────────────────────────────────────────┤
 │  Real-time Collaboration (WebSocket + Yjs CRDT)             │
 ├─────────────────────────────────────────────────────────────┤
 │  API Server (Gleam on BEAM)                                 │
 │  REST + WebSocket + Automations                             │
 ├─────────────────────────────────────────────────────────────┤
-│  Lithoglyph Engine                                              │
+│  Lithoglyph Engine                                          │
 │  Provenance | Reversibility | PROMPT Scores                 │
 ├─────────────────────────────────────────────────────────────┤
+│  Formal Verification Layer (Idris2)                         │
+│  Type-level guarantees | Correctness proofs                 │
+├─────────────────────────────────────────────────────────────┤
 │  Storage: Local | Dropbox | GDrive | S3                     │
 └─────────────────────────────────────────────────────────────┘
 ----
@@ -261,6 +267,12 @@ Link records to canonical sources. DOI-linked records are immutable; edits creat
 | UI Framework
 | ReScript + React
 
+| High-Assurance Rendering
+| link:https://github.com/hyperpolymath/rescript-dom-mounter[rescript-dom-mounter]
+
+| Formal Verification
+| link:https://github.com/hyperpolymath/proven[Proven] (Idris2 proofs)
+
 | State Management
 | Jotai
 

ROADMAP.adoc

@@ -1,22 +1,98 @@
 // SPDX-License-Identifier: PMPL-1.0-or-later
-= YOUR Template Repo Roadmap
+= Glyphbase Roadmap
 
 == Current Status
 
-Initial development phase.
+*v0.1.0* - Core Grid implementation with deployment infrastructure (70% complete)
 
 == Milestones
 
-=== v0.1.0 - Foundation
-* [ ] Core functionality
-* [ ] Basic documentation
-* [ ] CI/CD pipeline
+=== v0.1.0 - Core Grid _(70% Complete - In Progress)_
+* [x] Create/delete bases and tables
+* [x] Add/edit/delete rows
+* [x] Core field types (text, number, date, select, multi-select)
+* [x] Sort, filter, hide columns
+* [x] Keyboard navigation
+* [x] Lithoglyph provenance integration (scaffolded)
 
-=== v1.0.0 - Stable Release
-* [ ] Full feature set
-* [ ] Comprehensive tests
-* [ ] Production ready
+=== v0.2.0 - Deployment & Infrastructure _(✅ Complete)_
+* [x] Landing page at glyphbase.lithoglyph.org
+* [x] GitHub Pages deployment workflow
+* [x] Docker & docker-compose setup
+* [x] Multi-arch container builds (amd64, arm64)
+* [x] Comprehensive installation guide (6 methods)
+* [x] Automated release workflow to ghcr.io
+* [x] Documentation conversion (AsciiDoc → HTML)
+
+=== v0.3.0 - Multiple Views _(Next Priority)_
+* [ ] Kanban view with drag-and-drop
+* [ ] Calendar view with date field mapping
+* [ ] Gallery view with image attachments
+* [ ] Form builder for public data collection
+
+=== v0.4.0 - Formal Verification Integration
+* [ ] Integrate link:https://github.com/hyperpolymath/rescript-dom-mounter[rescript-dom-mounter] for high-assurance rendering
+* [ ] Add link:https://github.com/hyperpolymath/proven[Proven] library (Idris2) integration
+* [ ] Formal proofs for critical data operations
+* [ ] Verified formula evaluation engine
+* [ ] Correctness proofs for CRUD operations
+* [ ] Type-level guarantees for cell data integrity
+
+=== v0.5.0 - Real-time Collaboration
+* [ ] Real-time cursors with Yjs CRDT
+* [ ] WebSocket-based synchronization
+* [ ] Cell comments and discussions
+* [ ] Activity feed from Lithoglyph provenance
+* [ ] @mentions for team notifications
+* [ ] Conflict-free collaborative editing
+
+=== v0.6.0 - Automations & Workflows
+* [ ] Trigger/action automation system
+* [ ] Webhooks for external integrations
+* [ ] Email notifications (SMTP/SendGrid)
+* [ ] Scheduled tasks (cron-like)
+* [ ] Slack/Discord integrations
+* [ ] Custom JavaScript automation scripts
+
+=== v0.7.0 - Lithoglyph Superpowers
+* [ ] Provenance view for cell history
+* [ ] Time travel UI (view data at any point in time)
+* [ ] PROMPT scoring for data quality
+* [ ] Proof export (audit-grade documentation)
+* [ ] DOI linking for immutable records
+* [ ] Cryptographic integrity verification
+
+=== v0.8.0 - Advanced Features
+* [ ] Formula system (Excel-like)
+* [ ] Rollup and lookup field types
+* [ ] Linked records (foreign keys)
+* [ ] File attachments (S3/local)
+* [ ] API rate limiting and quotas
+* [ ] Row-level permissions
+
+=== v1.0.0 - Production Release
+* [ ] Complete test coverage (>90%)
+* [ ] Performance optimization (10k+ records per table)
+* [ ] Security audit completion
+* [ ] Accessibility compliance (WCAG 2.1 AA)
+* [ ] Mobile-responsive design
+* [ ] Import from Airtable/CSV/Excel
+* [ ] Export to multiple formats
+* [ ] Migration tooling for existing databases
 
 == Future Directions
 
-_To be determined based on community feedback._
+=== Post-1.0 Considerations
+* AI-powered data insights
+* Natural language queries (via GQL)
+* Advanced visualizations (charts, graphs)
+* Blockchain-backed provenance
+* Multi-tenant SaaS deployment
+* Enterprise SSO (SAML, LDAP)
+* Advanced caching strategies
+* GraphQL API alongside REST
+
+---
+
+*Last Updated:* 2026-02-05
+*Version:* 0.2.0 complete, 0.3.0 next