commit - 2c427bcc0f0e56eb79a6040424334dcb9c4f848a
commit + 71c65582d277160a6367c7c817baf4093d375460
blob - bdb6b8d00c529b3d62b7a5dec711a1df9e5204f3
blob + e864cda3a3ec5e85ef725d8981f44d5fce583edb
--- README.md
+++ README.md
@@ -62,6 +62,7 @@ PingCAP | | | ```TLA+``` [TLA+ in TiDB](https://github
 [Sukhoi](https://www.sukhoi.org/) | Russia, Moscow | Aerospace and defense | [```ANSYS SCADE Suite```](https://www.ansys.com/products/embedded-software/ansys-scade-suite) (source - [A Formally Verified Compiler for Lustre](http://www.tbrk.org/papers/pldi17-slides.pdf))
 [TrustInSoft](https://trust-in-soft.com/) | USA, CA, San Francisco | - | ```TrustInSoft Analyzer``` [Site](https://trust-in-soft.com/polarssl-verification-kit/)
 [Trustworthy Systems](https://ts.data61.csiro.au/) | Australia, Sydney  |  | ```Isabelle/HOL```, ```Coq``` [Site](https://ts.data61.csiro.au/projects/TS/l4.verified/)
+[Two Six Technologies](https://twosixtech.com/) | USA | Defense research | ```Isabelle/HOL```, Hardware verification ([example](https://github.com/twosixlabs/ReWire)), ```Coq``` ([example](https://github.com/twosixlabs/coq-operads))
 [JetBrains Research](https://jetbrains.org) | Saint Petersburg, Russia | - | `Coq` ([source](https://research.jetbrains.org/ru/groups/group-for-dependent-types-and-hott))
 [МЦСТ](http://www.mcst.ru/) | Moscow, Russia | ? | ```SPIN/Promela``` [Методы и средства верификации протоколов когерентности памяти](https://www.youtube.com/watch?v=67eD3hLmU_8&t=43s)
 [T-Platforms](https://www.t-platforms.ru/) | Moscow, Russia | - | ```Coq```, ```SPIN/Promela```, ```TLA+```, ```McErlang```, ```mCRL2``` [Employee CV](https://ru.linkedin.com/in/evgeniy-shishkin-9b1b67b3)