Veridian — Hardened Banking System
This project implements a formally verified, production-grade banking system integrated with the Veridian fraud intelligence platform.
Formal Verification (TLA+)
Three TLA+ specifications formally verify core banking invariants:
Spec
Invariants Verified
tla+/BankingSystem.tla
Double-entry, no money creation, frozen account isolation, idempotency, balance non-negativity, transaction atomicity
tla+/FraudDetection.tla
Score bounds [0,1], all transactions scored, blocked transactions invariant, audit trail append-only, reversal preserves original
tla+/Reconciliation.tla
Global balance, per-account balance, hash chain integrity, no orphaned entries, double-entry per transaction
cmd/
bank/ — Banking REST API server
veridian/ — Fraud intelligence CLI
internal/
banking/
domain/ — Account, Transaction models with invariants
ledger/ — Double-entry ledger with SHA-256 hash chain
service/ — Account & transaction processing
api/ — REST API with auth, CORS, rate limiting
fraud/ — Fraud evaluation engine
compliance/ — AML/CTR/SAR alerting
repository/ — PostgreSQL persistence
config/ — Configuration management
Standard
Implementation
ISO 27001
RBAC, encryption (AES-256-GCM), audit logging, security policies
PCI DSS
PAN masking, CVV never stored, card data encryption, key rotation
SWIFT CSP
User management, segregation of duties, threat monitoring, incident response
ISO 20022
PACS.008/PAIN.001 XML messaging, validation, parsing
NIST CSF
Identify (vulnerability mgmt), Protect (encryption/RBAC), Detect (monitoring), Respond (incidents), Recover (reconciliation)
Go 1.22+
PostgreSQL 16+
Docker (optional)
# Build both binaries
make build
# Run banking server
make run-bank
# Run CLI
make run-cli
# Run with Docker
docker compose up --build
# Evaluate transaction
veridian evaluate --score 0.85 --amount 50000
# Sign audit payload
veridian sign --data " audit payload" --mode hybrid
# Check security posture
veridian posture
# Simulate threat
veridian threat --type auth_brute_force --count 15
# Check API health
veridian health --url http://localhost:8080
Method
Path
Description
POST
/v1/banking/accounts
Create account
GET
/v1/banking/accounts/{id}
Get account
GET
/v1/banking/accounts/{id}/balance
Get balance
POST
/v1/banking/accounts/{id}/freeze
Freeze account
POST
/v1/banking/accounts/{id}/unfreeze
Unfreeze account
POST
/v1/banking/accounts/{id}/close
Close account
POST
/v1/banking/transfers
Transfer funds
POST
/v1/banking/deposits
Deposit funds
POST
/v1/banking/withdrawals
Withdraw funds
GET
/v1/banking/transactions/{id}
Get transaction
GET
/v1/banking/health
Health check
Security Invariants (TLA+ Verified)
Double-Entry : ∀ tx: sum(debits) = sum(credits)
No Money Creation : ∀ acct: balance + overdraft >= 0
Frozen Isolation : frozen acct → no operations
Idempotency : same key → same result
Score Bounds : ∀ tx: 0.0 ≤ fraudScore ≤ 1.0
Audit Append-Only : ∀ i < j: audit[i].clock ≤ audit[j].clock
Hash Chain : ∀ entry: hash = SHA-256(prev + tx + acct + amount)
# Python tests (existing)
python -m pytest tests/ -q
# Go tests
go test ./internal/... -v -cover